{-# 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