A way to interpret delimited continuations in an EDSL

DelCont.hs

import Control.Monad.Trans.Cont hiding (shift,reset)
import Control.Monad.Trans.Reader
import Control.Monad.Trans.State







data Expr
  = Expr :&&: Expr
  | Not Expr
  | Var String
  | Expr :<: Expr
  | Forall String Expr
  | Exists String Expr
  | Reset Expr
  | Shift Expr
  | Continue Expr
  deriving (Show)


type Continuer a = Reader (Expr -> Expr) a

continue :: Expr -> Continuer Expr
continue x = do k <- ask
                return (k x)


makeContinuer :: Expr -> Continuer Expr
makeContinuer (x :&&: y) = (:&&:) <$> makeContinuer x <*> makeContinuer y
makeContinuer (Not x) = Not <$> makeContinuer x
makeContinuer (Var v) = pure (Var v)
makeContinuer (x :<: y) = (:<:) <$> makeContinuer x <*> makeContinuer y
makeContinuer (Forall v x) = Forall v <$> makeContinuer x
makeContinuer (Exists v x) = Exists v <$> makeContinuer x
makeContinuer (Reset x) = pure (Reset x)
makeContinuer (Shift x) = pure (Shift x)
makeContinuer (Continue x) = continue x





newtype Shifter a = Shifter { runShifter :: State Int ([Expr] -> a, [Expr]) }

instance Functor Shifter where
  fmap f x = Shifter $ do
               (g,e) <- runShifter x
               return (f.g, e)

instance Applicative Shifter where
  pure x = Shifter (pure (const x, []))
  f <*> x = Shifter $ do
              (f',e) <- runShifter f
              (x',e') <- runShifter x
              return (\env -> f' env (x' env), e ++ e')

shift :: Expr -> Shifter Expr
shift x = Shifter $ do
            i <- get
            put (i+1)
            return ((!! i), [x])



makeShifter :: Expr -> Shifter Expr
makeShifter (x :&&: y) = (:&&:) <$> makeShifter x <*> makeShifter y
makeShifter (Not x) = Not <$> makeShifter x
makeShifter (Var v) = pure (Var v)
makeShifter (x :<: y) = (:<:) <$> makeShifter x <*> makeShifter y
makeShifter (Forall v x) = Forall v <$> makeShifter x
makeShifter (Exists v x) = Exists v <$> makeShifter x
makeShifter (Reset x) = pure (Reset x)
makeShifter (Shift x) = shift x
makeShifter (Continue x) = pure (Continue x)

evalShifter :: Shifter Expr -> ([Expr] -> Expr, [Expr])
evalShifter r = evalState (runShifter r) 0




reset :: Expr -> Expr
reset x =
  let (m,shifts) = evalShifter (makeShifter x)
  in if null shifts
     then m []
     else let ks = forM shifts $ \r ->
                     cont (runReader (makeContinuer r))
          in reset (runCont ks m)



decontinuize :: Expr -> Expr
decontinuize (x :&&: y) = decontinuize x :&&: decontinuize y
decontinuize (Not x) = Not (decontinuize x)
decontinuize (Var v) = Var v
decontinuize (x :<: y) = decontinuize x :<: decontinuize y
decontinuize (Forall v x) = Forall v (decontinuize x)
decontinuize (Exists v x) = Exists v (decontinuize x)
decontinuize (Reset x) = reset (decontinuize x)
decontinuize (Shift x) = Shift (decontinuize x)
decontinuize (Continue x) = Continue (decontinuize x)



main :: IO ()
main = do putStrLn "Example 1"
          print example
          print (continuedExample id)
          print (continuedExample $ \s -> Var "q" :<: s)
          
          putStrLn "\nExample 2"
          print example2
          print (decontinuize example2)
          
          putStrLn "\nExample 3"
          print example3
          print (decontinuize example3)
  where
    example :: Expr
    example = Continue (Var "x") :&&: Continue (Var "y")
    
    continuedExample :: (Expr -> Expr) -> Expr
    continuedExample = runReader (makeContinuer example)
    
    -- two shift points under a reset
    example2 :: Expr
    example2 = Reset $ (Shift $ Forall "x" (Continue $ Var "x")) :<: (Shift $ Exists "y" (Continue $ Var "y"))
    
    -- multiple continues in a shift
    example3 :: Expr
    example3 = Reset $ Not (Shift $ (Continue $ Var "p") :&&: (Continue $ Var "q"))