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)
- 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
- 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)
Variables
Variable identifier
data Variable ctx a whereSource
Variables
WitnessSat (Variable ctx) | |
WitnessCons (Variable ctx) | |
ExprEq (Variable ctx) |
|
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
Lambda binding
WitnessCons (Lambda ctx) | |
ExprEq (Lambda ctx) |
|
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
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