General binding constructs
- newtype VarId = VarId {}
- showVar :: VarId -> String
- data Variable ctx a where
- prjVariable :: (Variable ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Variable ctx a)
- data Lambda ctx a where
- prjLambda :: (Lambda ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Lambda ctx a)
- class NAry ctx a dom | a -> dom where
- data Let ctxa ctxb a where
- prjLet :: (Let ctxa ctxb) :<: sup => Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)
- 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)] Bool
- alphaEq :: ((Lambda ctx) :<: dom, (Variable ctx) :<: dom, ExprEq dom) => Proxy ctx -> AST dom a -> AST dom b -> Bool
- evalLambdaM :: (Eval dom, MonadReader [(VarId, Dynamic)] m) => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> m a
- evalLambda :: Eval dom => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> a
Variables
Variable identifier
data Variable ctx a whereSource
Variables
WitnessSat (Variable ctx) | |
WitnessCons (Variable ctx) | |
ExprEq (Variable ctx) |
|
ToTree (Variable ctx) | |
Render (Variable ctx) | |
PartialEval dom ctx dom => PartialEval (Variable ctx) ctx dom |
prjVariable :: (Variable ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Variable ctx a)Source
Partial Variable
projection with explicit context
Lambda binding
Lambda binding
WitnessCons (Lambda ctx) | |
ExprEq (Lambda ctx) |
|
ToTree (Lambda ctx) | |
Render (Lambda ctx) | |
PartialEval dom ctx dom => PartialEval (Lambda ctx) ctx dom |
prjLambda :: (Lambda ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Lambda ctx a)Source
Partial Lambda
projection with explicit context
class NAry ctx a dom | a -> dom whereSource
The class of n-ary binding functions
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
).
WitnessSat (Let ctxa ctxb) | |
WitnessCons (Let ctxa ctxb) | |
ExprEq (Let ctxa ctxb) | |
ToTree (Let ctxa ctxb) | |
Render (Let ctxa ctxb) | |
Eval (Let ctxa ctxb) | |
((Let ctxa ctxb) :<: dom, PartialEval dom ctx dom) => PartialEval (Let ctxa ctxb) ctx dom |
prjLet :: (Let ctxa ctxb) :<: sup => Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)Source
Partial Let
projection with explicit context
Interpretation
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
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.