nom-0.1.0.1: Name-binding & alpha-equivalence

Copyright(c) Murdoch J. Gabbay 2020
LicenseGPL-3
Maintainermurdoch.gabbay@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellNone
LanguageHaskell2010

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

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

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 Programs 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 Programs 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

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