content: module WhileTest where
  
  {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--short-names" @-}
  {-@ LIQUID "--no-pattern-inline" @-}
  
  import RIO
  import WhileM
  
  -------------------------------------------------------------------------------
  ----------------------------- whileM client -----------------------------------
  -------------------------------------------------------------------------------
  {-@ measure counter :: World -> Int @-}
  
  
  whileTest       :: RIO ()
  {-@ whileTest   :: RIO <{\x -> true}, {\w1 x w2 -> counter w2 <= 0}> () @-}
  whileTest       = whileM (checkGtZero) (decrM)
    where
      checkGtZero = do {x <- get; return $ x > 0}
  
  
  whileTest1       :: RIO ()
  {-@ whileTest1   :: RIO <{\x -> counter x >= 0}, {\w1 x w2 -> counter w2 == 0}> () @-}
  whileTest1       = 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 = undefined
  
  {-@ qual2 :: RIO <{\x -> true}, {\w1 b w2 -> b <=> counter w2 /= 0}> Bool @-}
  qual2 :: RIO Bool
  qual2 = undefined
  