{-# LANGUAGE PatternGuards, KindSignatures #-}
{-# LANGUAGE ExistentialQuantification, RankNTypes, ImpredicativeTypes #-}

-- This file is the CPS version of CCExc.hs, implementing the identical
-- interface
--
-- <http://okmij.org/ftp/continuations/implementations.html#CC-monads>
--
-- Monad transformer for multi-prompt delimited control
-- It implements the superset of the interface described in
--
-- > A Monadic Framework for Delimited Continuations
-- > R. Kent Dybvig, Simon Peyton Jones, and Amr Sabry
-- > JFP, v17, N6, pp. 687--730, 2007.
-- > http://www.cs.indiana.edu/cgi-bin/techreports/TRNNN.cgi?trnum=TR615
--
-- The first main difference is the use of generalized prompts, which
-- do not have to be created with new_prompt and therefore can be defined
-- at top level. That removes one of the main practical drawbacks of
-- Dybvig et al implementations: the necessity to carry around the prompts
-- throughout all the code.
--
-- The delimited continuation monad is parameterized by the flavor
-- of generalized prompts. The end of this code defines several flavors;
-- the library users may define their own. User-defined flavors are 
-- especially useful when user's code uses a small closed set of answer-types. 
-- Flavors PP and PD below are more general, assuming the set of possible
-- answer-types is open and Typeable. If the user wishes to create several
-- distinct prompts with the same answer-types, the user should use
-- the flavor of prompts accepting an integral prompt identifier, such as PD.
-- Prompts of the flavor PD correspond to the prompts in Dybvig, Peyton Jones,
-- Sabry framework. If the user wishes to generate unique prompts, the user
-- should arrange himself for the generation of unique integers
-- (using a state monad, for example). On the other hand, the user
-- can differentiate answer-types using `newtype.' The latter can
-- only produce the set of distinct prompts that is fixed at run-time.
-- Sometimes that is sufficient. There is not need to create a gensym
-- monad then.
--
-- See CCExc.hs for further comments about the implementation

module Control.CCCxe (
              CC,                       -- Types
              SubCont,
              CCT,
              Prompt,

              -- Basic delimited control operations
              pushPrompt,
              takeSubCont,
              pushSubCont,
              runCC,

              -- Useful derived operations
              abortP,
              shiftP,
              shift0P,
              controlP,

              -- Pre-defined prompt flavors
              PS, ps,
              P2, p2L, p2R,
              PP, pp,
              PM, pm,
              PD, newPrompt,
              as_prompt_type
              ) where

import Control.Monad.Trans
import Data.Typeable                    -- for prompts of the flavor PP, PD

-- | Delimited-continuation monad transformer
-- It is parameterized by the prompt flavor p
-- The first argument is the regular (success) continuation,
-- the second argument is the bubble, or a resumable exception
newtype CC p m a = 
    CC{unCC:: forall w. (a -> m w) -> 
                        (forall x. SubCont p m x a -> p m x  -> m w) -> 
                        m w}

-- | The captured sub-continuation
type SubCont p m a b = CC p m a -> CC p m b

-- | The type of control operator's body
type CCT p m a w = SubCont p m a w -> CC p m w

-- | Generalized prompts for the answer-type w: an injection-projection pair
type Prompt p m w = 
    (forall x. CCT p m x w -> p m x,
     forall x. p m x -> Maybe (CCT p m x w))


-- --------------------------------------------------------------------
-- | CC monad: general monadic operations
--
instance Monad m => Monad (CC p m) where
    return x = CC $ \ki kd -> ki x

    m >>= f = CC $ \ki kd -> unCC m 
                              (\a -> unCC (f a) ki kd)
                              (\ctx -> kd (\x -> ctx x >>= f))

instance MonadTrans (CC p) where
    lift m = CC $ \ki kd -> m >>= ki

instance MonadIO m => MonadIO (CC p m) where
    liftIO = lift . liftIO

-- --------------------------------------------------------------------
-- | Basic Operations of the delimited control interface
--
pushPrompt :: Monad m =>
              Prompt p m w -> CC p m w -> CC p m w
pushPrompt p@(_,proj) body = CC $ \ki kd -> 
 let kd' ctx body | Just b <- proj body  = unCC (b ctx) ki kd
     kd' ctx body = kd (\x -> pushPrompt p (ctx x)) body
 in unCC body ki kd'


-- | Create the initial bubble
takeSubCont :: Monad m =>
               Prompt p m w -> CCT p m x w -> CC p m x
takeSubCont p@(inj,_) body = CC $ \ki kd -> kd id (inj body)

-- | Apply the captured continuation
pushSubCont :: Monad m => SubCont p m a b -> CC p m a -> CC p m b
pushSubCont = ($)

runCC :: Monad m => CC (p :: (* -> *) -> * -> *) m a -> m a
runCC m = unCC m return err
 where
 err = error "Escaping bubble: you have forgotten pushPrompt"


-- --------------------------------------------------------------------
-- | Useful derived operations
--
abortP :: Monad m => 
          Prompt p m w -> CC p m w -> CC p m any
abortP p e = takeSubCont p (\_ -> e)

shiftP :: Monad m => 
          Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
shiftP p f = takeSubCont p $ \sk -> 
               pushPrompt p (f (\c -> 
                  pushPrompt p (pushSubCont sk (return c))))

shift0P :: Monad m => 
          Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
shift0P p f = takeSubCont p $ \sk -> 
               f (\c -> 
                  pushPrompt p (pushSubCont sk (return c)))

controlP :: Monad m => 
          Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
controlP p f = takeSubCont p $ \sk -> 
               pushPrompt p (f (\c -> 
                  pushSubCont sk (return c)))

-- --------------------------------------------------------------------
-- Prompt flavors

-- | The extreme case: prompts for the single answer-type w.
-- The monad (CC PS) then is the monad for regular (single-prompt) 
-- delimited continuations
newtype PS w m x = PS (CCT (PS  w) m x w)

-- | There is only one generalized prompt of the flavor PS for a
-- given answer-type w. It is defined below
ps :: Prompt (PS w) m w
ps = (inj, prj)
 where
 inj = PS
 prj (PS x) = Just x

-- | Prompts for the closed set of answer-types
-- The following prompt flavor P2, for two answer-types w1 and w2,
-- is given as an example. Typically, a programmer would define their
-- own variant data type with variants for the answer-types that occur
-- in their program.
--
newtype P2 w1 w2 m x = 
  P2 (Either (CCT (P2 w1 w2) m x w1) (CCT (P2 w1 w2) m x w2))


-- | There are two generalized prompts of the flavor P2"
p2L :: Prompt (P2 w1 w2) m w1
p2L = (inj, prj)
 where
 inj = P2 . Left
 prj (P2 (Left x)) = Just x
 prj _ = Nothing

p2R :: Prompt (P2 w1 w2) m w2
p2R = (inj, prj)
 where
 inj = P2 . Right
 prj (P2 (Right x)) = Just x
 prj _ = Nothing


-- | Prompts for the open set of answer-types
--
data PP m x = forall w. Typeable w => PP (CCT PP m x w)

-- | We need to wrap the type alias CCT into a newtype. Otherwise, gcast
-- doesn't work. We can't treat (CCT p m a w) as a an application of
-- the `type constructor' (CCT p m a) to the type w: type aliases can't 
-- be partially applied. But we can treat the type (NCCT p m a w) that way.
newtype NCCT p m a w = NCCT{unNCCT :: CCT p m a w}

pp :: Typeable w => Prompt PP m w
pp = (inj, prj)
 where
 inj = PP
 prj (PP c) = maybe Nothing (Just . unNCCT) (gcast (NCCT c))

-- | The same as PP but with the phantom parameter c
-- The parameter is useful to statically enforce various constrains
-- (statically pass some information between shift and reset)
-- The prompt PP is too `dynamic': all errors are detected dynamically
-- See Generator2.hs for an example
data PM c m x = forall w. Typeable w => PM (CCT (PM c) m x w)

pm :: Typeable w => Prompt (PM c) m w
pm = (inj, prj)
 where
 inj = PM
 prj (PM c) = maybe Nothing (Just . unNCCT) (gcast (NCCT c))

-- | Open set of answer types, with an additional distinction (given by
-- integer identifiers)
-- This prompt flavor corresponds to the prompts in the Dybvig, Peyton-Jones,
-- Sabry framework (modulo the Typeable constraint).
--
data PD m x = forall w. Typeable w => PD Int (CCT PD m x w)

newPrompt :: Typeable w => Int -> Prompt PD m w
newPrompt mark = (inj, prj)
 where
 inj = PD mark
 prj (PD mark' c) | mark' == mark, 
                    Just (NCCT x) <- gcast (NCCT c) = Just x
 prj _ = Nothing

-- | It is often helpful, for clarity of error messages, to specify the 
-- answer-type associated with the prompt explicitly (rather than relying 
-- on the type inference to figure that out). The following function
-- is useful for that purpose.
as_prompt_type :: Prompt p m w -> w -> Prompt p m w
as_prompt_type = const