module Language.Syntactic.Features.Binding.HigherOrder
( module Language.Syntactic
, Variable
, evalLambda
, Let (..)
, HOLambda (..)
, HOAST
, lambda
, lambdaN
, let_
, reifyM
, 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
, NAryDom a ~ (HOLambda dom :+: Variable :+: dom)
) =>
a -> HOAST dom (Full (NAryEval a))
lambdaN = bindN lambda
let_ :: (Typeable a, Typeable b, Let :<: dom)
=> HOAST dom (Full a)
-> (HOAST dom (Full a) -> HOAST dom (Full b))
-> HOAST dom (Full b)
let_ 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
reify :: Typeable a => HOAST dom a -> AST (Lambda :+: Variable :+: dom) a
reify = flip evalState 0 . reifyM