StatefulLocalSemantics.hs

test :: (Local Int !! Ask Int + (!) (State Bool + IO)) ()
test = do
    raise $ send0 $ put False
    k <- getCC
    local @Int (+ 1) do
        unlessM (raise $ send0 get) k
        raise $ send0 $ put True
        env <- ask @Int
        raise $ send0 $ sendIns $ print env

elaborateLocalStatefully ::
    forall r eh ef.
    (Ask r <| ef, Ask r <| (LState r ': ef), Forall HFunctor eh) =>
    (Local r ': eh) :!! ef ~> eh :!! ef
elaborateLocalStatefully a = do
    initialEnv <- ask @r
    evalStateRec initialEnv do
        raise a & interpretRecH \(Local f a') -> do
            currentEnv <- get @r
            put $ f currentEnv
            r <- a' & interposeRec @(Ask r) \Ask -> get
            put currentEnv
            pure r

evalStateRec :: forall s eh ef. Forall HFunctor eh => s -> eh :!! (LState s ': ef) ~> eh :!! ef
evalStateRec s =
    splitUnder >>> interpretAllRec (raiseAllH . evalState s . fromEffF |+ exhaust)

splitUnder :: Forall HFunctor eh => eh :!! ef ~> eh :!! '[LiftIns ((:!) ef)]
splitUnder = transformAll (inject0 . LiftIns . liftIns . EffUnionF)