syntactic-1.15.1: Generic abstract syntax, and utilities for embedded languages

Safe HaskellNone
LanguageHaskell2010

Language.Syntactic.Constructs.Binding

Contents

Description

General binding constructs

Synopsis

Variables

newtype VarId Source

Variable identifier

Constructors

VarId 

Fields

varInteger :: Integer
 

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

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

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

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