module Language.Syntactic.Constructs.Binding.HigherOrder
( Variable
, Let (..)
, HOLambda (..)
, HODomain
, lambda
, reifyM
, reifyTop
, reify
) where
import Control.Monad.State
import Data.Typeable
import Data.Proxy
import Language.Syntactic
import Language.Syntactic.Constructs.Binding
data HOLambda ctx dom a
where
HOLambda :: (Typeable a, Typeable b, Sat ctx a)
=> (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b)
-> HOLambda ctx dom (Full (a -> b))
type HODomain ctx dom = HOLambda ctx dom :+: Variable ctx :+: dom
instance WitnessCons (HOLambda ctx dom)
where
witnessCons (HOLambda _) = ConsWit
instance MaybeWitnessSat ctx1 (HOLambda ctx2 dom)
where
maybeWitnessSat _ _ = Nothing
lambda :: (Typeable a, Typeable b, Sat ctx a)
=> (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b)
-> ASTF (HODomain ctx dom) (a -> b)
lambda = inj . HOLambda
instance
( Syntactic a (HODomain ctx dom)
, Syntactic b (HODomain ctx dom)
, Sat ctx (Internal a)
) =>
Syntactic (a -> b) (HODomain ctx dom)
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 ctx dom a . Typeable a
=> AST (HODomain ctx dom) a
-> State VarId (AST (Lambda ctx :+: Variable ctx :+: dom) a)
reifyM (f :$ a) = liftM2 (:$) (reifyM f) (reifyM a)
reifyM (Sym (InjR a)) = return $ Sym $ InjR a
reifyM (Sym (InjL (HOLambda f))) = do
v <- get; put (v+1)
body <- reifyM $ f $ inj $ (Variable v `withContext` ctx)
return $ inj (Lambda v `withContext` ctx) :$ body
where
ctx = Proxy :: Proxy ctx
reifyTop :: Typeable a =>
AST (HODomain ctx dom) a -> AST (Lambda ctx :+: Variable ctx :+: dom) a
reifyTop = flip evalState 0 . reifyM
reify :: Syntactic a (HODomain ctx dom)
=> a
-> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a)
reify = reifyTop . desugar