blob: 045f3c96c05592e5fc6a7b5723592e7b1fb18b77 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
module TestData where
data A = A1 | A2
-- If we put noA2 and yesA2 here, they are out of scope
-- in ESC's eyes. i.e. they are not in EscEnv.vals
{-
noA2 A1 = True
noA2 A2 = False
yesA2 A1 = False
yesA2 A2 = True
-}
{-# CONTRACT h1 :: {x | noA2 x} -> {r | yesA2 r} #-}
h1 :: A -> A
h1 A1 = A2
g1 :: A -> A
g1 A1 = A1
g1 A2 = A1
{-# CONTRACT h2 :: {x | not1 (noA2 x)} -> {r | not1 (yesA2 r)} #-}
h2 :: A -> A
h2 A2 = A1
noA2 A1 = True
noA2 A2 = False
yesA2 A1 = False
yesA2 A2 = True
not1 True = False
not1 False = True
test = h1 (g1 A2)
|
