Language.Syntactic.Constructs.Binding

General binding constructs

Variables

newtype VarId

Variable identifier

Constructors

VarId

Fields

varInteger :: Integer

Instances

Enum VarId

Eq VarId

Integral VarId

Num VarId

Ord VarId

Real VarId

Show VarId

Ix VarId

(~) (* -> Constraint) p (Sat dom) => NodeEqEnv dom (EqEnv dom p)

VarEqEnv [(VarId, VarId)]

VarEqEnv (EqEnv dom p)

showVar :: VarId -> String

data Variable a where

Variables

Constructors

Variable :: VarId -> Variable (Full a)

Instances

Equality Variable

equal does strict identifier comparison; i.e. no alpha equivalence.

exprHash assigns the same hash to all variables. This is a valid over-approximation that enables the following property:

alphaEq a b  ==>  exprHash a == exprHash b

StringTree Variable

Render Variable

Constrained Variable

EvalBind Variable

Optimize Variable

(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Variable Variable dom env

IsHODomain (HODomain dom p pVar) p pVar

type Sat Variable = Top

Lambda binding

data Lambda a where

Lambda binding

Constructors

Lambda :: VarId -> Lambda (b :-> Full (a -> b))

Instances

Equality Lambda

equal does strict identifier comparison; i.e. no alpha equivalence.

exprHash assigns the same hash to all Lambda bindings. This is a valid over-approximation that enables the following property:

alphaEq a b  ==>  exprHash a == exprHash b

StringTree Lambda

Render Lambda

Constrained Lambda

EvalBind Lambda

Optimize Lambda

(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Lambda Lambda dom env

type Sat Lambda = Top

reuseLambda :: Lambda (b :-> Full (a -> b)) -> Lambda (c :-> Full (a -> c))

Allow an existing binding to be used with a body of a different type

Let binding

data Let a where

Let binding

Let is just an application operator with flipped argument order. The argument (a -> b) is preferably constructed by Lambda.

Constructors

Let :: Let (a :-> ((a -> b) :-> Full b))

Instances

Equality Let

StringTree Let

Render Let

Eval Let

Constrained Let

EvalBind Let

Optimize Let

AlphaEq dom dom dom env => AlphaEq Let Let dom env

type Sat Let = Top

Interpretation

subst

Arguments

:: (ConstrainedBy dom Typeable, Project Lambda dom, Project Variable dom)

=> VarId

Variable to be substituted

-> ASTF dom a

Expression to substitute for

-> ASTF dom b

Expression to substitute in

-> ASTF dom b

Should be a capture-avoiding substitution, but it is currently not correct.

Note: Variables with a different type than the new expression will be silently ignored.

betaReduce

Arguments

:: (ConstrainedBy dom Typeable, Project Lambda dom, Project Variable dom)

=> ASTF dom a

Argument

-> ASTF dom (a -> b)

Function to be reduced

-> ASTF dom b

Beta-reduction of an expression. The expression to be reduced is assumed to be a Lambda.

class EvalBind sub where

Evaluation of expressions with variables

Minimal complete definition

Nothing

Methods

evalBindSym :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig)) => sub sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Instances

EvalBind Empty

EvalBind Condition

EvalBind Construct

EvalBind Identity

EvalBind Literal

EvalBind Tuple

EvalBind Select

EvalBind Let

EvalBind Lambda

EvalBind Variable

Monad m => EvalBind (MONAD m)

(EvalBind sub1, EvalBind sub2) => EvalBind ((:+:) sub1 sub2)

EvalBind dom => EvalBind ((:||) dom pred)

EvalBind dom => EvalBind ((:|) dom pred)

EvalBind dom => EvalBind (Decor info dom)

EvalBind dom => EvalBind (SubConstr1 c dom p)

EvalBind dom => EvalBind (SubConstr2 c dom pa pb)

evalBindM :: (EvalBind dom, ConstrainedBy dom Typeable) => ASTF dom a -> Reader [(VarId, Dynamic)] a

Evaluation of possibly open expressions

evalBind :: (EvalBind dom, ConstrainedBy dom Typeable) => ASTF dom a -> a

Evaluation of closed expressions

appDen :: Denotation sig -> Args Identity sig -> DenResult sig

Apply a symbol denotation to a list of arguments

evalBindSymDefault :: (Eval sub, EvalBind dom, ConstrainedBy dom Typeable) => sub sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Convenient default implementation of evalBindSym

Alpha equivalence

class VarEqEnv a where

Environments containing a list of variable equivalences

Methods

prjVarEqEnv :: a -> [(VarId, VarId)]

modVarEqEnv :: ([(VarId, VarId)] -> [(VarId, VarId)]) -> a -> a

Instances

VarEqEnv [(VarId, VarId)]

VarEqEnv (EqEnv dom p)

class AlphaEq sub1 sub2 dom env where

Alpha-equivalence

Minimal complete definition

Nothing

Methods

alphaEqSym :: sub1 a -> Args (AST dom) a -> sub2 b -> Args (AST dom) b -> Reader env Bool

Instances

AlphaEq Empty Empty dom env

AlphaEq dom dom dom env => AlphaEq Condition Condition dom env

AlphaEq dom dom dom env => AlphaEq Construct Construct dom env

AlphaEq dom dom dom env => AlphaEq Identity Identity dom env

AlphaEq dom dom dom env => AlphaEq Literal Literal dom env

AlphaEq dom dom dom env => AlphaEq Tuple Tuple dom env

AlphaEq dom dom dom env => AlphaEq Select Select dom env

AlphaEq dom dom dom env => AlphaEq Let Let dom env

(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Lambda Lambda dom env

(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Variable Variable dom env

(AlphaEq dom dom dom env, NodeEqEnv dom env) => AlphaEq Node Node dom env

(AlphaEq dom dom dom env, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env

(AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) => AlphaEq ((:+:) subA1 subA2) ((:+:) subB1 subB2) dom env

AlphaEq sub sub dom env => AlphaEq ((:||) sub pred) ((:||) sub pred) dom env

AlphaEq sub sub dom env => AlphaEq ((:|) sub pred) ((:|) sub pred) dom env

AlphaEq sub sub dom env => AlphaEq (Decor info sub) (Decor info sub) dom env

AlphaEq sub sub dom env => AlphaEq (SubConstr1 c sub p) (SubConstr1 c sub p) dom env

AlphaEq sub sub dom env => AlphaEq (SubConstr2 c sub pa pb) (SubConstr2 c sub pa pb) dom env

alphaEqM :: AlphaEq dom dom dom env => ASTF dom a -> ASTF dom b -> Reader env Bool

alphaEqM2 :: AlphaEq dom dom dom env => ASTF dom b -> dom a -> Args (AST dom) a -> Reader env Bool

alphaEq :: AlphaEq dom dom dom [(VarId, VarId)] => ASTF dom a -> ASTF dom b -> Bool

Alpha-equivalence on lambda expressions. Free variables are taken to be equivalent if they have the same identifier.

alphaEqSymDefault :: (Equality sub, AlphaEq dom dom dom env) => sub a -> Args (AST dom) a -> sub b -> Args (AST dom) b -> Reader env Bool

alphaEqChildren :: AlphaEq dom dom dom env => AST dom a -> AST dom b -> Reader env Bool