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

Language.Syntactic.Features.Binding

Contents

Description

General binding constructs

Synopsis

Variables

newtype VarId Source

Variable identifier

Constructors

VarId 

Fields

varInteger :: Integer
 

data Variable ctx a whereSource

Variables

Constructors

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

Instances

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) 

prjVariable :: (Variable ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Variable ctx a)Source

Partial Variable projection with explicit context

Lambda binding

data Lambda ctx a whereSource

Lambda binding

Constructors

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

Instances

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) 

prjLambda :: (Lambda ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Lambda ctx a)Source

Partial Lambda projection with explicit context

alphaEqM :: ((Lambda ctx) :<: dom, (Variable ctx) :<: dom) => Proxy ctx -> (forall a b. AST dom a -> AST dom b -> Reader [(VarId, VarId)] Bool) -> forall a b. AST dom a -> AST dom b -> Reader [(VarId, VarId)] BoolSource

Alpha equivalence in an environment of variable equivalences. The supplied equivalence function gets called when the argument expressions are not both Variables, both Lambdas or both :$:.

alphaEq :: ((Lambda ctx) :<: dom, (Variable ctx) :<: dom, ExprEq dom) => Proxy ctx -> AST dom a -> AST dom b -> BoolSource

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

evalLambdaM :: (Eval dom, MonadReader [(VarId, Dynamic)] m) => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> m aSource

Evaluation of possibly open lambda expressions

evalLambda :: Eval dom => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> aSource

Evaluation of closed lambda expressions

class NAry ctx a dom | a -> dom whereSource

The class of n-ary binding functions

Associated Types

type NAryEval a Source

Methods

bindN :: Proxy ctx -> (forall b c. (Typeable b, Typeable c, Sat ctx b) => (ASTF dom b -> ASTF dom c) -> ASTF dom (b -> c)) -> a -> ASTF dom (NAryEval a)Source

N-ary binding by nested use of the supplied binder

Instances

(Typeable a, Sat ctx a, NAry ctx b dom, Typeable (NAryEval b)) => NAry ctx (ASTF dom a -> b) dom 
Sat ctx a => NAry ctx (ASTF dom a) dom 

Let binding

data Let ctxa ctxb a whereSource

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

WitnessSat (Let ctxa ctxb) 
WitnessCons (Let ctxa ctxb) 
ExprEq (Let ctxa ctxb) 
ToTree (Let ctxa ctxb) 
Render (Let ctxa ctxb) 
Eval (Let ctxa ctxb) 

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

Partial Let projection with explicit context