Copyright	(c) Murdoch J. Gabbay 2020
License	GPL-3
Maintainer	murdoch.gabbay@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Language.Nominal.Examples.Assembly2

Description

Based on an example in the Bound package. This is interesting for the binding behaviour of Add and the swapping behaviour of Swp. Add adds two numbers and binds the result to a fresh register with scope over subsequent instructions. Swp swaps the contents of two registers with scope over subsequent instructions.

Synopsis

type V = Name String
data Operand
- = Lit Int
- | Var V
data Prog
- = Ret Operand
- | Swp Operand Operand Prog
- | Add Operand Operand (KAbs V Prog)
evalOperand :: Operand -> Int
normaliseProg :: Prog -> Prog
evalProg :: Prog -> Int
example1 :: Prog
example1eval :: Int

Documentation

type V = Name String Source #

Variables are string-labelled names

data Operand Source #

An operand is an integer literal or a variable

Constructors

Lit Int
Var V

Instances

Eq Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods (==) :: Operand -> Operand -> Bool # (/=) :: Operand -> Operand -> Bool #
Show Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods showsPrec :: Int -> Operand -> ShowS # show :: Operand -> String # showList :: [Operand] -> ShowS #
Generic Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Associated Types type Rep Operand :: Type -> Type # Methods from :: Operand -> Rep Operand x # to :: Rep Operand x -> Operand #
Swappable Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods kswp :: Typeable s => KAtom s -> KAtom s -> Operand -> Operand Source #
KSub V Operand Prog Source #	Substitution on `Prog`rams is generic
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Prog -> Prog Source #
KSub V Operand Operand Source #	Substitution as standard on `Operand`
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Operand -> Operand Source #
type Rep Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 type Rep Operand = D1 (MetaData "Operand" "Language.Nominal.Examples.Assembly2" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" False) (C1 (MetaCons "Lit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: C1 (MetaCons "Var" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 V)))

data Prog Source #

Terms of our assembly language

Constructors

Ret Operand	Return a value
Swp Operand Operand Prog	Swap the contents of two variables
Add Operand Operand (KAbs V Prog)	Add two operands and store the value in a fresh variable which is local to subsequent computation (the third argument)

Instances

Eq Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods (==) :: Prog -> Prog -> Bool # (/=) :: Prog -> Prog -> Bool #
Show Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods showsPrec :: Int -> Prog -> ShowS # show :: Prog -> String # showList :: [Prog] -> ShowS #
Generic Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Associated Types type Rep Prog :: Type -> Type # Methods from :: Prog -> Rep Prog x # to :: Rep Prog x -> Prog #
Swappable Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods kswp :: Typeable s => KAtom s -> KAtom s -> Prog -> Prog Source #
KSub V Operand Prog Source #	Substitution on `Prog`rams is generic
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Prog -> Prog Source #
type Rep Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 type Rep Prog = D1 (MetaData "Prog" "Language.Nominal.Examples.Assembly2" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" False) (C1 (MetaCons "Ret" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Operand)) :+: (C1 (MetaCons "Swp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Operand) :: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Operand) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Prog))) :+: C1 (MetaCons "Add" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Operand) :: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Operand) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (KAbs V Prog))))))

evalOperand :: Operand -> Int Source #

Evaluate an operand.

A literal maps to its corresponding integer.
If asked to evaluate a free variable, complain.

normaliseProg :: Prog -> Prog Source #

Normalise a program by executing any embedded Swp commands.

evalProg :: Prog -> Int Source #

Evaluate a program

example1 :: Prog Source #

Add 1 2 [v] Add v v [w] Swp v w Ret w

example1eval :: Int Source #

3