testsuite/tests/esc/F123.hs


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

module F123 where


data A = A1 | A2
data B = B1 | B2

{-# CONTRACT h1 :: {x | noA2 x} -> {r | yesA2 r} #-}
h1 :: A -> A
h1 A1 = A2


noA2 A1 = True
noA2 A2 = False

yesA2 A1 = False
yesA2 A2 = True

f3 x y =  case y of
	     B1 -> f2 x y

f2 x y = case y of
            B1 -> f1 x

f1 x = h1 A2