Add support for new metavariable representation in the normalizer.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/normalizer.cpp

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/metavar.h"
 #include "kernel/free_vars.h"
+#include "kernel/instantiate.h"
 #include "kernel/kernel_exception.h"
 
 #ifndef LEAN_KERNEL_NORMALIZER_MAX_DEPTH
@@ -141,6 +142,44 @@ class normalizer::imp {
         return expr();
     }
 
+    /** \brief Return true iff the value_stack does affect the context of a metavariable */
+    bool is_identity_stack(value_stack const & s, unsigned k) {
+        if (length(s) != k)
+            return false;
+        unsigned i = 0;
+        for (auto e : s) {
+            if (e.kind() != svalue_kind::BoundedVar || k - to_bvar(e) - 1 != i)
+                return false;
+            ++i;
+        }
+        return true;
+    }
+
+    /**
+       \brief Update the metavariable context for \c m based on the
+       value_stack \c s and the number of binders \c k.
+       \pre is_metavar(m)
+    */
+    expr updt_metavar(expr const & m, value_stack const & s, unsigned k) {
+        lean_assert(is_metavar(m));
+        if (is_identity_stack(s, k))
+            return m; // nothing to be done
+        meta_ctx mctx    = metavar_ctx(m);
+        unsigned midx    = metavar_idx(m);
+        unsigned len_s   = length(s);
+        unsigned len_ctx = m_ctx.size();
+        lean_assert(k >= len_ctx);
+        if (k > len_ctx)
+            mctx = add_lift(mctx, len_s, k - len_ctx);
+        expr r = mk_metavar(midx, mctx);
+        buffer<expr> subst;
+        for (auto e : s) {
+            subst.push_back(reify(e, k));
+        }
+        std::reverse(subst.begin(), subst.end());
+        return instantiate(r, subst.size(), subst.data());
+    }
+
     /** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */
     svalue normalize(expr const & a, value_stack const & s, unsigned k) {
         flet<unsigned> l(m_depth, m_depth+1);
@@ -161,8 +200,7 @@ class normalizer::imp {
             if (m_menv && m_menv->contains(a) && m_menv->is_assigned(a)) {
                 r = normalize(m_menv->get_subst(a), s, k);
             } else {
-                // TODO(Leo): update metavariable
+                r = svalue(updt_metavar(a, s, k));
-                r = svalue(a);
             }
             break;
         case expr_kind::Var:

src/tests/kernel/metavar.cpp

@@ -229,7 +229,6 @@ static void tst12() {
     std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n";
 }
 
-#if 0
 static void tst13() {
     environment env;
     metavar_env menv;
@@ -358,7 +357,40 @@ static void tst17() {
     lean_assert(instantiate_metavars(norm(F, ctx), menv2) ==
                 norm(instantiate_metavars(F, menv2), ctx));
 }
-#endif
+
+static void tst18() {
+    environment env;
+    metavar_env menv;
+    normalizer  norm(env);
+    context ctx;
+    ctx = extend(ctx, "w1", Type());
+    ctx = extend(ctx, "w2", Type());
+    expr m1 = menv.mk_metavar();
+    expr m2 = menv.mk_metavar();
+    expr f = Const("f");
+    expr g = Const("g");
+    expr h = Const("h");
+    expr x = Const("x");
+    expr y = Const("y");
+    expr z = Const("z");
+    expr N = Const("N");
+    expr a = Const("a");
+    env.add_var("N", Type());
+    env.add_var("a", N);
+    env.add_var("g", N >> N);
+    env.add_var("h", N >> (N >> 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;
+    menv2.assign(0, Var(1));
+    menv2.assign(1, h(Var(2), Var(1)));
+    std::cout << instantiate_metavars(norm(F, ctx), menv2) << "\n";
+    std::cout << instantiate_metavars(F, menv2) << "\n";
+    lean_assert(instantiate_metavars(norm(F, ctx), menv2) ==
+                norm(instantiate_metavars(F, menv2), ctx));
+    lean_assert(instantiate_metavars(norm(F, ctx), menv2) ==
+                Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z))));
+}
 
 int main() {
     tst1();
@@ -373,11 +405,11 @@ int main() {
     tst10();
     tst11();
     tst12();
-    // tst13();
+    tst13();
-    // tst14();
+    tst14();
-    // tst15();
+    tst15();
-    // tst16();
+    tst16();
-    // tst17();
+    tst17();
+    tst18();
     return has_violations() ? 1 : 0;
 }
-