{-#  OPTIONS -fglasgow-exts  #-}

-- contracts by Hinze et al. as shown in their paper
-- original source (including blame assignment):
-- http://people.cs.uu.nl/andres/Contracts.html

module SemiEagerContract where

infixr :->

data Contract :: * -> * where
  Prop    ::  (a -> Bool) -> Contract a
  Id      ::  Contract a
  (:->)   ::  Contract a -> Contract b -> Contract (a -> b)
  (:=>)   ::  Contract a -> Contract b -> Contract (a -> b)
  List    ::  Contract a -> Contract [a]
  SList   ::  Contract a -> Contract [a]
  And     ::  Contract a -> Contract a -> Contract a


assert ::  Contract a -> a -> a
assert (Prop p)     =  \ a -> if p a then a else error "assertion failed"
assert Id           =  id
assert (c1 :-> c2)  =  \ f -> assert c2 . f . assert c1
assert (c1 :=> c2)  =  \ f x -> x `seq` (assert c2 . f . assert c1) x
assert (List c)     =  map (assert c)
assert (SList c)    =  \ xs -> eval xs `seq` map (assert c) xs
assert (And c1 c2)  =  \ a -> (assert c2 . assert c1) a 


eval []        =  []
eval (a : as)  =  a `seq` eval as

{-
evens []              =  []
evens [a]             =  [a]
evens (a1 : a2 : as)  =  evens as

assert (Id :-> Id) (const 1) undefined
assert (Id :=> Id) (const 1) undefined

assert (Id :=> Id) (sum . evens) [1, undefined]
assert (SList Id :=> Id) (sum . evens) [1, undefined]
-}

--
-- Examples
--

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