module Language.Syntactic.Sharing.ReifyHO
( reifyGraphTop
, reifyGraph
) where
import Control.Monad.Writer
import Data.IntMap as Map
import Data.IORef
import Data.Typeable
import System.Mem.StableName
import Data.Proxy
import Language.Syntactic
import Language.Syntactic.Features.Binding
import Language.Syntactic.Features.Binding.HigherOrder
import Language.Syntactic.Sharing.Graph
import Language.Syntactic.Sharing.StableName
import qualified Language.Syntactic.Sharing.Reify
type GraphMonad ctx dom a = WriterT
[(NodeId, SomeAST (Node ctx :+: Lambda ctx :+: Variable ctx :+: dom))]
IO
(AST (Node ctx :+: Lambda ctx :+: Variable ctx :+: dom) a)
reifyGraphM :: forall ctx dom a . Typeable a
=> (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))
-> IORef VarId
-> IORef NodeId
-> IORef (History (HOAST ctx dom))
-> HOASTF ctx dom a
-> GraphMonad ctx dom (Full a)
reifyGraphM canShare vSupp nSupp history = reifyNode
where
reifyNode :: Typeable b => HOASTF ctx dom b -> GraphMonad ctx dom (Full b)
reifyNode a = case canShare a of
Nothing -> reifyRec a
Just Witness' | a `seq` True -> do
st <- liftIO $ makeStableName a
hist <- liftIO $ readIORef history
case lookHistory hist (StName st) of
Just n -> return $ Symbol $ InjectL $ Node n
_ -> do
n <- fresh nSupp
liftIO $ modifyIORef history $ remember (StName st) n
a' <- reifyRec a
tell [(n, SomeAST a')]
return $ Symbol $ InjectL $ Node n
reifyRec :: HOAST ctx dom b -> GraphMonad ctx dom b
reifyRec (f :$: a) = liftM2 (:$:) (reifyRec f) (reifyNode a)
reifyRec (Symbol (InjectR a)) = return $ Symbol (InjectR (InjectR a))
reifyRec (Symbol (InjectL (HOLambda f))) = do
v <- fresh vSupp
body <- reifyNode $ f $ inject $ (Variable v `withContext` ctx)
return $ inject (Lambda v `withContext` ctx) :$: body
where
ctx = Proxy :: Proxy ctx
reifyGraphTop :: Typeable a
=> (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))
-> HOASTF ctx dom a
-> IO (ASG ctx (Lambda ctx :+: Variable ctx :+: dom) a, VarId)
reifyGraphTop canShare a = do
vSupp <- newIORef 0
nSupp <- newIORef 0
history <- newIORef empty
(a',ns) <- runWriterT $ reifyGraphM canShare vSupp nSupp history a
v <- readIORef vSupp
n <- readIORef nSupp
return (ASG a' ns n, v)
reifyGraph :: Reifiable ctx a dom internal
=> (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))
-> a
-> IO
( ASG ctx (Lambda ctx :+: Variable ctx :+: dom) (NAryEval internal)
, VarId
)
reifyGraph canShare = reifyGraphTop canShare . lambdaN . desugarN