9 files changed, 181 insertions, 0 deletions
diff --git a/testsuite/tests/esc/F123.hs b/testsuite/tests/esc/F123.hs
new file mode 100644
index 0000000000..6aaad164cf
--- /dev/null
+++ b/testsuite/tests/esc/F123.hs
@@ -0,0 +1,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
+
+ 
+
diff --git a/testsuite/tests/esc/Makefile b/testsuite/tests/esc/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/esc/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/esc/Sum.hs b/testsuite/tests/esc/Sum.hs
new file mode 100644
index 0000000000..2b9ee29688
--- /dev/null
+++ b/testsuite/tests/esc/Sum.hs
@@ -0,0 +1,22 @@
+module Sum where
+
+{-- {-# SPECIALISE f :: Int -> Int #-}
+-- {-# CONTRACT f :: x:{y | y > 0} -> {r | r == x + 1} #-}
+-- {-# CONTRACT f :: x:{y | y > 0} -> {y | y > 0} -> {r | r == x + 1} #-}
+-- {-# CONTRACT f :: any -> {y | y > 0}  #-}
+-- {-# CONTRACT f :: {y | y > 0} -> _ #-}
+{-# CONTRACT inc :: {y | y > 0} -> {r | r > 1} #-}
+inc :: Int -> Int
+inc x = x + 1
+
+-}
+-- {-# CONTRACT sum2 :: x:{y | y > 0} -> {y | y > x} -> {r | r > 0} #-}
+-- {-# CONTRACT sum2 :: x:{y | y > 0} -> {y | y > x} -> _ #-}
+sum2 :: Int -> Int -> Int
+sum2 x y = x + y
+
+{-
+t1  = inc 5
+t2a = sum2 (inc 5) 2
+t2b = sum2 (inc 5) 6
+-}
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)
diff --git a/testsuite/tests/esc/TestDataCon.hs b/testsuite/tests/esc/TestDataCon.hs
new file mode 100644
index 0000000000..e5b66eb094
--- /dev/null
+++ b/testsuite/tests/esc/TestDataCon.hs
@@ -0,0 +1,25 @@
+module TestDataCon where
+
+{-# CONTRACT g1 :: ({x | x>0}, any) -> {r | r>0} #-}
+g1 :: (Int, Int) -> Int
+g1 (x,y) = x
+{-# CONTRACT g2 :: (any, {y | y>0}) -> {r | r>0} #-}
+g2 :: (Int, Int) -> Int
+g2 (x,y) = y
+
+bad = error "bad!"
+
+t1 = g1 (5, bad)
+t2 = g2 (bad, 6)
+t3 = g1 (bad, 7)
+t4 = g1 (-1, 6) -- seems inlining is done.
+
+{-
+data A a = B a | C a Int
+
+{-# CONTRACT g :: B {x | x>0} -> any #-}
+g :: B Int -> Int
+g (B x) = x
+
+
+-}
diff --git a/testsuite/tests/esc/TestImport.hs b/testsuite/tests/esc/TestImport.hs
new file mode 100644
index 0000000000..bf91eafb63
--- /dev/null
+++ b/testsuite/tests/esc/TestImport.hs
@@ -0,0 +1,27 @@
+module TestImport where
+
+import TestList
+
+{-# CONTRACT t2 :: _ #-}
+t2 = head1 [True]  -- same as TestList res2
+
+{-# CONTRACT t3 :: {x | True} #-}
+t3 = head1 [True]  -- same as TestList.res3
+
+t4 = head1 []      -- same as TestList.res4
+
+t5 = head1 [True]  -- same as TestList.res5
+
+t2a = res2
+t3a = res3
+t4a = res4
+t5a = res5
+
+{-# CONTRACT tail1 :: {xs | not1 (null1 xs)} ->  {r | True} #-}
+tail1 :: [Int] -> [Int]
+tail1 (x:xs) = xs
+
+{-# CONTRACT tail2 :: {xs | not (null xs)} ->  {r | True} #-}
+tail2 :: [Int] -> [Int]
+tail2 (x:xs) = xs
+
diff --git a/testsuite/tests/esc/TestList.hs b/testsuite/tests/esc/TestList.hs
new file mode 100644
index 0000000000..66f9df2263
--- /dev/null
+++ b/testsuite/tests/esc/TestList.hs
@@ -0,0 +1,24 @@
+module TestList where
+
+{-# CONTRACT head1 :: {ys | not1 (null1 ys)} -> {r | True} #-}
+-- {-# CONTRACT head1 :: {xs | not (null xs)} -> {r | True} #-}
+head1 :: [Bool] -> Bool
+head1 (x:xs) = x
+
+not1 True = False
+not1 False = True
+
+null1 [] = True
+null1 xs = False
+
+{-# CONTRACT res2 :: _ #-}
+res2 = head1 [True]
+
+{-# CONTRACT res3 :: {x | True} #-}
+res3 = head1 [True]
+
+res4 = head1 []
+
+res5 = head1 [True]
+
+
diff --git a/testsuite/tests/esc/all.T b/testsuite/tests/esc/all.T
new file mode 100644
index 0000000000..55b21ee2a3
--- /dev/null
+++ b/testsuite/tests/esc/all.T
@@ -0,0 +1,5 @@
+esc = unless_tag('esc', skip)
+
+test('TestList', esc, compile, ['-fesc'])
+test('TestImport', esc, compile, ['-fesc'])
+test('TestData', esc, compile, ['-fesc'])
diff --git a/testsuite/tests/esc/synonym.hs b/testsuite/tests/esc/synonym.hs
new file mode 100644
index 0000000000..24b035ccc1
--- /dev/null
+++ b/testsuite/tests/esc/synonym.hs
@@ -0,0 +1,10 @@
+{-# TYPE nat = {x | x > 0} #-}
+{-# TYPE notNull = {xs | not (null xs)} #-}
+
+{-# CONTRACT f :: nat -> nat #-}
+f :: Int -> Int
+f x = x 
+
+{-# CONTRACT g :: notNull -> any #-}
+g :: [Int] -> Int
+g (x:xs) = x