Safe Haskell | None |
---|
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
- data Let ctxa ctxb a where
- data HOLambda ctx dom a where
- type HODomain ctx dom = HOLambda ctx dom :+: (Variable ctx :+: dom)
- lambda :: (Typeable a, Typeable b, Sat ctx a) => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) -> ASTF (HODomain ctx dom) (a -> b)
- reifyM :: forall ctx dom a. Typeable a => AST (HODomain ctx dom) a -> State VarId (AST (Lambda ctx :+: (Variable ctx :+: dom)) a)
- reifyTop :: Typeable a => AST (HODomain ctx dom) a -> AST (Lambda ctx :+: (Variable ctx :+: dom)) a
- reify :: Syntactic a (HODomain ctx dom) => a -> ASTF (Lambda ctx :+: (Variable ctx :+: dom)) (Internal a)
Documentation
Variables
MaybeWitnessSat ctx1 (Variable ctx2) | |
MaybeWitnessSat ctx (Variable ctx) | |
WitnessSat (Variable ctx) | |
WitnessCons (Variable ctx) | |
ExprEq (Variable ctx) |
|
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, VarEqEnv 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) |
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
).
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 |
data HOLambda ctx dom a whereSource
Higher-order lambda binding
HOLambda :: (Typeable a, Typeable b, Sat ctx a) => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) -> HOLambda ctx dom (Full (a -> b)) |
MaybeWitnessSat ctx1 (HOLambda ctx2 dom) | |
WitnessCons (HOLambda ctx dom) | |
(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 :: (Typeable a, Typeable b, Sat ctx a) => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) -> ASTF (HODomain ctx dom) (a -> b)Source
Lambda binding
reifyM :: forall ctx dom a. Typeable a => AST (HODomain ctx dom) a -> State VarId (AST (Lambda ctx :+: (Variable ctx :+: dom)) a)Source