content: {-# OPTIONS -XRebindableSyntax #-}
  -- Haskell98!
  
  -- Tests of the do-notation for the parameterized monads
  -- We demonstrate a variable-type state `monadic' transformer
  -- and its phantom-type-state relative to enforce the locking protocol
  -- (a lock can be released only if it is being held, and acquired only
  -- if it is not being held)
  -- The tests are based on the code
  -- http://okmij.org/ftp/Computation/monads.html#param-monad
  
  -- Please search for DO-NOT-YET
  
  module DoParamM where
  
  import Prelude (const, String, ($), (.), Maybe(..),
                  Int, fromInteger, succ, pred, fromEnum, toEnum,
                  (+), Char, (==), Bool(..),
                  IO, getLine, putStrLn, read, show)
  import qualified Prelude
  import qualified Control.Monad.State as State
  import qualified Control.Monad.Identity as IdM
  
  -- A parameterized `monad'
  class Monadish m where
      return :: a -> m p p a
      fail   :: String -> m p p a
      (>>=)  :: m p q a -> (a -> m q r b) -> m p r b
  
  m1 >> m2 = m1 >>= (const m2)
  
  -- All regular monads are the instances of the parameterized monad
  
  newtype RegularM m p q a = RegularM{unRM :: m a}
  
  instance Prelude.Monad m => Monadish (RegularM m) where
      return = RegularM . Prelude.return
      fail   = RegularM . Prelude.fail
      m >>= f = RegularM ((Prelude.>>=) (unRM m) (unRM . f))
  
  -- As a warm-up, we write the regular State computation, with the same
  -- type of state throughout. We thus inject Monad.State into the
  -- parameterized monad
  
  test1 = State.runState (unRM c) (0::Int) where
           c = gget >>= (\v -> gput (succ v) >> return v)
           gget :: (State.MonadState s m) => RegularM m s s s
           gget = RegularM State.get
           gput :: (State.MonadState s m) => s -> RegularM m s s ()
           gput = RegularM . State.put
  -- (0,1)
  
  -- The same in the do-notation
  test1_do = State.runState (unRM c) (0::Int) where
           c = do
               v <- gget
               gput (succ v)
               return v
           gget :: (State.MonadState s m) => RegularM m s s s
           gget = RegularM State.get
           gput :: (State.MonadState s m) => s -> RegularM m s s ()
           gput = RegularM . State.put
  -- (0,1)
  
  
  -- Introduce the variable-type state (transformer)
  
  newtype VST m si so v = VST{runVST:: si -> m (so,v)}
  
  instance Prelude.Monad m => Monadish (VST m) where
    return x = VST (\si -> Prelude.return (si,x))
    fail x   = VST (\si -> Prelude.fail x)
    m >>= f  = VST (\si -> (Prelude.>>=) (runVST m si)
                                         (\ (sm,x) -> runVST (f x) sm))
  
  vsget :: Prelude.Monad m => VST m si si si
  vsget = VST (\si -> Prelude.return (si,si))
  vsput :: Prelude.Monad m => so -> VST m si so ()
  vsput x = VST (\si -> Prelude.return (x,()))
  
  
  -- Repeat test1 via VST: the type of the state is the same
  vsm1 () = vsget >>= (\v -> vsput (succ v) >> return v)
  
  -- The same with the do-notation
  vsm1_do () = do
               v <- vsget
               vsput (succ v)
               return v
  
  {-
   *DoParamM> :t vsm1
   vsm1 :: (Monadish (VST m), IdM.Monad m, Prelude.Enum si) =>
           () -> VST m si si si
  -}
  
  test2 = IdM.runIdentity (runVST (vsm1 ()) (0::Int))
  -- (1,0)
  
  test2_do = IdM.runIdentity (runVST (vsm1_do ()) (0::Int))
  -- (1,0)
  
  
  -- Now, we vary the type of the state, from Int to a Char
  vsm2 () = vsget >>= (\v -> vsput ((toEnum (65+v))::Char) >>
                             vsget >>= \v' -> return (v,v'))
  
  {-
   *DoParamM> :t vsm2
   vsm2 :: (Monadish (VST m), IdM.Monad m) => () -> VST m Int Char (Int, Char)
  -}
  
  -- The same with the do-notation
   -- the following does not yet work
  vsm2_do () = do
               v <- vsget
               vsput ((toEnum (65+v))::Char)
               v' <- vsget
               return (v,v')
  
  test3 = IdM.runIdentity (runVST (vsm2 ()) (0::Int))
  -- ('A',(0,'A'))
  
  test3_do = IdM.runIdentity (runVST (vsm2_do ()) (0::Int))
  -- ('A',(0,'A'))
  
  {- The following is a deliberate error:
  
   DoParamM.hs:147:55:
      Couldn't match expected type `Int' against inferred type `Char'
      In the second argument of `(==)', namely `v''
      In the first argument of `return', namely `(v == v')'
      In the expression: return (v == v')
  
  vsm3 () = vsget >>= (\v -> vsput ((toEnum (65+v))::Char) >>
                             vsget >>= \v' -> return (v==v'))
   -}
  
  
   -- The following too must report a type error -- the expression
  --    return (v == v') must be flagged, rather than something else
  vsm3_do () = do
               v <- vsget
               vsput ((toEnum (65+v))::Char)
               v' <- vsget
               return (v==v')
  
  
  
  -- Try polymorphic recursion, over the state.
  -- crec1 invokes itself, and changes the type of the state from
  -- some si to Bool.
  crec1 :: (Prelude.Enum si, Prelude.Monad m) => VST m si si Int
  crec1 = vsget >>= (\s1 -> case fromEnum s1 of
                        0 -> return 0
                        1 -> vsput (pred s1) >> return 1
                        _ -> vsput True >>
                             crec1 >>= (\v ->
                               (vsput s1 >> -- restore state type to si
                                return (v + 10))))
  
  -- The same in the do-notation
  crec1_do :: (Prelude.Enum si, Prelude.Monad m) => VST m si si Int
  crec1_do = do
          s1 <- vsget
          case fromEnum s1 of
             0 -> return 0
             1 -> do {vsput (pred s1); return 1}
             _ -> do
                  vsput True
                  v <- crec1_do
                  vsput s1 -- restore state type to si
                  return (v + 10)
  
  
  test4 = IdM.runIdentity (runVST crec1 'a')
  -- ('a',11)
  
  test4_do = IdM.runIdentity (runVST crec1_do 'a')
  -- ('a',11)
  
  -- Another example, to illustrate locking and static reasoning about
  -- the locking state
  
  data Locked = Locked; data Unlocked = Unlocked
  newtype LIO p q a = LIO{unLIO::IO a}
  
  instance Monadish LIO where
    return  = LIO . Prelude.return
    m >>= f = LIO ((Prelude.>>=) (unLIO m) (unLIO . f))
  
  lput :: String -> LIO p p ()
  lput = LIO . putStrLn
  lget :: LIO p p String
  lget = LIO getLine
  
  -- In the real program, the following will execute actions to acquire
  -- or release the lock. Here, we just print out our intentions.
  lock :: LIO Unlocked Locked ()
  lock = LIO (putStrLn "Lock")
  
  unlock :: LIO Locked Unlocked ()
  unlock = LIO (putStrLn "UnLock")
  
  -- We should start in unlocked state, and finish in the same state
  runLIO :: LIO Unlocked Unlocked a -> IO a
  runLIO = unLIO
  
  -- User code
  
  tlock1 = lget >>=  (\l ->
           return (read l) >>= (\x ->
           lput (show (x+1))))
  
  tlock1r = runLIO tlock1
  
  -- the same in the do-notation
  tlock1_do = do
              l <- lget
              let x = read l
              lput (show (x+1))
  
  {-
    *VarStateM> :t tlock1
    tlock1 :: LIO p p ()
   Inferred type has the same input and output states and is polymorphic:
   tlock1 does not affect the state of the lock.
  -}
  
  
  tlock2 = lget >>= (\l ->
           lock >> (
           return (read l) >>= (\x ->
           lput (show (x+1)))))
  
  tlock2_do = do
              l <- lget
              lock
              let x = read l
              lput (show (x+1))
  
  {-
    *VarStateM> :t tlock2
    tlock2 :: LIO Unlocked Locked ()
  
  The inferred type says that the computation does the locking.
  -}
  
  tlock3 = tlock2 >> unlock
  tlock3r = runLIO tlock3
  
  {-
    *DoParamM> :t tlock3
    tlock3 :: LIO Unlocked Unlocked ()
  -}
  
  {-
  *DoParamM> tlock3r
  -- user input: 123
  Lock
  124
  UnLock
  -}
  
  tlock3_do = do {tlock2_do; unlock}
  tlock3r_do = runLIO tlock3_do
  
  
  -- An attempt to execute the following
  -- tlock4 = tlock2 >> tlock2
  
  {-
   gives a type error:
      Couldn't match expected type `Locked'
             against inferred type `Unlocked'
        Expected type: LIO Locked r b
        Inferred type: LIO Unlocked Locked ()
      In the expression: tlock2
      In a lambda abstraction: \ _ -> tlock2
  
  The error message correctly points out an error of acquiring an already
  held lock.
  -}
  
  -- The following too must be an error: with the SAME error message as above
  tlock4_do = do {tlock2_do; tlock2_do}
  
  -- Similarly, the following gives a type error because of an attempt
  -- to release a lock twice
  -- tlock4' = tlock2 >> unlock >> unlock
  {-
  DoParamM.hs:298:30:
      Couldn't match expected type `Unlocked'
             against inferred type `Locked'
        Expected type: LIO Unlocked r b
        Inferred type: LIO Locked Unlocked ()
      In the second argument of `(>>)', namely `unlock'
      In the expression: (tlock2 >> unlock) >> unlock
  -}
  
   -- The following too must be an error: with the SAME error message as above
  tlock4'_do = do {tlock2_do; unlock; unlock}
  
  