{-# LANGUAGE RankNTypes, FlexibleContexts, GADTs, KindSignatures, TypeFamilies #-}
module RefStepwise where

import Control.Monad
import Control.Monad.Cont
import Control.Monad.Error
import Control.Monad.Trans
import Control.Applicative

data family Op   i  :: * -> *
type family Inp  o  :: *
type family Out  o  :: *


data S :: * -> * -> * -> (* -> *) -> * -> * where
  Return  :: a -> S q r i m a
  Bind    :: S q r i m a -> P q r i m a b -> S q r i m b
  Fail    :: String -> S q r i m a
  Act     :: Op i o -> Inp o -> S q r i m (Out o)
  Lift    :: m a -> S q r i m a
  Ahead   :: ((a -> S q r i m r) -> S q r i m r) -> S q r i m a

data P :: * -> * -> * -> (* -> *) -> * -> * -> * where
  Top       :: Seal r a b -> P a r i m a b
  Next      :: P q r i m a a
  Pending   :: (a -> S q r i m b) -> P q r i m b c -> P q r i m a c

data Seal :: * -> * -> * -> * where
  Root  :: Seal r a a
  More  :: Seal r a r

data R :: * -> * -> * -> (* -> *) -> * where
  Done    :: Seal r a b -> q -> R q r i m
  Failed  :: String -> R q r i m
  Await   :: Seal r a b -> ((q -> S q r i m r) -> S q r i m r) -> R q r i m
  Action  :: Op i o -> Inp o -> (S q r i m (Out o) ->  S q r i m a) -> R q r i m

bindS :: S q r i m a -> (a -> S q r i m b) -> S q r i m b
p `bindS` q = Bind p (Pending q Next)

begin :: S a r i m a -> S a r i m a
begin m = Bind m (Top Root)

one :: Monad m => S q r i m a -> m (R q r i m)
one (Bind m p)    = reduce m p
one (Fail s)      = return (Failed s)

reduce :: Monad m => S q r i m a -> P q r i m a b -> m (R q r i m)
reduce m             Next           = one m
reduce (Return v)    p              = beta p v
reduce (Ahead f)     (Pending g p)  = one $ f $ \v -> Bind (g v) (mkPending p)
reduce (Ahead f)     (Top s)        = return (Await s f)
reduce (Lift m)      p              = m >>= beta p
reduce (Act op inp)  p              = return $ Action op inp $ \out -> Bind out p
reduce (Bind m p)    p'             = reduce m (push p p')

beta :: Monad m => P q r i m a b -> a-> m (R q r i m)
beta (Pending f p)  v  = reduce (f v) p
beta (Top s)        v  = return (Done s v)

mkPending :: P q r i m b c -> P q r i m b r
mkPending (Top _)        = Top More
mkPending (Pending m p)  = Pending m (mkPending p)

push :: P q r i m a b -> P q r i m b c -> P q r i m a c
push Next           p   = p
push (Pending f p)  p'  = Pending f (push p p')

{-
reduce :: Monad m => S q r i m a -> P q r i m a b -> m (R q r i m b)
reduce (Del o i)     p             = return (Action o i (\m -> Bind m p))
reduce m             Root          = one m
reduce (Fail s)      _             = return (Failed s)
reduce (Return v)    (Parent f p)  = reduce (f v) p
reduce (Lift m)      (Parent f p)  = m >>= \v -> reduce (f v) p
reduce (Ahead f)     (Parent g p)  = one $ Escape $ f $ \a -> Ahead $ \k -> {- Bind (g a) p -} undefined `bindS` k  -- prove q ~ b
reduce (Escape m)    _             = one (Escape m)
reduce (Bind m p)    p'            = reduce m (push p p')

instance Monad (S q r i m) where
  return  = Return
  (>>=)   = bindS
  fail    = Fail

instance MonadTrans (S q r i) where
  lift      = Lift

instance Functor (S q r i m) where
  fmap f m  = m >>= return . f

ahead :: ((q -> S q r i m r) -> S q r i m r) -> S q r i m a
ahead = Ahead
-}



{-
data Back = Back
instance Error Back where
  noMsg    = Back
  strMsg _ = Back

type BackT r m a = ContT r (ErrorT Back m) a

next :: Monad m => BackT r m a
next = lift $ throwError Back

alt :: Monad m => BackT a m a -> BackT a m a -> BackT r m a
alt p q = ContT $ \c -> catchError (runContT p return) (const (runContT q return)) >>= c

ahead :: Monad m => ((a -> ContT r m r) -> ContT r m r) -> ContT r m a
ahead f = ContT (\c -> runContT (f (\a -> ContT (\k -> c a >>= k))) return)

cut :: Monad m => BackT a m a -> BackT k m a
cut p = ContT $ \c -> runContT p return >>= c

run :: Monad m => BackT a m a -> m a
run m = do r <- runErrorT (runContT m return)
           case r of
             Left _  -> fail "backtracking alternatives exhausted"
             Right a -> return a

ex2 :: IO Int
ex2 = run $ do
        x <- ahead (\k -> (return 1 >>= k) `alt` (return 2 >>= k))
        if (x == 1) then next else return ()
        next `alt` return x
-}