{-----------------------------------------------------------------------------
    A small language with both a choice operationa  orElse  and  callCC
    
    In response to
    http://www.haskell.org/pipermail/haskell-cafe/2010-June/079029.html
------------------------------------------------------------------------------}
{-# LANGUAGE GADTs, RankNTypes, TypeSynonymInstances, FlexibleInstances #-}
import Control.Monad.Identity
import Control.Monad

import Control.Monad.Operational

{-----------------------------------------------------------------------------
    Language definition
------------------------------------------------------------------------------}
    -- primitive instructions
data Instruction r a where
    CallCC :: ((forall b. a -> M r b) -> M r a) -> Instruction r a
    Jump   :: M r r -> Instruction r a
    OrElse :: M r a -> M r a -> Instruction r a
    MZero  :: Instruction r a

jump   = singleton . Jump -- not exported, needed to implement  callCC
callCC = singleton . CallCC
orElse m n = singleton (OrElse m n)

instance MonadPlus (ProgramT (Instruction r) Identity) where
    mzero = singleton MZero
    mplus = undefined -- ignore

    -- main type
type M r a = Program (Instruction r) a

    -- examples
example1, example2 :: M Int Int
example1 = ((callCC (\k -> k 0) >> mzero) `orElse` return 2) >>= return . (+3)
example2 = (mzero `orElse` return 2) >>= return . (+3)

{-----------------------------------------------------------------------------
    Interpreter
------------------------------------------------------------------------------}
    -- global interpreter
interpret :: M r r -> Maybe r
interpret m = case (eval return . view) m of
    JumpR mr  -> interpret mr
    ReturnR a -> Just a
    MZeroR    -> Nothing

    -- helper type for the interpreter
data Result r a where
    ReturnR :: a -> Result r a
    MZeroR  :: Result r a
    JumpR   :: M r r -> Result r a

    -- local interpreter
    -- Passes around the current continuation  kk  so that we can 
    -- implement  callCC , but never continues evaluation with  kk
eval :: (a -> M r r) -> ProgramView (Instruction r) a -> Result r a
eval kk (Return a)          = ReturnR a
eval kk (CallCC f   :>>= k) = (eval kk . view) $ f (jump . kk') >>= k
    where kk' = k >=> kk
eval kk (OrElse n m :>>= k) = case (eval kk' . view) n of
        ReturnR a -> (eval kk . view) (k a)
        JumpR  mr -> JumpR mr
        MZeroR    -> (eval kk . view) (m >>= k)
    where kk' = k >=> kk
eval kk (MZero      :>>= k) = MZeroR
eval kk (Jump mr    :>>= k) = JumpR mr