summaryrefslogtreecommitdiff
path: root/testsuite/tests/esc/TestData.hs
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/esc/TestData.hs')
-rw-r--r--testsuite/tests/esc/TestData.hs37
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)