From d79cfa38e392c6ecc73748ecd50ecd669bd7e08c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Mar 2020 15:48:00 -0700
Subject: [PATCH] test: `generalizeTelescope` tests

---
 tests/lean/run/generalizeTelescope.lean | 62 +++++++++++++++++++++++++
 1 file changed, 62 insertions(+)
 create mode 100644 tests/lean/run/generalizeTelescope.lean

diff --git a/tests/lean/run/generalizeTelescope.lean b/tests/lean/run/generalizeTelescope.lean
new file mode 100644
index 0000000000..abe79f60c1
--- /dev/null
+++ b/tests/lean/run/generalizeTelescope.lean
@@ -0,0 +1,62 @@
+import Init.Lean
+open Lean
+open Lean.Meta
+
+inductive Vec (α : Type) : Nat → Type
+| nil      : Vec 0
+| cons {n} : α → Vec n → Vec (n+1)
+
+set_option trace.Meta.debug true
+
+def nat  := mkConst `Nat
+def succ := mkConst `Nat.succ
+
+def tst1 : MetaM Unit :=
+withLocalDecl `n nat BinderInfo.default $ fun n => do
+let n1    := mkApp succ n;
+let vecN1 := mkApp2 (mkConst `Vec) nat n1;
+withLocalDecl `xs vecN1 BinderInfo.default $ fun xs => do
+generalizeTelescope #[n1, xs] `aux $ fun ys => do
+let ys := (ys.map mkFVar);
+t ← mkLambda ys ys.back;
+trace! `Meta.debug t;
+pure ()
+
+#eval tst1
+
+set_option pp.all true
+
+def tst2 : MetaM Unit :=
+withLocalDecl `n nat BinderInfo.default $ fun n => do
+let n1    := mkApp succ n;
+let vecN1 := mkApp2 (mkConst `Vec) nat n1;
+withLocalDecl `xs vecN1 BinderInfo.default $ fun xs => do
+e ← mkEqRefl xs;
+generalizeTelescope #[n1, xs, e] `aux $ fun ys => do
+let ys := (ys.map mkFVar);
+t ← mkLambda ys ys.back;
+trace! `Meta.debug t;
+pure ()
+
+#eval tst2
+
+def failIfSuccess (x : MetaM Unit) : MetaM Unit :=
+whenM (catch (x *> pure true) (fun _ => pure false)) $
+  throw $ Exception.other "unexpected success"
+
+def tst3 : MetaM Unit :=
+withLocalDecl `n nat BinderInfo.default $ fun n => do
+let n1    := mkApp succ n;
+let vecN1 := mkApp2 (mkConst `Vec) nat n1;
+withLocalDecl `xs vecN1 BinderInfo.default $ fun xs => do
+e ← mkEqRefl xs;
+failIfSuccess $ do {
+  generalizeTelescope #[n1, e] `aux $ fun ys => do
+  let ys := (ys.map mkFVar);
+  t ← mkLambda ys ys.back;
+  trace! `Meta.debug t;
+  pure ()
+};
+trace! `Meta.debug "failed as expected"
+
+#eval tst3