From a5adddaf14890cbf909070bba93a8956293c52ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 31 Aug 2013 18:46:18 -0700
Subject: [PATCH] Add more tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 .gitignore                       |  2 +-
 tests/lean/ex2.lean              | 17 +++++++++++++++++
 tests/lean/ex2.lean.expected.out | 20 ++++++++++++++++++++
 tests/lean/ex3.lean              |  9 +++++++++
 tests/lean/ex3.lean.expected.out | 18 ++++++++++++++++++
 tests/lean/test.sh               |  4 ++--
 6 files changed, 67 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/ex2.lean
 create mode 100644 tests/lean/ex2.lean.expected.out
 create mode 100644 tests/lean/ex3.lean
 create mode 100644 tests/lean/ex3.lean.expected.out

diff --git a/.gitignore b/.gitignore
index cbbd71e0a7..c54341b587 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,6 @@
 *~
 .lean_trace
+*.produced.out
 a.out
 build
 GPATH
@@ -9,4 +10,3 @@ GTAGS
 Makefile
 *.cmake
 CMakeFiles/
-
diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean
new file mode 100644
index 0000000000..219e901bad
--- /dev/null
+++ b/tests/lean/ex2.lean
@@ -0,0 +1,17 @@
+(* comment *)
+(* (* nested comment *) *)
+Show true
+Set lean::pp::notation false
+Show true && false
+Variable a : Bool
+Variable a : Bool
+Variable b : Bool
+Show a && b
+Variable A : Type
+Check a && A
+Show Environment 1
+Show Options
+Set lean::p::notation true
+Set lean::pp::notation 10
+Set lean::pp::notation true
+Show a && b
diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out
new file mode 100644
index 0000000000..1036e93024
--- /dev/null
+++ b/tests/lean/ex2.lean.expected.out
@@ -0,0 +1,20 @@
+⊤
+  Set option: lean::pp::notation
+and true false
+  Assumed: a
+Error (line: 7, pos: 0) invalid object declaration, environment already has an object named 'a'
+  Assumed: b
+and a b
+  Assumed: A
+Error (line: 11, pos: 11) type mismatch at application argument 2 of
+    and a A
+expected type
+    Bool
+given type
+    Type
+Variable A : Type
+⟨lean::pp::notation ↦ false⟩
+Error (line: 14, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
+Error (line: 15, pos: 23) invalid option value, given option is not an integer
+  Set option: lean::pp::notation
+a ∧ b
diff --git a/tests/lean/ex3.lean b/tests/lean/ex3.lean
new file mode 100644
index 0000000000..9154da3c82
--- /dev/null
+++ b/tests/lean/ex3.lean
@@ -0,0 +1,9 @@
+Variable myeq : Pi (A : Type), A -> A -> Bool
+Show myeq _ true false
+Variable T : Type
+Variable a : T
+Check myeq _ true a
+Variable myeq2 {A:Type} (a b : A) : Bool
+Infix 50 === : myeq2
+Set lean::pp::implicit true
+Check true === a
\ No newline at end of file
diff --git a/tests/lean/ex3.lean.expected.out b/tests/lean/ex3.lean.expected.out
new file mode 100644
index 0000000000..809eb404cb
--- /dev/null
+++ b/tests/lean/ex3.lean.expected.out
@@ -0,0 +1,18 @@
+  Assumed: myeq
+myeq Bool ⊤ ⊥
+  Assumed: T
+  Assumed: a
+Error (line: 5, pos: 6) type mismatch at application argument 3 of
+    myeq Bool ⊤ a
+expected type
+    Bool
+given type
+    T
+  Assumed: myeq2
+  Set option: lean::pp::implicit
+Error (line: 9, pos: 15) type mismatch at application argument 3 of
+    myeq2::explicit Bool ⊤ a
+expected type
+    Bool
+given type
+    T
diff --git a/tests/lean/test.sh b/tests/lean/test.sh
index 55bdc07907..f946325254 100755
--- a/tests/lean/test.sh
+++ b/tests/lean/test.sh
@@ -11,11 +11,11 @@ else
 fi
 NUM_ERRORS=0
 for f in `ls *.lean`; do
-    echo $f
+    echo "-- testing $f"
     $LEAN $f > $f.produced.out
     if test -f $f.expected.out; then
         if diff $f.produced.out $f.expected.out; then
-            echo "-- $f checked"
+            echo "-- checked"
         else
             echo "ERROR: file $f.produced.out does not match $f.expected.out"
             NUM_ERRORS=$(($NUM_ERRORS+1))