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.Assembly1

Description

Based on an example in the Bound package. What makes this interesting is the binding behaviour of Add, which adds two numbers and binds the result to a fresh register with scope over subsequent instructions.

Synopsis

type V = Name String
data Operand
- = Lit Int
- | Var V
data Prog
- = Ret Operand
- | Add Operand Operand (KAbs V Prog)
evalOperand :: Operand -> Int
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.Assembly1 Methods (==) :: Operand -> Operand -> Bool # (/=) :: Operand -> Operand -> Bool #
Show Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods showsPrec :: Int -> Operand -> ShowS # show :: Operand -> String # showList :: [Operand] -> ShowS #
Generic Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly1 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.Assembly1 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.Assembly1 Methods sub :: V -> Operand -> Prog -> Prog Source #
KSub V Operand Operand Source #	Substitution as standard on `Operand`
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods sub :: V -> Operand -> Operand -> Operand Source #
type Rep Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly1 type Rep Operand = D1 (MetaData "Operand" "Language.Nominal.Examples.Assembly1" "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
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.Assembly1 Methods (==) :: Prog -> Prog -> Bool # (/=) :: Prog -> Prog -> Bool #
Show Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods showsPrec :: Int -> Prog -> ShowS # show :: Prog -> String # showList :: [Prog] -> ShowS #
Generic Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly1 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.Assembly1 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.Assembly1 Methods sub :: V -> Operand -> Prog -> Prog Source #
type Rep Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly1 type Rep Prog = D1 (MetaData "Prog" "Language.Nominal.Examples.Assembly1" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" False) (C1 (MetaCons "Ret" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Operand)) :+: 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.

evalProg :: Prog -> Int Source #

Evaluate a program

example1 :: Prog Source #

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

example1eval :: Int Source #

6