module Language.Syntactic.Constructs.Binding.HigherOrder
( Variable
, Let (..)
, HOLambda (..)
, HODomain
, lambda
, reifyM
, reifyTop
, reify
) where
import Control.Monad.State
import Language.Syntactic
import Language.Syntactic.Constructs.Binding
data HOLambda dom p a
where
HOLambda
:: p a
=> (ASTF (HODomain dom p) a -> ASTF (HODomain dom p) b)
-> HOLambda dom p (Full (a -> b))
type HODomain dom p = (HOLambda dom p :+: Variable :+: dom) :|| p
instance Constrained (HOLambda dom p)
where
type Sat (HOLambda dom p) = Top
exprDict _ = Dict
lambda
:: (p a, p (a -> b))
=> (ASTF (HODomain dom p) a -> ASTF (HODomain dom p) b)
-> ASTF (HODomain dom p) (a -> b)
lambda = injC . HOLambda
instance
( Syntactic a (HODomain dom p)
, Syntactic b (HODomain dom p)
, p (Internal a)
, p (Internal a -> Internal b)
) =>
Syntactic (a -> b) (HODomain dom p)
where
type Internal (a -> b) = Internal a -> Internal b
desugar f = lambda (desugar . f . sugar)
sugar = error "sugar not implemented for (a -> b)"
reifyM
:: AST (HODomain dom p) a
-> State VarId (AST ((Lambda :+: Variable :+: dom) :|| p) 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 (Variable v)
return $ injC (Lambda v) :$ body
reifyTop ::
AST (HODomain dom p) a -> AST ((Lambda :+: Variable :+: dom) :|| p) a
reifyTop = flip evalState 0 . reifyM
reify :: Syntactic a (HODomain dom p) =>
a -> ASTF ((Lambda :+: Variable :+: dom) :|| p) (Internal a)
reify = reifyTop . desugar