module StateLib ( returnST -- :: a -> ST a s , bindST -- :: ST a s -> (a -> ST b s) -> ST b s , ST(..) ) where import Prelude hiding (snd, fst) data ST a s = S (s -> (a, s)) {-@ data ST a s
 Bool, post :: a -> s -> Bool> 
       = S (ys::(x:s
 -> ((a, s))))
  @-}

{-@ returnST :: forall 
 Bool, post :: a -> s -> Bool>.
               xState:a 
           -> ST <{v:s| true}, post> a s
  @-}
returnST :: a -> ST a s
returnST x = S $ \s -> (x, s)


{-@ bindST :: forall  Bool, qbind :: a -> s -> Bool, rbind :: b -> s -> Bool>.
            ST  a s 
         -> (xbind:a -> ST <{v:s | true}, rbind> b s) 
         -> ST  b s
 @-}
bindST :: ST a s -> (a -> ST b s) -> ST b s
bindST (S m) k = S $ \s -> let (a, s') = m s in apply (k a) s'

{-@ apply :: forall 

Bool, q :: a -> s -> Bool>. ST a s -> s

-> (a, s) @-} apply :: ST a s -> s -> (a, s) apply (S f) s = f s