State.hs

module State(StateM,runS,returnS,bindS,
             st,load{-,store-},update,inFst,inSnd) where

newtype StateM s a = S (s->(a,s))
runS (S m) = m
st = S

--instance Functor (StateM s) where
--  fmap f (S m) = S (apFst f . m)

instance Monad (StateM s) where
  return = returnS
  (>>=) = bindS

returnS x = st $ \ s -> (x,s)

m1 `bindS` xm2 = st $ uncurry' (runS.xm2) . runS m1
uncurry' f p = f (fst p) (snd p) -- lazier than Prelude.curry

load = st $ \ s -> (s,s)
--store s = S $ \ s' -> ((),s)
update f = st $ \ s -> ((),f s)

inFst m = st $ \ s -> let r = runS m (fst s) in (fst r,(snd r,snd s))
inSnd m = st $ \ s -> let r = runS m (snd s) in (fst r,(fst s,snd r))

--apFst f (x,y) = (f x,y)
--apSnd f (x,y) = (x,f y)

{-P:
{-
property RelatedResult R =
    {| res1,res2 | {fst res1}==={fst res2} /\ R {snd res1} {snd res2} |}

property MostlyStateIndependent R =
    {| m | All s1 . All s2 .
           R s1 s2 ==> RelatedResult R {runS m s1} {runS m s2} |}

-- Quantifying over relations is not allowed in P-Logic :-(

assert ReturnS = All x . All R . MostlyStateIndependent R {return x}

assert BindS =
  All m1 . All xm2 . All R .
    MostlyStateIndependent R m1 ==>
    (All x . MostlyStateIndependent R {xm2 x}) ==>
    MostlyStateIndependent R {m1 `bindS` xm2}
-}
-}