module Compose where data ST s a = ST {runState :: s -> (a,s)} {-@ data ST s a

Bool, q :: s -> s -> Bool, r :: s -> a -> Bool> = ST (runState :: x:s

-> (a, s)) @-} {-@ runState :: forall

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

-> (a, s) @-} {- cmp :: forall < pref :: s -> Bool, postf :: s -> s -> Bool , pre :: s -> Bool, postg :: s -> s -> Bool , post :: s -> s -> Bool , rg :: s -> a -> Bool , rf :: s -> b -> Bool , r :: s -> b -> Bool >. {xx::s

, w::s |- s <: s}
       {ww::s
 |- s <: s}
       (ST  s a)
    -> (ST  s b)
    -> (ST  s b)
@-}

cmp :: (ST s a)
    -> (ST s b)
    -> (ST s b)

cmp (ST g) (ST f) = ST (\x -> case g x of {(_, s) -> f s})    

{-@ 
bind :: forall < pref :: s -> Bool, postf :: s -> s -> Bool
              , pre  :: s -> Bool, postg :: s -> s -> Bool
              , post :: s -> s -> Bool
              , rg   :: s -> a -> Bool
              , rf   :: s -> b -> Bool
              , r    :: s -> b -> Bool
              , pref0 :: a -> Bool 
              >. 
       {x::s
 |- a <: a}      
       {x::s
, y::s |- b <: b}
       {xx::s
, w::s |- s <: s}
       {ww::s
 |- s <: s}
       (ST  s a)
    -> (a -> ST  s b)
    -> (ST  s b)
@-}

bind :: (ST s a)
    -> (a -> ST s b)
    -> (ST s b)

bind (ST g) f = ST (\x -> case g x of {(y, s) -> (runState (f y)) s})    

{-@ incr :: ST <{\x -> x >= 0}, {\x v -> v = x + 1}, {\x v -> v = x}>  Nat Nat @-}
incr :: ST Int Int
incr = ST $ \x ->  (x, x + 1)

{-@ incr2 :: ST <{\x -> x >= 0}, {\x v -> v = x + 2}, {\x v -> v = x + 1}>  Nat Nat @-}
incr2 :: ST Int Int
incr2 = bind incr (\_ -> incr)


{-@ incr3 :: ST <{\x -> x >= 0}, {\x v -> v = x + 3}, {\x v -> v = x + 2}>  Nat Nat @-}
incr3 :: ST Int Int
incr3 = bind (bind incr (\_ -> incr)) (\_ -> incr)


foo :: (Int, Int)
{-@ foo :: ({v:Nat |  v = 2}, {v:Nat |  v = 3}) @-}
foo = (runState incr3) 0