module SemiEagerExamples where

import SemiEagerContract

ordered_pair :: Contract (Integer, Integer)
ordered_pair = 
  Prop (\ x -> case x of (x1,x2) -> (x1 < x2))

arg_is_zero :: Contract (Integer -> a)
arg_is_zero =
  let pre  = Prop (\ x -> (x == 0))
      post = Prop (\ x -> True)
  in (:->) pre post


ex1 :: Integer -> Integer
ex1 = assert arg_is_zero (\x -> 1)

not_terminating :: Integer -> Integer
not_terminating x = not_terminating x + 1

ex2 :: Integer
ex2 = (\ x -> case x of (x1,x2) -> x1) (assert ordered_pair (5, (not_terminating 1)))