module Language.Syntactic.Constructs.Binding.HigherOrder
( Variable
, Let (..)
, HOLambda (..)
, HODomain
, FODomain
, CLambda
, lambda
, reifyM
, reifyTop
, reify
) where
import Control.Monad.State
import Language.Syntactic
import Language.Syntactic.Constructs.Binding
data HOLambda dom p pVar a
where
HOLambda
:: (p a, pVar a)
=> (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b)
-> HOLambda dom p pVar (Full (a -> b))
type HODomain dom p pVar = (HOLambda dom p pVar :+: (Variable :|| pVar) :+: dom) :|| p
type FODomain dom p pVar = (CLambda pVar :+: (Variable :|| pVar) :+: dom) :|| p
type CLambda pVar = SubConstr2 (->) Lambda pVar Top
lambda
:: (p (a -> b), p a, pVar a)
=> (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b)
-> ASTF (HODomain dom p pVar) (a -> b)
lambda = injC . HOLambda
instance
( Syntactic a (HODomain dom p pVar)
, Syntactic b (HODomain dom p pVar)
, p (Internal a -> Internal b)
, p (Internal a)
, pVar (Internal a)
) =>
Syntactic (a -> b) (HODomain dom p pVar)
where
type Internal (a -> b) = Internal a -> Internal b
desugar f = lambda (desugar . f . sugar)
sugar = error "sugar not implemented for (a -> b)"
reifyM :: forall dom p pVar a
. AST (HODomain dom p pVar) a -> State VarId (AST (FODomain dom p pVar) a)
reifyM (f :$ a) = liftM2 (:$) (reifyM f) (reifyM a)
reifyM (Sym (C' (InjR a))) = return $ Sym $ C' $ InjR a
reifyM (Sym (C' (InjL (HOLambda f)))) = do
v <- get; put (v+1)
body <- reifyM $ f $ injC $ symType pVar $ C' (Variable v)
return $ injC (symType pLam $ SubConstr2 (Lambda v)) :$ body
where
pVar = P::P (Variable :|| pVar)
pLam = P::P (CLambda pVar)
reifyTop :: AST (HODomain dom p pVar) a -> AST (FODomain dom p pVar) a
reifyTop = flip evalState 0 . reifyM
reify :: Syntactic a (HODomain dom p pVar) => a -> ASTF (FODomain dom p pVar) (Internal a)
reify = reifyTop . desugar