SMR.Core.Exp

Abstract Syntax

data Decl s p

Top-level declaration, parameterised by the types of symbols and primitives.

Constructors

DeclMac Name (Exp s p)

DeclSet Name (Exp s p)

Instances

(Show p, Show s) => Show (Decl s p)

Methods

showsPrec :: Int -> Decl s p -> ShowS

show :: Decl s p -> String

showList :: [Decl s p] -> ShowS

data Exp s p

Expression, parameterised by the types of symbols and primitives

Constructors

XRef !(Ref s p)

Reference to an external thing.

XKey !Key !(Exp s p)

Keyed expressions.

XApp !(Exp s p) ![Exp s p]

Application of a function expression to an argument.

XVar !Name !Depth

Variable name with a depth counter.

XAbs ![Param] !(Exp s p)

Abstraction with a list of parameters and a body expression.

XSub !(Train s p) !(Exp s p)

Substitution train applied to an expression. The train car at the head of the list is applied first.

Instances

(Show s, Show p) => Show (Exp s p)

Methods

showsPrec :: Int -> Exp s p -> ShowS

show :: Exp s p -> String

showList :: [Exp s p] -> ShowS

data Param

Function parameter.

Constructors

PParam !Name !Form

Instances

Show Param

Methods

showsPrec :: Int -> Param -> ShowS

show :: Param -> String

showList :: [Param] -> ShowS

data Form

Form of argument required in application.

Constructors

PVal

Value for call-by-value.

PExp

Expression for call-by-name

Instances

Show Form

Methods

showsPrec :: Int -> Form -> ShowS

show :: Form -> String

showList :: [Form] -> ShowS

data Key

Expression keys (super primitives)

Constructors

KBox

Delay evaluation of an expression used as the argument of a call-by-value function application.

KRun

Run a boxed expression.

Instances

Show Key

Methods

showsPrec :: Int -> Key -> ShowS

show :: Key -> String

showList :: [Key] -> ShowS

type Train s p = [Car s p]

Substitution train.

data Car s p

A car on the substitution train, parameterised by the types used for symbols and primitives.

Constructors

CSim !(Snv s p)

Simultaneous subsitution.

CRec !(Snv s p)

Recursive substitution.

CUps !Ups

Lifting.

Instances

(Show p, Show s) => Show (Car s p)

Methods

showsPrec :: Int -> Car s p -> ShowS

show :: Car s p -> String

showList :: [Car s p] -> ShowS

data Snv s p

Explicit substitution map, parameterised by the types used for symbols and primitives.

Constructors

SSnv ![SnvBind s p]

Instances

(Show s, Show p) => Show (Snv s p)

Methods

showsPrec :: Int -> Snv s p -> ShowS

show :: Snv s p -> String

showList :: [Snv s p] -> ShowS

data SnvBind s p

Constructors

BindVar !Name !Depth !(Exp s p)

BindNom !Nom !(Exp s p)

Instances

(Show p, Show s) => Show (SnvBind s p)

Methods

showsPrec :: Int -> SnvBind s p -> ShowS

show :: SnvBind s p -> String

showList :: [SnvBind s p] -> ShowS

data Ups

Lifting indicator, mapping name and binding depth to number of levels to lift.

Constructors

UUps ![UpsBump]

Instances

Show Ups

Methods

showsPrec :: Int -> Ups -> ShowS

show :: Ups -> String

showList :: [Ups] -> ShowS

type UpsBump = ((Name, Depth), Bump)

Indicates how to bump the index on a variable.

data Ref s p

A reference to some external thing.

Constructors

RSym !s

An uninterpreted symbol.

RPrm !p

A primitive value.

RMac !Name

A macro name.

RSet !Name

A set name.

RNom !Nom

A nominal variable.

Instances

(Show p, Show s) => Show (Ref s p)

Methods

showsPrec :: Int -> Ref s p -> ShowS

show :: Ref s p -> String

showList :: [Ref s p] -> ShowS

type Name = Text

Generic names for things.

type Nom = Integer

Index of a nominal constant.

type Depth = Integer

Binding depth indicator.

type Bump = Integer

Bump index indicator.

data Text :: *

A space efficient, packed, unboxed Unicode text type.

Instances

Build Text

Methods

build :: Text -> Builder

type Item Text

type Item Text = Char

Compounds

makeXApps :: Exp s p -> [Exp s p] -> Exp s p

Make an application of a function to the given list of arguments, suppressing the application of there are no arguments.

takeXApps :: Exp s p -> Maybe (Exp s p, [Exp s p])

Take an application of a function to a list of arguments. TODO(BL): fix rubbish list append complexity.

makeXAbs :: [Param] -> Exp s p -> Exp s p

Make an abstraction, short circuiting to the body if there are no parameters.

nameOfParam :: Param -> Name

Get the name of a function parameter.

formOfParam :: Param -> Form

Get the argument form required by a parameter.

Substitution Trains

trainCons :: Car s p -> [Car s p] -> [Car s p]

Cons a car on the front of an existing train.

If the new car is empty it will be suppressed.

If the new car can be combined with the first car on the existing train then it will be combined.

trainAppend :: [Car s p] -> [Car s p] -> [Car s p]

Append two trains.

trainApply :: [Car s p] -> Exp s p -> Exp s p

Wrap an expression in a substitution train. If the expression is a plain

snvApply :: Bool -> Snv s p -> Exp s p -> Exp s p

Wrap a train consisting of a single simultaneous substitution around an expression.

snvOfNamesArgs :: [Name] -> [Exp s p] -> Snv s p

Build a substitution from lists of names and arguments.

Substitution Pushing

pushHead :: Exp s p -> Maybe (Exp s p)

Push down any outermost substitution train to reveal the head constructor.

pushDeep :: Exp s p -> Maybe (Exp s p)

Push down the left-most substitution train in an expression, or Nothing if there isn't one.