content: {-@ LIQUID "--expect-any-error" @-}
  module WhileM where
  
  {-@ LIQUID "--no-pattern-inline" @-}
  {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--short-names" @-}
  
  import RIO
  
  {-@
  whileM  :: forall < p   :: World -> Bool
                 , qc :: World -> Bool -> World -> Bool
                 , qe :: World -> () -> World -> Bool
                 , q  :: World -> () -> World -> Bool>.
         {x::(), s1::World<p>, b::{v:Bool | v}, s2::World<qc s1 b> |- World<qe s2 x> <: World<p>}
         {b::{v:Bool | v}, x2::(), s1::World<p>, s3::World |- World<q s3 x2> <: World<q s1 x2> }
         {b::{v:Bool | not (v)}, x2::(), s1::World<p> |- World<qc s1 b> <: World<q s1 x2> }
            RIO <p, qc> Bool
         -> RIO <{\v -> true}, qe> ()
         -> RIO <p, q> ()
  @-}
  whileM :: RIO Bool -> RIO () -> RIO ()
  whileM (RIO cond) (RIO e)
      = undefined
  {-
      = RIO $ \s1 -> case cond s1 of {(y, s2) ->
         if y
          then case e s2 of {(y2, s3) -> runState (whileM (RIO cond) (RIO e)) s3}
          else ((), s2)
        }
  -}
  
  -- First Condition Used to be:
  --        {x::(), s1::World<p>, b::{v:Bool | v}, s2::World<qc s1 b> |- World<qe s2 x> <: World<p>}
  --
  -- But it got simplify to fit it one line
  
  -------------------------------------------------------------------------------
  ----------------------------- whileM client -----------------------------------
  -------------------------------------------------------------------------------
  {-@ measure counter :: World -> Int @-}
  
  
  whileTestUnSafe       :: RIO ()
  {-@ whileTestUnSafe   :: RIO <{\x -> true}, {\w1 x w2 -> counter w2 == 0}> () @-}
  whileTestUnSafe       = whileM checkGtZero decrM
    where
      checkGtZero = do {x <- get; return $ x > 0}
  
  
  decrM :: RIO ()
  {-@ decrM :: RIO <{\x -> true}, {\w1 x w2 -> counter w2 = (counter w1) - 1}> () @-}
  decrM = undefined
  
  
  get :: RIO Int
  {-@ get :: forall <p :: World -> Bool >.
         RIO <p,\w x -> {v:World<p> | x = counter v && v == w}> Int @-}
  get = undefined
  
  {-@ qual99 :: n:Int -> RIO <{v:World | counter v >= 0}, \w1 b -> {v:World |  (b <=> n >= 0) && (b <=> counter v >= 0)}> {v:Bool | v <=> n >= 0} @-}
  qual99 :: Int -> RIO Bool
  qual99 = undefined -- \x -> return (x >= 0)
  
  {-@ qual3 :: m:Int ->  n:Int -> RIO <{v:World | counter v >= m}, \w1 b -> {v:World |  (b <=> n >= m) && (b <=> counter v >= m)}> {v:Bool | v <=> n >= m} @-}
  qual3 :: Int -> Int -> RIO Bool
  qual3 = undefined -- \x -> return (x >= 0)
  
  {-@ qual1 :: n:Int -> RIO <{v:World | counter v = n}, \w1 b -> {v:World |  (b <=> n > 0) && (b <=> counter v > 0)}> {v:Bool | v <=> n > 0} @-}
  qual1 :: Int -> RIO Bool
  qual1 = \x -> return (x > 0)
  
  {-@ qual2 :: RIO <{\x -> true}, {\w1 b w2 -> b <=> counter w2 /= 0}> Bool @-}
  qual2 :: RIO Bool
  qual2 = undefined
  