From 7b88d68afb2439b38ca5cdddea22d44b170b3067 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 27 Jan 2014 15:11:16 -0800
Subject: [PATCH] test(tests/lean): add test using simplifier monitor for
 tracking failures

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/simp32.lean              | 42 +++++++++++++++++++++++++++++
 tests/lean/simp32.lean.expected.out | 16 +++++++++++
 2 files changed, 58 insertions(+)
 create mode 100644 tests/lean/simp32.lean
 create mode 100644 tests/lean/simp32.lean.expected.out

diff --git a/tests/lean/simp32.lean b/tests/lean/simp32.lean
new file mode 100644
index 000000000..50d68b85c
--- /dev/null
+++ b/tests/lean/simp32.lean
@@ -0,0 +1,42 @@
+import cast
+variable vec    : Nat → Type
+variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
+infixl   65 ; : concat
+axiom    concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) :
+             (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))
+                              (v1 ; (v2 ; v3))
+variable empty : vec 0
+axiom    concat_empty {n : Nat} (v : vec n) :
+             v ; empty = cast (congr2 vec (symm (Nat::add_zeror n)))
+                         v
+
+rewrite_set simple
+add_rewrite Nat::add_assoc Nat::add_zeror eq_id : simple
+add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror : simple
+
+variable f {A : Type} : A → A
+
+(*
+local m = simplifier_monitor(nil, nil, nil,
+                             function (s, e, i, k)
+                                print("App simplification failure, argument #" .. i)
+                                print(e)
+                                print("Kind: " .. k)
+                                print("-----------")
+                             end,
+                             function (s, e, ceq, ceq_id, i, k)
+                                print("Rewrite failure: " .. tostring(e))
+                             end,
+                             function (s, e, k)
+                                print("Abst failure: " .. tostring(e))
+                             end
+)
+local s = simplifier("simple", options(), m)
+local t = parse_lean('λ val : Nat, (λ n : Nat, λ v : vec (n + 0), (f v) ; empty) val == (λ n : Nat, λ v : vec (n + 0), v) val')
+print(t)
+print("=====>")
+local t2, pr = s(t)
+print(t2)
+-- print(pr)
+get_environment():type_check(pr)
+*)
diff --git a/tests/lean/simp32.lean.expected.out b/tests/lean/simp32.lean.expected.out
new file mode 100644
index 000000000..4e31cb177
--- /dev/null
+++ b/tests/lean/simp32.lean.expected.out
@@ -0,0 +1,16 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'cast'
+  Assumed: vec
+  Assumed: concat
+  Assumed: concat_assoc
+  Assumed: empty
+  Assumed: concat_empty
+  Assumed: f
+λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val
+=====>
+App simplification failure, argument #2
+(λ (n : ℕ) (v : vec (n + 0)), f v ; empty) 2::1 == (λ (n : ℕ) (v : vec (n + 0)), v) 2::1
+Kind: 0
+-----------
+λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val