From 7b0b363b325b884bad88e690e59504c651334f10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Dec 2013 06:40:26 -0800
Subject: [PATCH] fix(kernel/normalizer): metavariable reification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/metavar.cpp          |  4 +++-
 src/kernel/normalizer.cpp       | 15 ++++++++-------
 src/tests/kernel/metavar.cpp    | 21 +++++++++++----------
 src/tests/kernel/normalizer.cpp | 12 ++++++++++++
 4 files changed, 34 insertions(+), 18 deletions(-)

diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 2df7c208f..6beced623 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -380,7 +380,9 @@ expr metavar_env_cell::instantiate_metavars(expr const & e, buffer<justification
     if (!has_metavar(e)) {
         return e;
     } else {
-        return instantiate_metavars_proc(this, jsts)(e);
+        expr r = instantiate_metavars_proc(this, jsts)(e);
+        lean_assert(!has_assigned_metavar(r));
+        return r;
     }
 }
 
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 6d95be471..18261cedf 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -159,17 +159,18 @@ class normalizer::imp {
                 });
         } else {
             lean_assert(is_metavar(e));
-            if (is_identity_stack(s, k))
-                return e; // nothing to be done
-            local_context lctx = metavar_lctx(e);
-            unsigned len_s     = length(s);
-            unsigned len_ctx   = ctx.size();
+            local_context lctx     = metavar_lctx(e);
+            unsigned len_s         = length(s);
+            unsigned len_ctx       = ctx.size();
             lean_assert(k >= len_ctx);
             expr r;
-            if (k > len_ctx)
-                r = add_lift(e, len_s, k - len_ctx);
+            if (k > len_ctx + len_s)
+                r = add_lift(e, len_s, k - len_ctx - len_s);
             else
                 r = e;
+            if (is_identity_stack(s, k)) {
+                return r;
+            }
             buffer<expr> subst;
             for (auto v : s)
                 subst.push_back(reify(v, k));
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 002aabeda..2be93a48e 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -376,9 +376,6 @@ static void tst18() {
     environment env;
     metavar_env menv;
     normalizer  norm(env);
-    context ctx;
-    ctx = extend(ctx, "w1", Type());
-    ctx = extend(ctx, "w2", Type());
     expr f = Const("f");
     expr g = Const("g");
     expr h = Const("h");
@@ -387,12 +384,13 @@ static void tst18() {
     expr z = Const("z");
     expr N = Const("N");
     expr a = Const("a");
+    context ctx({{"x1", N}});
     env->add_var("N", Type());
     env->add_var("a", N);
     env->add_var("g", N >> N);
     env->add_var("h", N >> (N >> N));
-    expr m1 = menv->mk_metavar(context({{"z", Type()}, {"f", N >> N}, {"y", Type()}}));
-    expr m2 = menv->mk_metavar(context({{"z", Type()}, {"x", N}, {"x1", N}}));
+    expr m1 = menv->mk_metavar(context({{"x1", N}, {"z", Type()}, {"f", N >> N}, {"y", Type()}}));
+    expr m2 = menv->mk_metavar(context({{"x1", N}, {"z", Type()}, {"x", N}}));
     expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N));
     std::cout << norm(F, ctx) << "\n";
     metavar_env menv2 = menv.copy();
@@ -400,9 +398,12 @@ static void tst18() {
     menv2->assign(m2, h(Var(2), Var(1)));
     std::cout << menv2->instantiate_metavars(norm(F, ctx)) << "\n";
     std::cout << menv2->instantiate_metavars(F) << "\n";
-    lean_assert_eq(menv2->instantiate_metavars(norm(F, ctx)),
-                   norm(menv2->instantiate_metavars(F), ctx));
-    lean_assert_eq(menv2->instantiate_metavars(norm(F, ctx)),
+    lean_assert_eq(menv2->instantiate_metavars(norm(F, ctx, menv2)),
+                   norm(menv2->instantiate_metavars(F), ctx, menv2));
+    std::cout << "norm(F...): " << norm(F, ctx, menv2) << "\n";
+    lean_assert(menv2->is_assigned(m1));
+    lean_assert(menv2->is_assigned(m2));
+    lean_assert_eq(menv2->instantiate_metavars(norm(F, ctx, menv2)),
                    Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z))));
 }
 
@@ -420,8 +421,8 @@ static void tst19() {
     expr F  = Fun({{N, Type()}, {x, N}, {y, N}}, m1);
     std::cout << norm(F) << "\n";
     std::cout << norm(F, ctx) << "\n";
-    lean_assert(norm(F) == F);
-    lean_assert(norm(F, ctx) == F);
+    lean_assert_eq(norm(F, context(), menv), F);
+    lean_assert_eq(norm(F, ctx, menv), F);
 }
 
 static void tst20() {
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index a619a3f30..3b04e6476 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -303,6 +303,17 @@ static void tst9() {
     lean_assert_eq(N, Fun({x, Type()}, f(x, Bool)));
 }
 
+static void tst10() {
+    environment env;
+    import_all(env);
+    metavar_env menv;
+    context ctx({{"x", Bool}, {"y", Bool}});
+    expr m  = menv->mk_metavar(ctx);
+    ctx     = extend(ctx, "z", none_expr(), m);
+    std::cout << normalizer(env)(Var(0), ctx) << "\n";
+    lean_assert_eq(normalizer(env)(Var(0), ctx), add_lift(m, 0, 1));
+}
+
 int main() {
     save_stack_info();
     tst_church_numbers();
@@ -315,5 +326,6 @@ int main() {
     tst7();
     tst8();
     tst9();
+    tst10();
     return has_violations() ? 1 : 0;
 }