This module provides binding constructs using higher-order syntax and a function for translating to first-order syntax. Expressions constructed using the exported interface are guaranteed to have a well-behaved translation.
- data Variable ctx a
- evalLambda :: Eval dom => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> a
- data Let ctxa ctxb a where
- data HOLambda ctx dom a where
- type HOAST ctx dom = AST (HOLambda ctx dom :+: (Variable ctx :+: dom))
- type HOASTF ctx dom a = HOAST ctx dom (Full a)
- lambda :: (Typeable a, Typeable b, Sat ctx a) => (HOASTF ctx dom a -> HOASTF ctx dom b) -> HOASTF ctx dom (a -> b)
- lambdaN :: forall ctx dom a. NAry ctx a (HOLambda ctx dom :+: (Variable ctx :+: dom)) => a -> HOASTF ctx dom (NAryEval a)
- letBindCtx :: forall ctxa ctxb dom a b. (Typeable a, Typeable b, (Let ctxa ctxb) :<: dom, Sat ctxa a, Sat ctxb b) => Proxy ctxb -> HOASTF ctxa dom a -> (HOASTF ctxa dom a -> HOASTF ctxa dom b) -> HOASTF ctxa dom b
- letBind :: (Typeable a, Typeable b, (Let Poly Poly) :<: dom) => HOASTF Poly dom a -> (HOASTF Poly dom a -> HOASTF Poly dom b) -> HOASTF Poly dom b
- reifyM :: forall ctx dom a. Typeable a => HOAST ctx dom a -> State VarId (AST (Lambda ctx :+: (Variable ctx :+: dom)) a)
- reifyTop :: Typeable a => HOAST ctx dom a -> AST (Lambda ctx :+: (Variable ctx :+: dom)) a
- class (SyntacticN a internal, NAry ctx internal (HOLambda ctx dom :+: (Variable ctx :+: dom)), Typeable (NAryEval internal)) => Reifiable ctx a dom internal | a -> dom internal
- reifyCtx :: Reifiable ctx a dom internal => Proxy ctx -> a -> ASTF (Lambda ctx :+: (Variable ctx :+: dom)) (NAryEval internal)
- reify :: Reifiable Poly a dom internal => a -> ASTF (Lambda Poly :+: (Variable Poly :+: dom)) (NAryEval internal)
Documentation
Variables
WitnessSat (Variable ctx) | |
WitnessCons (Variable ctx) | |
ExprEq (Variable ctx) |
|
ToTree (Variable ctx) | |
Render (Variable ctx) |
evalLambda :: Eval dom => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> aSource
Evaluation of closed lambda expressions
data HOLambda ctx dom a whereSource
Higher-order lambda binding
HOLambda :: (Typeable a, Typeable b, Sat ctx a) => (HOASTF ctx dom a -> HOASTF ctx dom b) -> HOLambda ctx dom (Full (a -> b)) |
WitnessCons (HOLambda ctx dom) |
lambda :: (Typeable a, Typeable b, Sat ctx a) => (HOASTF ctx dom a -> HOASTF ctx dom b) -> HOASTF ctx dom (a -> b)Source
Lambda binding
lambdaN :: forall ctx dom a. NAry ctx a (HOLambda ctx dom :+: (Variable ctx :+: dom)) => a -> HOASTF ctx dom (NAryEval a)Source
N-ary lambda binding
letBindCtx :: forall ctxa ctxb dom a b. (Typeable a, Typeable b, (Let ctxa ctxb) :<: dom, Sat ctxa a, Sat ctxb b) => Proxy ctxb -> HOASTF ctxa dom a -> (HOASTF ctxa dom a -> HOASTF ctxa dom b) -> HOASTF ctxa dom bSource
Let binding with explicit context
letBind :: (Typeable a, Typeable b, (Let Poly Poly) :<: dom) => HOASTF Poly dom a -> (HOASTF Poly dom a -> HOASTF Poly dom b) -> HOASTF Poly dom bSource
Let binding
reifyM :: forall ctx dom a. Typeable a => HOAST ctx dom a -> State VarId (AST (Lambda ctx :+: (Variable ctx :+: dom)) a)Source
reifyTop :: Typeable a => HOAST ctx dom a -> AST (Lambda ctx :+: (Variable ctx :+: dom)) aSource
Translating expressions with higher-order binding to corresponding expressions using first-order binding
class (SyntacticN a internal, NAry ctx internal (HOLambda ctx dom :+: (Variable ctx :+: dom)), Typeable (NAryEval internal)) => Reifiable ctx a dom internal | a -> dom internalSource
Convenient class alias for n-ary syntactic functions