From 05f0c8325366a65f7f94cf42484c85ffd9580e4d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Oct 2019 19:49:29 -0700
Subject: [PATCH] test: add new test for `MetavarContext.mkLambda`

---
 tests/lean/mvar3.lean              | 71 ++++++++++++++++++++++++++++++
 tests/lean/mvar3.lean.expected.out |  8 ++++
 2 files changed, 79 insertions(+)
 create mode 100644 tests/lean/mvar3.lean
 create mode 100644 tests/lean/mvar3.lean.expected.out

diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
new file mode 100644
index 0000000000..eb4b2f7cb8
--- /dev/null
+++ b/tests/lean/mvar3.lean
@@ -0,0 +1,71 @@
+import Init.Lean.MetavarContext
+open Lean
+
+def check (b : Bool) : IO Unit :=
+unless b (throw "error")
+
+def f := Expr.const `f []
+def g := Expr.const `g []
+def a := Expr.const `a []
+def b := Expr.const `b []
+def c := Expr.const `c []
+
+def b0 := Expr.bvar 0
+def b1 := Expr.bvar 1
+def b2 := Expr.bvar 2
+
+def u := Level.param `u
+
+def typeE := Expr.sort Level.one
+def natE  := Expr.const `Nat []
+def boolE := Expr.const `Bool []
+def vecE  := Expr.const `Vec [Level.zero]
+
+def α := Expr.fvar `α
+def x := Expr.fvar `x
+def y := Expr.fvar `y
+def z := Expr.fvar `z
+def w := Expr.fvar `w
+
+def m1 := Expr.mvar `m1
+def m2 := Expr.mvar `m2
+def m3 := Expr.mvar `m3
+
+def bi := BinderInfo.default
+def arrow (d b : Expr) := Expr.forallE `_ bi d b
+
+def lctx1 : LocalContext := {}
+def lctx2 := lctx1.mkLocalDecl `α `α typeE
+def lctx3 := lctx2.mkLocalDecl `x `x m1
+def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE m2)
+
+def mctx1 : MetavarContext := {}
+def mctx2  := mctx1.mkDecl `m1 `m1 lctx2 typeE
+def mctx3  := mctx2.mkDecl `m2 `m2 lctx3 natE
+def mctx4  := mctx3.mkDecl `m3 `m3 lctx3 natE
+def mctx4' := mctx3.mkDecl `m3 `m3 lctx3 natE true
+
+def R1 :=
+match mctx4.mkLambda {namePrefix := `n} lctx4 #[α, x, y] $ mkApp f #[m3, x] with
+| Except.ok s    => s
+| Except.error e => panic! (toString e)
+def e1    := R1.2.2
+def mctx5 := R1.1
+
+#eval toString $ mctx5.decls.toList.map Prod.fst
+#eval toString mctx5.eAssignment.toList
+#eval e1
+#eval check (!e1.hasFVar)
+
+def R2 :=
+match mctx4'.mkLambda {namePrefix := `n} lctx4 #[α, x, y] $ mkApp f #[m3, x] with
+| Except.ok s    => s
+| Except.error e => panic! (toString e)
+def e2    := R2.2.2
+def mctx6 := R2.1
+
+#eval toString $ mctx6.decls.toList.map Prod.fst
+#eval toString mctx6.eAssignment.toList
+-- ?n.2 was delayed assigned because ?m.3 is synthetic
+#eval toString $ mctx6.dAssignment.toList.map Prod.fst
+#eval e2
diff --git a/tests/lean/mvar3.lean.expected.out b/tests/lean/mvar3.lean.expected.out
new file mode 100644
index 0000000000..5f6a458ef1
--- /dev/null
+++ b/tests/lean/mvar3.lean.expected.out
@@ -0,0 +1,8 @@
+"[m1, m2, n.1, n.2, m3, n.3]"
+"[(m1, ?n.1 α), (m2, ?n.3 α x), (m3, ?n.2 α x)]"
+fun (α : Type) (x : ?n.1 α) (y : Nat -> (?n.3 α x)) => f (?n.2 α x) x
+
+"[m1, m2, n.1, n.2, m3, n.3]"
+"[(m1, ?n.1 α), (m2, ?n.3 α x)]"
+"[n.2]"
+fun (α : Type) (x : ?n.1 α) (y : Nat -> (?n.3 α x)) => f (?n.2 α x) x