module TwiceM where {-@ LIQUID "--short-names" @-} import RIO {-@ appM :: forall
Bool, post :: World -> b -> World -> Bool>. (a -> RIOb) -> a -> RIOb @-} appM :: (a -> RIO b) -> a -> RIO b appM f x = f x {-@ twiceM :: forall < pre :: World -> Bool , post1 :: World -> a -> World -> Bool , post :: World -> a -> World -> Bool>. {w ::World, x::a|- World<: World } {w1::World, y::a, w2::World, w20::{v:World | v = w2}, x::a |- World<: World } (b -> RIO a) -> b -> RIOa @-} twiceM :: (b -> RIO a) -> b -> RIO a twiceM f w = let (RIO g) = f w in RIO $ \x -> case g x of {(y, s) -> let ff = \_ -> f w in (runState (ff y)) s} {-@ measure counter :: World -> Int @-} {-@ incr :: RIO <{\x -> counter x >= 0}, {\w1 x w2 -> counter w2 = counter w1 + 1}> Nat @-} incr :: RIO Int incr = undefined {-@ incr2 :: RIO <{\x -> counter x >= 0}, {\w1 x w2 -> counter w2 = counter w1 + 42}> Nat @-} incr2 :: RIO Int incr2 = twiceM (\_ -> incr) 0