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

NodeEqEnv dom (EqEnv dom)

VarEqEnv [(VarId, VarId)]

VarEqEnv (EqEnv dom)

showVar :: VarId -> String

data Variable ctx a where

Variables

Constructors

Variable :: (Typeable a, Sat ctx a) => VarId -> Variable ctx (Full a)

Instances

MaybeWitnessSat ctx1 (Variable ctx2)

MaybeWitnessSat ctx (Variable ctx)

WitnessSat (Variable ctx)

WitnessCons (Variable ctx)

ExprEq (Variable ctx)

exprEq 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

ToTree (Variable ctx)

Render (Variable ctx)

EvalBind (Variable ctx)

(:<: (Variable ctx) dom, Optimize dom ctx dom) => Optimize (Variable ctx) ctx dom

AlphaEq dom dom dom env => AlphaEq (Variable ctx) (Variable ctx) dom env

(Syntactic a (HODomain ctx dom), Syntactic b (HODomain ctx dom), Sat ctx (Internal a)) => Syntactic (a -> b) (HODomain ctx dom)

(:<: (MONAD m) dom, Syntactic a (HODomain ctx dom), Monad m, Typeable1 m, Sat ctx (Internal a)) => Syntactic (Mon ctx dom m a) (HODomain ctx dom)

Lambda binding

data Lambda ctx a where

Lambda binding

Constructors

Lambda :: (Typeable a, Sat ctx a) => VarId -> Lambda ctx (b :-> Full (a -> b))

Instances

MaybeWitnessSat ctx1 (Lambda ctx2)

WitnessCons (Lambda ctx)

ExprEq (Lambda ctx)

exprEq 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

ToTree (Lambda ctx)

Render (Lambda ctx)

EvalBind (Lambda ctx)

(:<: (Lambda ctx) dom, Optimize dom ctx dom) => Optimize (Lambda ctx) ctx dom

AlphaEq dom dom dom env => AlphaEq (Lambda ctx) (Lambda ctx) dom env

Let binding

data Let ctxa ctxb a where

Let binding

A Let expression is really just an application of a lambda binding (the argument (a -> b) is preferably constructed by Lambda).

Constructors

Let :: (Sat ctxa a, Sat ctxb b) => Let ctxa ctxb (a :-> ((a -> b) :-> Full b))

Instances

MaybeWitnessSat ctx (Let ctxa ctxb)

MaybeWitnessSat ctxb (Let ctxa ctxb)

WitnessSat (Let ctxa ctxb)

WitnessCons (Let ctxa ctxb)

ExprEq (Let ctxa ctxb)

ToTree (Let ctxa ctxb)

Render (Let ctxa ctxb)

Eval (Let ctxa ctxb)

EvalBind (Let ctxa ctxb)

(:<: (Let ctxa ctxb) dom, Optimize dom ctx dom) => Optimize (Let ctxa ctxb) ctx dom

AlphaEq dom dom dom env => AlphaEq (Let ctxa ctxb) (Let ctxa ctxb) dom env

letBind :: (Sat ctx a, Sat ctx b) => Proxy ctx -> Let ctx ctx (a :-> ((a -> b) :-> Full b))

Let binding with explicit context

prjLet :: Let ctxa ctxb :<: sup => Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)

Partial Let projection with explicit context

Interpretation

subst

Arguments

:: forall ctx dom a b . (Lambda ctx :<: dom, Variable ctx :<: dom, Typeable a)

=> Proxy ctx

-> VarId

Variable to be substituted

-> ASTF dom a

Expression to substitute for

-> ASTF dom b

Expression to substitute in

-> ASTF dom b

Capture-avoiding substitution

betaReduce

Arguments

:: forall ctx dom a b . (Lambda ctx :<: dom, Variable ctx :<: dom)

=> Proxy ctx

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

Methods

evalBindSym :: (EvalBind dom, Signature a) => sub a -> Args (AST dom) a -> Reader [(VarId, Dynamic)] (DenResult a)

Instances

EvalBind (Condition ctx)

EvalBind (Construct ctx)

EvalBind (Identity ctx)

EvalBind (Literal ctx)

Monad m => EvalBind (MONAD m)

EvalBind (Select ctx)

EvalBind (Tuple ctx)

EvalBind (Lambda ctx)

EvalBind (Variable ctx)

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

EvalBind dom => EvalBind (Decor info dom)

EvalBind (Let ctxa ctxb)

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

Evaluation of possibly open expressions

evalBind :: EvalBind dom => ASTF dom a -> a

Evaluation of closed expressions

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

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)

class VarEqEnv env => AlphaEq sub1 sub2 dom env where

Methods

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

Instances

AlphaEq dom dom dom env => AlphaEq (Condition ctx) (Condition ctx) dom env

AlphaEq dom dom dom env => AlphaEq (Construct ctx) (Construct ctx) dom env

AlphaEq dom dom dom env => AlphaEq (Identity ctx) (Identity ctx) dom env

AlphaEq dom dom dom env => AlphaEq (Literal ctx) (Literal ctx) dom env

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

AlphaEq dom dom dom env => AlphaEq (Select ctx) (Select ctx) dom env

AlphaEq dom dom dom env => AlphaEq (Tuple ctx) (Tuple ctx) dom env

AlphaEq dom dom dom env => AlphaEq (Lambda ctx) (Lambda ctx) dom env

AlphaEq dom dom dom env => AlphaEq (Variable ctx) (Variable ctx) dom env

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

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

AlphaEq dom dom dom env => AlphaEq (Let ctxa ctxb) (Let ctxa ctxb) dom env

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

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

alphaEqM2 :: (AlphaEq dom dom dom env, Signature a) => 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 :: (ExprEq sub, AlphaEq dom dom dom env, Signature a, Signature b) => 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