diff options
Diffstat (limited to 'testsuite/tests/esc/TestData.hs')
-rw-r--r-- | testsuite/tests/esc/TestData.hs | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/testsuite/tests/esc/TestData.hs b/testsuite/tests/esc/TestData.hs new file mode 100644 index 0000000000..045f3c96c0 --- /dev/null +++ b/testsuite/tests/esc/TestData.hs @@ -0,0 +1,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) |