From 08b23d8b4fe070079cd1c31061e17e8b6721aacf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 27 Jul 2015 20:59:29 -0700
Subject: [PATCH] test(tests/lean/extra): add test for "show goal" feature

---
 src/shell/CMakeLists.txt                      |  5 ++-
 tests/lean/extra/show_goal.14.6.expected.out  |  9 +++++
 tests/lean/extra/show_goal.15.6.expected.out  |  9 +++++
 tests/lean/extra/show_goal.18.20.expected.out | 10 ++++++
 tests/lean/extra/show_goal.18.21.expected.out |  3 ++
 tests/lean/extra/show_goal.18.6.expected.out  |  9 +++++
 tests/lean/extra/show_goal.20.4.expected.out  | 10 ++++++
 tests/lean/extra/show_goal.23.6.expected.out  | 10 ++++++
 tests/lean/extra/show_goal.24.2.expected.out  | 10 ++++++
 tests/lean/extra/show_goal.24.3.expected.out  |  3 ++
 tests/lean/extra/show_goal.6.0.expected.out   |  4 +++
 tests/lean/extra/show_goal.6.14.expected.out  |  6 ++++
 tests/lean/extra/show_goal.8.4.expected.out   |  6 ++++
 tests/lean/extra/show_goal.8.5.expected.out   |  6 ++++
 tests/lean/extra/show_goal.9.12.expected.out  |  3 ++
 tests/lean/extra/show_goal.9.4.expected.out   |  6 ++++
 tests/lean/extra/show_goal.lean               | 25 ++++++++++++++
 tests/lean/extra/show_goal.sh                 | 34 +++++++++++++++++++
 18 files changed, 167 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/extra/show_goal.14.6.expected.out
 create mode 100644 tests/lean/extra/show_goal.15.6.expected.out
 create mode 100644 tests/lean/extra/show_goal.18.20.expected.out
 create mode 100644 tests/lean/extra/show_goal.18.21.expected.out
 create mode 100644 tests/lean/extra/show_goal.18.6.expected.out
 create mode 100644 tests/lean/extra/show_goal.20.4.expected.out
 create mode 100644 tests/lean/extra/show_goal.23.6.expected.out
 create mode 100644 tests/lean/extra/show_goal.24.2.expected.out
 create mode 100644 tests/lean/extra/show_goal.24.3.expected.out
 create mode 100644 tests/lean/extra/show_goal.6.0.expected.out
 create mode 100644 tests/lean/extra/show_goal.6.14.expected.out
 create mode 100644 tests/lean/extra/show_goal.8.4.expected.out
 create mode 100644 tests/lean/extra/show_goal.8.5.expected.out
 create mode 100644 tests/lean/extra/show_goal.9.12.expected.out
 create mode 100644 tests/lean/extra/show_goal.9.4.expected.out
 create mode 100644 tests/lean/extra/show_goal.lean
 create mode 100755 tests/lean/extra/show_goal.sh

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 49ba6c99a..a459bc0ab 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -52,8 +52,11 @@ add_test(NAME "issue_597"
 add_test(NAME "issue_616"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./issue_616.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+add_test(NAME "show_goal"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./show_goal.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
-  # The following test cannot be executed on Windows because of the 
+  # The following test cannot be executed on Windows because of the
   # bash script timeout.sh
   add_test(NAME "normalizer_perf"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
diff --git a/tests/lean/extra/show_goal.14.6.expected.out b/tests/lean/extra/show_goal.14.6.expected.out
new file mode 100644
index 000000000..a4486e0be
--- /dev/null
+++ b/tests/lean/extra/show_goal.14.6.expected.out
@@ -0,0 +1,9 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0,
+aeq0 : a = 0,
+h₃ : c + 1 + a = 1,
+h₄ : d = c - 1
+⊢ c = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.15.6.expected.out b/tests/lean/extra/show_goal.15.6.expected.out
new file mode 100644
index 000000000..ba78529b2
--- /dev/null
+++ b/tests/lean/extra/show_goal.15.6.expected.out
@@ -0,0 +1,9 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0,
+aeq0 : a = 0,
+h₃ : c + 1 + 0 = 1,
+h₄ : d = c - 1
+⊢ c = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.18.20.expected.out b/tests/lean/extra/show_goal.18.20.expected.out
new file mode 100644
index 000000000..ed377d1b7
--- /dev/null
+++ b/tests/lean/extra/show_goal.18.20.expected.out
@@ -0,0 +1,10 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0,
+aeq0 : a = 0,
+h₃ : succ c = 1,
+h₄ : d = c - 1,
+a_eq : c = 0
+⊢ c = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.18.21.expected.out b/tests/lean/extra/show_goal.18.21.expected.out
new file mode 100644
index 000000000..f44617d8b
--- /dev/null
+++ b/tests/lean/extra/show_goal.18.21.expected.out
@@ -0,0 +1,3 @@
+LEAN_INFORMATION
+no goals
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.18.6.expected.out b/tests/lean/extra/show_goal.18.6.expected.out
new file mode 100644
index 000000000..e8056e617
--- /dev/null
+++ b/tests/lean/extra/show_goal.18.6.expected.out
@@ -0,0 +1,9 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0,
+aeq0 : a = 0,
+h₃ : succ c = 1,
+h₄ : d = c - 1
+⊢ c = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.20.4.expected.out b/tests/lean/extra/show_goal.20.4.expected.out
new file mode 100644
index 000000000..b24f1f7a6
--- /dev/null
+++ b/tests/lean/extra/show_goal.20.4.expected.out
@@ -0,0 +1,10 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0,
+aeq0 : a = 0,
+h₃ : c + 1 + a = 1,
+h₄ : d = c - 1,
+ceq : c = 0
+⊢ d = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.23.6.expected.out b/tests/lean/extra/show_goal.23.6.expected.out
new file mode 100644
index 000000000..a3cf7e12d
--- /dev/null
+++ b/tests/lean/extra/show_goal.23.6.expected.out
@@ -0,0 +1,10 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0,
+aeq0 : a = 0,
+h₃ : c + 1 + a = 1,
+h₄ : d = c - 1,
+deq0 : d = 0
+⊢ d = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.24.2.expected.out b/tests/lean/extra/show_goal.24.2.expected.out
new file mode 100644
index 000000000..a3cf7e12d
--- /dev/null
+++ b/tests/lean/extra/show_goal.24.2.expected.out
@@ -0,0 +1,10 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0,
+aeq0 : a = 0,
+h₃ : c + 1 + a = 1,
+h₄ : d = c - 1,
+deq0 : d = 0
+⊢ d = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.24.3.expected.out b/tests/lean/extra/show_goal.24.3.expected.out
new file mode 100644
index 000000000..f44617d8b
--- /dev/null
+++ b/tests/lean/extra/show_goal.24.3.expected.out
@@ -0,0 +1,3 @@
+LEAN_INFORMATION
+no goals
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.6.0.expected.out b/tests/lean/extra/show_goal.6.0.expected.out
new file mode 100644
index 000000000..cb0d39f47
--- /dev/null
+++ b/tests/lean/extra/show_goal.6.0.expected.out
@@ -0,0 +1,4 @@
+LEAN_INFORMATION
+a b c d : ℕ
+⊢ a + b = 0 → b = 0 → c + 1 + a = 1 → d = c - 1 → d = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.6.14.expected.out b/tests/lean/extra/show_goal.6.14.expected.out
new file mode 100644
index 000000000..7069d8f74
--- /dev/null
+++ b/tests/lean/extra/show_goal.6.14.expected.out
@@ -0,0 +1,6 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0
+⊢ c + 1 + a = 1 → d = c - 1 → d = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.8.4.expected.out b/tests/lean/extra/show_goal.8.4.expected.out
new file mode 100644
index 000000000..19be93b21
--- /dev/null
+++ b/tests/lean/extra/show_goal.8.4.expected.out
@@ -0,0 +1,6 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + b = 0,
+h₂ : b = 0
+⊢ a = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.8.5.expected.out b/tests/lean/extra/show_goal.8.5.expected.out
new file mode 100644
index 000000000..1bf5821dc
--- /dev/null
+++ b/tests/lean/extra/show_goal.8.5.expected.out
@@ -0,0 +1,6 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + 0 = 0,
+h₂ : b = 0
+⊢ a = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.9.12.expected.out b/tests/lean/extra/show_goal.9.12.expected.out
new file mode 100644
index 000000000..f44617d8b
--- /dev/null
+++ b/tests/lean/extra/show_goal.9.12.expected.out
@@ -0,0 +1,3 @@
+LEAN_INFORMATION
+no goals
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.9.4.expected.out b/tests/lean/extra/show_goal.9.4.expected.out
new file mode 100644
index 000000000..1bf5821dc
--- /dev/null
+++ b/tests/lean/extra/show_goal.9.4.expected.out
@@ -0,0 +1,6 @@
+LEAN_INFORMATION
+a b c d : ℕ,
+h₁ : a + 0 = 0,
+h₂ : b = 0
+⊢ a = 0
+END_LEAN_INFORMATION
diff --git a/tests/lean/extra/show_goal.lean b/tests/lean/extra/show_goal.lean
new file mode 100644
index 000000000..47b83ab3d
--- /dev/null
+++ b/tests/lean/extra/show_goal.lean
@@ -0,0 +1,25 @@
+import data.nat
+open nat
+
+example (a b c d : nat) : a + b = 0 → b = 0 → c + 1 + a = 1 → d = c - 1 → d = 0 :=
+begin
+  intro h₁ h₂,
+  have aeq0 : a = 0, begin
+    rewrite h₂ at h₁,
+    exact h₁
+  end,
+  intro h₃ h₄,
+  have deq0 : d = 0, begin
+    have ceq : c = 0, begin
+      rewrite aeq0 at h₃,
+      rewrite add_zero at h₃,
+      rewrite add_succ at h₃,
+      rewrite add_zero at h₃,
+      injection h₃, assumption
+    end,
+    rewrite ceq at h₄,
+    repeat (esimp [sub, pred] at h₄),
+    assumption
+  end,
+  exact deq0
+end
diff --git a/tests/lean/extra/show_goal.sh b/tests/lean/extra/show_goal.sh
new file mode 100755
index 000000000..6457480ed
--- /dev/null
+++ b/tests/lean/extra/show_goal.sh
@@ -0,0 +1,34 @@
+#!/bin/bash
+set -e
+if [ $# -ne 1 ]; then
+    echo "Usage: show_goal.sh [lean-executable-path]"
+    exit 1
+fi
+LEAN=$1
+export LEAN_PATH=../../../library:.
+
+lines=('6' '6'  '8' '8' '9' '9'  '14' '15' '18' '18' '18' '20' '23' '24' '24');
+cols=('0'  '14' '4' '5' '4' '12' '6'  '6'  '20' '21' '6'  '4'  '6'  '2'  '3');
+size=${#lines[@]}
+
+i=0
+while [ $i -lt $size ]; do
+    line=${lines[$i]}
+    col=${cols[$i]}
+    let i=i+1
+    produced=show_goal.$line.$col.produced.out
+    expected=show_goal.$line.$col.expected.out
+    $LEAN --line=$line --col=$col --goal show_goal.lean &> $produced
+    if test -f $expected; then
+        if diff --ignore-all-space -I "executing external script" "$produced" "$expected"; then
+            echo "-- checked"
+        else
+            echo "ERROR: file $produced does not match $expected"
+            exit 1
+        fi
+    else
+        echo "ERROR: file $expected does not exist"
+        exit 1
+    fi
+done
+echo "done"