{-@ LIQUID "--noclasscheck" @-} module Compose where import Prelude hiding (Functor, Monad) 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) @-} class Functor f where fmap :: (a -> b) -> f a -> f b instance Functor (ST s) where fmap f (ST g) = ST (\s -> let (a, s') = g s in (f a, s')) class Functor m => Monad m where (>>) :: m a -> m b -> m b instance Monad (ST s) where {-@ instance Monad ST s where >> :: forall s a b < 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 >. {x::s

, y::s |- b <: b}
             {xx::s
, w::s |- s <: s}
             {ww::s
 |- s <: s}
             (ST  s a)
          -> (ST  s b)
          -> (ST  s b)
    @-}
  (ST g) >>  f = ST (\x -> case g x of {(y, s) -> (runState f) s})