module Language.Syntactic.Features.Binding.HigherOrder
( Variable
, evalLambda
, Let (..)
, HOLambda (..)
, HOAST
, HOASTF
, lambda
, lambdaN
, letBindCtx
, letBind
, reifyM
, reifyTop
, Reifiable
, reifyCtx
, reify
) where
import Control.Monad.State
import Data.Typeable
import Data.Proxy
import Language.Syntactic
import Language.Syntactic.Features.Binding
data HOLambda ctx dom a
where
HOLambda :: (Typeable a, Typeable b, Sat ctx a)
=> (HOASTF ctx dom a -> HOASTF ctx dom b)
-> HOLambda ctx dom (Full (a -> b))
type HOAST ctx dom = AST (HOLambda ctx dom :+: Variable ctx :+: dom)
type HOASTF ctx dom a = HOAST ctx dom (Full a)
instance WitnessCons (HOLambda ctx dom)
where
witnessCons (HOLambda _) = ConsWit
lambda :: (Typeable a, Typeable b, Sat ctx a) =>
(HOASTF ctx dom a -> HOASTF ctx dom b) -> HOASTF ctx dom (a -> b)
lambda = inject . HOLambda
lambdaN :: forall ctx dom a
. NAry ctx a (HOLambda ctx dom :+: Variable ctx :+: dom)
=> a -> HOASTF ctx dom (NAryEval a)
lambdaN = bindN (Proxy :: Proxy ctx) lambda
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
letBindCtx _ a f = inject let' :$: a :$: lambda f
where
let' :: Let ctxa ctxb (a :-> (a -> b) :-> Full b)
let' = Let
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
letBind = letBindCtx poly
reifyM :: forall ctx dom a . Typeable a
=> HOAST ctx dom a
-> State VarId (AST (Lambda ctx :+: Variable ctx :+: 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)
body <- reifyM $ f $ inject $ (Variable v `withContext` ctx)
return $ inject (Lambda v `withContext` ctx) :$: body
where
ctx = Proxy :: Proxy ctx
reifyTop :: Typeable a =>
HOAST ctx dom a -> AST (Lambda ctx :+: Variable ctx :+: dom) a
reifyTop = flip evalState 0 . reifyM
class
( SyntacticN a internal
, NAry ctx internal (HOLambda ctx dom :+: Variable ctx :+: dom)
, Typeable (NAryEval internal)
) =>
Reifiable ctx a dom internal | a -> dom internal
instance
( SyntacticN a internal
, NAry ctx internal (HOLambda ctx dom :+: Variable ctx :+: dom)
, Typeable (NAryEval internal)
) =>
Reifiable ctx a dom internal
reifyCtx :: Reifiable ctx a dom internal
=> Proxy ctx
-> a
-> ASTF (Lambda ctx :+: Variable ctx :+: dom) (NAryEval internal)
reifyCtx _ = reifyTop . lambdaN . desugarN
reify :: Reifiable Poly a dom internal =>
a -> ASTF (Lambda Poly :+: Variable Poly :+: dom) (NAryEval internal)
reify = reifyCtx poly