Safe Haskell	None

Language.Syntactic.Constructs.Binding

Contents

Variables
Lambda binding
Let binding
Interpretation
Alpha equivalence

Description

General binding constructs

Synopsis

Variables

newtype VarId Source

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 Source

data Variable a whereSource

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

Lambda binding

data Lambda a whereSource

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

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

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

Let binding

data Let a whereSource

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

Interpretation

subst Source

Arguments

:: forall constr dom a b . (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 Source

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 whereSource

Evaluation of expressions with variables

Methods

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

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)] aSource

Evaluation of possibly open expressions

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

Evaluation of closed expressions

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

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)Source

Convenient default implementation of evalBindSym

Alpha equivalence

class VarEqEnv a whereSource

Environments containing a list of variable equivalences

Methods

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

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

Instances

VarEqEnv [(VarId, VarId)]
VarEqEnv (EqEnv dom p)

class AlphaEq sub1 sub2 dom env whereSource

Alpha-equivalence

Methods

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

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 Source

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

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

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 Source

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