Safe Haskell	None
Language	Haskell2010

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 Source
Eq VarId Source
Integral VarId Source
Num VarId Source
Ord VarId Source
Real VarId Source
Show VarId Source
Ix VarId Source
(~) (* -> Constraint) p (Sat dom) => NodeEqEnv dom (EqEnv dom p) Source
VarEqEnv [(VarId, VarId)] Source
VarEqEnv (EqEnv dom p) Source

showVar :: VarId -> String Source

data Variable a where Source

Variables

Constructors

Variable :: VarId -> Variable (Full a)

Instances

Equality Variable Source	`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 Source
Render Variable Source
Constrained Variable Source
EvalBind Variable Source
Optimize Variable Source
(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Variable Variable dom env Source
IsHODomain (HODomain dom p pVar) p pVar Source
type Sat Variable = Top Source

Lambda binding

data Lambda a where Source

Lambda binding

Constructors

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

Instances

Equality Lambda Source	`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 Source
Render Lambda Source
Constrained Lambda Source
EvalBind Lambda Source
Optimize Lambda Source
(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Lambda Lambda dom env Source
type Sat Lambda = Top Source

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

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 Source
StringTree Let Source
Render Let Source
Eval Let Source
Constrained Let Source
EvalBind Let Source
Optimize Let Source
AlphaEq dom dom dom env => AlphaEq Let Let dom env Source
type Sat Let = Top Source

Interpretation

subst Source

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

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 Source
EvalBind Condition Source
EvalBind Construct Source
EvalBind Identity Source
EvalBind Literal Source
EvalBind Tuple Source
EvalBind Select Source
EvalBind Let Source
EvalBind Lambda Source
EvalBind Variable Source
Monad m => EvalBind (MONAD m) Source
(EvalBind sub1, EvalBind sub2) => EvalBind ((:+:) sub1 sub2) Source
EvalBind dom => EvalBind ((:\|\|) dom pred) Source
EvalBind dom => EvalBind ((:\|) dom pred) Source
EvalBind dom => EvalBind (Decor info dom) Source
EvalBind dom => EvalBind (SubConstr1 c dom p) Source
EvalBind dom => EvalBind (SubConstr2 c dom pa pb) Source

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

Evaluation of possibly open expressions

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

Evaluation of closed expressions

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

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

Environments containing a list of variable equivalences

Methods

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

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

Instances

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

class AlphaEq sub1 sub2 dom env where Source

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 Source
AlphaEq dom dom dom env => AlphaEq Condition Condition dom env Source
AlphaEq dom dom dom env => AlphaEq Construct Construct dom env Source
AlphaEq dom dom dom env => AlphaEq Identity Identity dom env Source
AlphaEq dom dom dom env => AlphaEq Literal Literal dom env Source
AlphaEq dom dom dom env => AlphaEq Tuple Tuple dom env Source
AlphaEq dom dom dom env => AlphaEq Select Select dom env Source
AlphaEq dom dom dom env => AlphaEq Let Let dom env Source
(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Lambda Lambda dom env Source
(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Variable Variable dom env Source
(AlphaEq dom dom dom env, NodeEqEnv dom env) => AlphaEq Node Node dom env Source
(AlphaEq dom dom dom env, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env Source
(AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) => AlphaEq ((:+:) subA1 subA2) ((:+:) subB1 subB2) dom env Source
AlphaEq sub sub dom env => AlphaEq ((:\|\|) sub pred) ((:\|\|) sub pred) dom env Source
AlphaEq sub sub dom env => AlphaEq ((:\|) sub pred) ((:\|) sub pred) dom env Source
AlphaEq sub sub dom env => AlphaEq (Decor info sub) (Decor info sub) dom env Source
AlphaEq sub sub dom env => AlphaEq (SubConstr1 c sub p) (SubConstr1 c sub p) dom env Source
AlphaEq sub sub dom env => AlphaEq (SubConstr2 c sub pa pb) (SubConstr2 c sub pa pb) dom env Source

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