Commit b28f70bf authored by nx200's avatar nx200

added contract synonym test case

parent d3fb9859
test('head', normal, compile, ['-fesc -ddump-esc'])
test('sum', normal, compile, ['-fesc -ddump-esc'])
test('f', normal, compile, ['-fesc -ddump-esc'])
test('synonym', normal, compile, ['-fesc -ddump-esc'])
test('dataA', normal, compile, ['-fesc -ddump-esc'])
......@@ -6,10 +6,10 @@ module Head where
and1 True x = x
and1 False x = False
{-# CONTRACT head1 :: {xs | not (null xs)} -> any #-}
{-# CONTRACT head1 :: {xs | not (null xs)} -> {r | not (null r)} #-}
-- {-# CONTRACT head1 :: {xs | not1 (null1 xs)} -> {r | r > 0} #-}
head1 :: [Int] -> Int
head1 (x:xs) = x
head1 :: [Int] -> [Int]
head1 (x:xs) = [x]
not1 True = False
not1 False = True
......@@ -17,9 +17,15 @@ not1 False = True
null1 [] = True
null1 xs = False
res1 = and1 True True
{-# CONTRACT f :: {x | x > 0 && x < 5} -> any #-}
f :: Int -> Int
f x = x + 1
{-# CONTRACT res2 :: any #-}
res2 = head1 [5]
res3 = head1 [6]
res4 = head1 []
......@@ -5,7 +5,7 @@ module Sum where
-- {-# CONTRACT f :: x:{y | y > 0} -> {y | y > 0} -> {r | r == x + 1} #-}
-- {-# CONTRACT f :: any -> {y | y > 0} #-}
-- {-# CONTRACT f :: {y | y > 0} -> any #-}
{-# CONTRACT f :: {y | y > 0} -> {r | r > 0} #-}
{-# CONTRACT f :: {y | y > 0} -> {r | r > 1} #-}
f :: Int -> Int
f x = x + 1
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment