{-#  OPTIONS -fglasgow-exts  #-}

module EagerContract where

infixr :->

data Contract :: * -> * where
  Prop    ::  (a -> Bool) -> Contract a
  Id      ::  Contract a
  (:->)   ::  Contract a -> Contract b -> Contract (a -> b)
  Pair    ::  Contract a -> Contract b -> Contract (a, b)
  List    ::  Contract a -> Contract [a]


assert ::  Contract a -> a -> a
assert c = \ a -> let (b, a') = assert' c a in a'

assert' :: Contract a -> a -> (Bool, a)
assert' (Prop p)      = \ a -> let b = p a in 
			       (b, if b then a else error "assertion failed")
assert' Id	      = \ a -> (True, a)
assert' (c1 :-> c2)   = \ f -> (True, \ x -> 
				      let (b', x') = assert' c1 x in
				      if b' then
					 let (b'', x'') = assert' c2 (f x') in
					 x''
				      else 
				         x' `seq` error "precondition failed")
assert' (Pair c1 c2)  = \ (x1, x2) -> let (b1', x1') = assert' c1 x1
					  (b2', x2') = assert' c2 x2
					  r = if not b1' then x1' `seq` undefined else 
					      if not b2' then x2' `seq` undefined else
					      (x1', x2')
				      in  (b1' && b2', r)
assert' (List c)      = \ xs -> let bxs' = map (assert' c) xs 
				    g ((b,x) : bxs) h =
				      if not b then x `seq` undefined else
				      g bxs (h . (x:))
				    g [] h = 
				      h []
				in  (and (map fst bxs'), g bxs' id)

-- 

simplify :: Contract a -> Contract a
simplify (Prop p) = (Prop p)
simplify Id = Id
simplify (c1 :-> c2)  = let sc1 = simplify c1
			    sc2 = simplify c2
		        in  case (sc1, sc2) of
			      (Id, Id) -> Id
			      _ -> (sc1 :-> sc2)
simplify (Pair c1 c2) = let sc1 = simplify c1
			    sc2 = simplify c2
		        in  case (sc1, sc2) of
			      (Id, Id) -> Id
			      _ -> Pair sc1 sc2
simplify (List c1)    = let sc1 = simplify c1
			in  case sc1 of 
			      Id -> Id
			      _ -> List sc1

--
-- Examples
--

fC = Prop (\x -> x == 0) :-> Prop (\_ -> True)
f = \_ -> 1