From ca24518ab5b573f73c1d609a35f4bcbcab487c91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Mar 2016 16:58:38 -0700
Subject: [PATCH] test(tests/lean/run/unify1.lean): new type_context is_def_eq

---
 tests/lean/unify1.lean              | 31 +++++++++++++++++++++++++++++
 tests/lean/unify1.lean.expected.out | 24 ++++++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 tests/lean/unify1.lean
 create mode 100644 tests/lean/unify1.lean.expected.out

diff --git a/tests/lean/unify1.lean b/tests/lean/unify1.lean
new file mode 100644
index 0000000000..34aef5ecd7
--- /dev/null
+++ b/tests/lean/unify1.lean
@@ -0,0 +1,31 @@
+import data.list
+open list
+
+definition ID {A : Type} (a : A) := a
+
+-- set_option trace.type_context.is_def_eq_detail true
+-- set_option pp.purify_metavars false
+
+#unify id (_ ++ (_ : list nat)), ([1, 2] ++ [(3:nat), 4])
+
+#unify (_ ++ (_ : list nat)), id ([1, 2] ++ [(3:nat), 4])
+
+#unify (_ ++ (_ : list nat)), ID ([1, 2] ++ [(3:nat), 4])
+
+#unify (_ ++ (_ : list nat)), ID (ID ([1, 2] ++ [(3:nat), 4]))
+
+#unify ID (_ ++ (_ : list nat)), ID ([1, 2] ++ [(3:nat), 4])
+
+#unify ID (_ ++ (_ : list nat)), ([1, 2] ++ [(3:nat), 4])
+
+-- The following one fails because both sides are productive, and
+-- we need to unfolding steps in the lhs to get the same
+-- head symbol in the rhs
+-- #unify ID (ID (_ ++ (_ : list nat))), ([1, 2] ++ [(3:nat), 4])
+
+#unify ([(1:nat)] ++ [2, 3, 4]), ([1, 2] ++ [(3:nat), 4])
+
+constant y1 : nat
+constant y2 : nat
+
+#unify (y1 :: _) ++ _, (let l := [y1] in l ++ [y2])
diff --git a/tests/lean/unify1.lean.expected.out b/tests/lean/unify1.lean.expected.out
new file mode 100644
index 0000000000..13b9894ac0
--- /dev/null
+++ b/tests/lean/unify1.lean.expected.out
@@ -0,0 +1,24 @@
+id (?M_1 ++ ?M_2) =?= [1, 2] ++ [3, 4]
+id ([1, 2] ++ [3, 4]) =?= [1, 2] ++ [3, 4]
+success
+?M_1 ++ ?M_2 =?= id ([1, 2] ++ [3, 4])
+[1, 2] ++ [3, 4] =?= id ([1, 2] ++ [3, 4])
+success
+?M_1 ++ ?M_2 =?= ID ([1, 2] ++ [3, 4])
+[1, 2] ++ [3, 4] =?= ID ([1, 2] ++ [3, 4])
+success
+?M_1 ++ ?M_2 =?= ID (ID ([1, 2] ++ [3, 4]))
+[1, 2] ++ [3, 4] =?= ID (ID ([1, 2] ++ [3, 4]))
+success
+ID (?M_1 ++ ?M_2) =?= ID ([1, 2] ++ [3, 4])
+ID ([1, 2] ++ [3, 4]) =?= ID ([1, 2] ++ [3, 4])
+success
+ID (?M_1 ++ ?M_2) =?= [1, 2] ++ [3, 4]
+ID ([1, 2] ++ [3, 4]) =?= [1, 2] ++ [3, 4]
+success
+[1] ++ [2, 3, 4] =?= [1, 2] ++ [3, 4]
+[1] ++ [2, 3, 4] =?= [1, 2] ++ [3, 4]
+success
+y1 :: ?M_1 ++ ?M_2 =?= let l := [y1] in l ++ [y2]
+[y1] ++ [y2] =?= let l := [y1] in l ++ [y2]
+success