content: {-@ LIQUID "--no-termination" @-}
  module Until where
  
  import Prelude hiding (until)
  
  {-@ until :: forall <p :: a -> Prop, i :: a -> Prop>.
               (a:a<i> -> {v:Bool | Prop v <=> papp1 p a})
            -> ({v:a<i> | not (papp1 p v)} -> a<i>)
            -> a<i>
            -> a<p>
    @-}
  until :: (a -> Bool) -> (a -> a) -> a -> a
  until p f = go
    where
      go x | p x          = x
           | otherwise    = go (f x)
  
  {-@ predicate Btwn Lo N Hi = Lo <= N && N < Hi @-}
  {-@ predicate Uint8 N = Btwn 0 N 256 @-}
  
  
  {-@ assume addUint8 :: x:{Int | Uint8 x} -> y:{Int | Uint8 y && Uint8 (x+y)}
                      -> {v:Int | Uint8 v && v = x + y}
    @-}
  addUint8 :: Int -> Int -> Int
  addUint8 = (+)
  
  {-@ ten :: {v:Int | Uint8 v && v >= 10} @-}
  ten = until (\x -> gt10 x) (\x -> add1 x) 0 
  
  {-@ gt10 :: x:Int -> {v:Bool | Prop v <=> x >= 10} @-}
  gt10 :: Int -> Bool
  gt10 x = x >= 10
  
  {-@ add1 :: x:{Int | Btwn 0 x 255} -> {v:Int | Uint8 v && v = x +1} @-}
  add1 x = addUint8 x 1
  
  
  {-@ untilMono :: (x:{Int | Uint8 x && x <= 10} -> {v:Bool | Prop v <=> x >= 10})
                -> ({v:Int | Uint8 v && v < 10} -> {v:Int | Uint8 v && v <= 10})
                -> {v:Int | Uint8 v && v <= 10}
                -> {v:Int | Uint8 v && v >= 10}
    @-}
  untilMono :: (Int -> Bool) -> (Int -> Int) -> Int -> Int
  -- untilMono p f x = until p f x
  untilMono p f = go
    where
      go x | p x          = x
           | otherwise    = go (f x)
  
  {-@ tenMono :: {v:Int | Uint8 v && v >= 10} @-}
  tenMono = untilMono gt10 add1 0 
  