module Language.Syntactic.Features.Binding.HigherOrder
( Variable
, evalLambda
, Let (..)
, HOLambda (..)
, HOAST
, lambda
, lambdaN
, letBind
, reifyM
, reifyHOAST
, Reifiable
, reify
) where
import Control.Monad.State
import Data.Typeable
import Language.Syntactic
import Language.Syntactic.Features.Binding
data HOLambda dom a
where
HOLambda :: (Typeable a, Typeable b)
=> (HOAST dom (Full a) -> HOAST dom (Full b))
-> HOLambda dom (Full (a -> b))
type HOAST dom = AST (HOLambda dom :+: Variable :+: dom)
lambda :: (Typeable a, Typeable b) =>
(HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full (a -> b))
lambda = inject . HOLambda
lambdaN :: NAry a (HOLambda dom :+: Variable :+: dom) =>
a -> HOAST dom (Full (NAryEval a))
lambdaN = bindN lambda
letBind :: (Typeable a, Typeable b, Let :<: dom)
=> HOAST dom (Full a)
-> (HOAST dom (Full a) -> HOAST dom (Full b))
-> HOAST dom (Full b)
letBind a f = inject Let :$: a :$: lambda f
reifyM :: Typeable a
=> HOAST dom a
-> State VarId (AST (Lambda :+: Variable :+: dom) a)
reifyM (f :$: a) = liftM2 (:$:) (reifyM f) (reifyM a)
reifyM (Symbol (InjectR a)) = return $ Symbol $ InjectR a
reifyM (Symbol (InjectL (HOLambda f))) = do
v <- get; put (v+1)
liftM (inject (Lambda v) :$:) $ reifyM $ f $ inject $ Variable v
reifyHOAST :: Typeable a => HOAST dom a -> AST (Lambda :+: Variable :+: dom) a
reifyHOAST = flip evalState 0 . reifyM
class
( SyntacticN a internal
, NAry internal (HOLambda dom :+: Variable :+: dom)
, Typeable (NAryEval internal)
) =>
Reifiable a dom internal | a -> dom internal
instance
( SyntacticN a internal
, NAry internal (HOLambda dom :+: Variable :+: dom)
, Typeable (NAryEval internal)
) =>
Reifiable a dom internal
reify :: Reifiable a dom internal =>
a -> ASTF (Lambda :+: Variable :+: dom) (NAryEval internal)
reify = reifyHOAST . lambdaN . desugarN