feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed

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

src/frontends/lean/frontend_elaborator.cpp

@@ -175,7 +175,7 @@ class frontend_elaborator::imp {
             if (!f_t || is_pi(*f_t)) {
                 return f_t;
             } else {
-                expr r = m_ref.m_normalizer(*f_t, ctx);
+                expr r = m_ref.m_normalizer(*f_t, ctx, m_ref.m_menv);
                 if (is_pi(r))
                     return some_expr(r);
                 else

src/kernel/normalizer.cpp

@@ -72,12 +72,21 @@ class normalizer::imp {
 
     ro_environment::weak_ref m_env;
     context                  m_ctx;
+    cached_metavar_env       m_menv;
     cache                    m_cache;
     unsigned                 m_max_depth;
     unsigned                 m_depth;
 
     ro_environment env() const { return ro_environment(m_env); }
 
+    expr instantiate(expr const & e, unsigned n, expr const * s) {
+        return ::lean::instantiate(e, n, s, m_menv.to_some_menv());
+    }
+
+    expr add_lift(expr const & m, unsigned s, unsigned n) {
+        return ::lean::add_lift(m, s, n, m_menv.to_some_menv());
+    }
+
     /**
         \brief Auxiliary object for saving the current context.
         We need this to be able to process values in the context.
@@ -164,9 +173,11 @@ class normalizer::imp {
         unsigned len_s     = length(s);
         unsigned len_ctx   = m_ctx.size();
         lean_assert(k >= len_ctx);
+        expr r;
         if (k > len_ctx)
-            lctx = add_lift(lctx, len_s, k - len_ctx);
-        expr r = update_metavar(m, lctx);
+            r = add_lift(m, len_s, k - len_ctx);
+        else
+            r = m;
         buffer<expr> subst;
         for (auto e : s) {
             subst.push_back(reify(e, k));
@@ -296,20 +307,24 @@ public:
         m_depth          = 0;
     }
 
-    expr operator()(expr const & e, context const & ctx) {
+    expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
         set_ctx(ctx);
+        if (m_menv.update(menv))
+            m_cache.clear();
         unsigned k = m_ctx.size();
         return reify(normalize(e, value_stack(), k), k);
     }
 
-    void clear() { m_ctx = context(); m_cache.clear(); }
+    void clear() { m_ctx = context(); m_cache.clear(); m_menv.clear(); }
 };
 
 normalizer::normalizer(ro_environment const & env, unsigned max_depth):m_ptr(new imp(env, max_depth)) {}
 normalizer::normalizer(ro_environment const & env):normalizer(env, std::numeric_limits<unsigned>::max()) {}
 normalizer::normalizer(ro_environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {}
 normalizer::~normalizer() {}
-expr normalizer::operator()(expr const & e, context const & ctx) { return (*m_ptr)(e, ctx); }
+expr normalizer::operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv) { return (*m_ptr)(e, ctx, menv); }
+expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const & menv) { return operator()(e, ctx, some_menv(menv)); }
+expr normalizer::operator()(expr const & e, context const & ctx) { return operator()(e, ctx, none_menv()); }
 void normalizer::clear() { m_ptr->clear(); }
 
 expr normalize(expr const & e, ro_environment const & env, context const & ctx) {

src/kernel/normalizer.h

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 namespace lean {
 class environment;
 class options;
+class metavar_env;
 /** \brief Functional object for normalizing expressions */
 class normalizer {
     class imp;
@@ -23,6 +24,8 @@ public:
     normalizer(ro_environment const & env, options const & opts);
     ~normalizer();
 
+    expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv);
+    expr operator()(expr const & e, context const & ctx, metavar_env const & menv);
     expr operator()(expr const & e, context const & ctx = context());
 
     void clear();

src/kernel/type_checker.cpp

@@ -51,7 +51,7 @@ class type_checker::imp {
     }
 
     expr normalize(expr const & e, context const & ctx) {
-        return m_normalizer(e, ctx);
+        return m_normalizer(e, ctx, m_menv.to_some_menv());
     }
 
     expr check_pi(expr const & e, expr const & s, context const & ctx) {

src/library/elaborator/elaborator.cpp

@@ -535,7 +535,7 @@ class elaborator::imp {
     }
 
     expr normalize(context const & ctx, expr const & a) {
-        return m_normalizer(a, ctx);
+        return m_normalizer(a, ctx, m_state.m_menv);
     }
 
     void process_app(context const & ctx, expr & a) {

src/tests/kernel/normalizer.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/printer.h"
+#include "kernel/metavar.h"
 #include "library/all/all.h"
 using namespace lean;
 
@@ -248,6 +249,30 @@ static void tst6() {
     }
 }
 
+static void tst7() {
+    environment env;
+    import_all(env);
+    metavar_env menv;
+    expr m1 = menv->mk_metavar();
+    expr x  = Const("x");
+    expr F  = Fun({x, Bool}, m1(x))(True);
+    normalizer proc(env);
+    std::cout << F << " --> " << proc(F, context(), menv) << "\n";
+    // In the following assertion, we provide the metavar_env to the normalizer.
+    // Thus, it "knowns" the metavariable does not contain the free variable #0
+    lean_assert_eq(proc(F, context(), menv), m1(True));
+    // In the following assertion, we did not provide the metavar_env to the normalizer.
+    // Thus, it assumes the may contain the free variable #0, then it adds
+    // the local context ?m::0[inst:0 true]
+    lean_assert_eq(proc(F, context()), add_inst(m1, 0, True)(True));
+    // In the following assertion, the normalizer has to use the local context
+    // because the metavariable m2 was defined in a context of size 1.
+    // Thus, it may contain the free variable #0.
+    expr m2 = menv->mk_metavar(context({{"x", Bool}}));
+    expr F2  = Fun({x, Bool}, m2(x))(True);
+    lean_assert_eq(proc(F2, context(), menv), add_inst(m2, 0, True)(True));
+}
+
 int main() {
     save_stack_info();
     tst_church_numbers();
@@ -257,5 +282,6 @@ int main() {
     tst4();
     tst5();
     tst6();
+    tst7();
     return has_violations() ? 1 : 0;
 }