Add partial support for metavariables in the normalizer

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

src/kernel/normalizer.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/context.h"
 #include "kernel/environment.h"
 #include "kernel/builtin.h"
+#include "kernel/metavar.h"
 #include "kernel/free_vars.h"
 #include "kernel/kernel_exception.h"
 
@@ -69,6 +70,8 @@ class normalizer::imp {
 
     environment const & m_env;
     context             m_ctx;
+    metavar_env const * m_menv;
+    unsigned            m_menv_timestamp;
     cache               m_cache;
     unsigned            m_max_depth;
     unsigned            m_depth;
@@ -143,10 +146,13 @@ class normalizer::imp {
         svalue r;
         switch (a.kind()) {
         case expr_kind::MetaVar:
-            // TODO(Leo) The following code should be unreachable in the current implementation.
+            if (m_menv && m_menv->contains(a) && m_menv->is_assigned(a)) {
-            // It will be needed when we implement the new elaborator.
+                r = normalize(m_menv->get_subst(a), s, k);
-            lean_unreachable();
+            } else {
-            return svalue(a);
+                // TODO(Leo) We must store in the metavariable the implicit substitution stored in value_stack.
+                r = svalue(a);
+            }
+            break;
         case expr_kind::Var:
             r = lookup(s, var_idx(a), k);
             break;
@@ -270,16 +276,33 @@ class normalizer::imp {
         }
     }
 
+    void set_menv(metavar_env const * menv) {
+        if (m_menv == menv) {
+            // Check whether m_menv has been updated since the last time the normalizer has been invoked
+            if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) {
+                m_menv_timestamp = m_menv->get_timestamp();
+                m_cache.clear();
+            }
+        } else {
+            m_menv = menv;
+            m_cache.clear();
+            m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0;
+        }
+    }
+
 public:
     imp(environment const & env, unsigned max_depth):
         m_env(env) {
-        m_interrupted = false;
+        m_interrupted    = false;
-        m_max_depth   = max_depth;
+        m_max_depth      = max_depth;
-        m_depth       = 0;
+        m_depth          = 0;
+        m_menv           = nullptr;
+        m_menv_timestamp = 0;
     }
 
-    expr operator()(expr const & e, context const & ctx) {
+    expr operator()(expr const & e, context const & ctx, metavar_env const * menv) {
         set_ctx(ctx);
+        set_menv(menv);
         unsigned k = m_ctx.size();
         return reify(normalize(e, value_stack(), k), k);
     }
@@ -294,7 +317,7 @@ public:
         return is_convertible_core(e_n, g_n);
     }
 
-    void clear() { m_ctx = context(); m_cache.clear(); }
+    void clear() { m_ctx = context(); m_cache.clear(); m_menv = nullptr; m_menv_timestamp = 0; }
     void set_interrupt(bool flag) { m_interrupted = flag; }
 };
 
@@ -302,13 +325,13 @@ normalizer::normalizer(environment const & env, unsigned max_depth):m_ptr(new im
 normalizer::normalizer(environment const & env):normalizer(env, std::numeric_limits<unsigned>::max()) {}
 normalizer::normalizer(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, metavar_env const * menv) { return (*m_ptr)(e, ctx, menv); }
 bool normalizer::is_convertible(expr const & t1, expr const & t2, context const & ctx) { return m_ptr->is_convertible(t1, t2, ctx); }
 void normalizer::clear() { m_ptr->clear(); }
 void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 
-expr normalize(expr const & e, environment const & env, context const & ctx) {
+expr normalize(expr const & e, environment const & env, context const & ctx, metavar_env const * menv) {
-    return normalizer(env)(e, ctx);
+    return normalizer(env)(e, ctx, menv);
 }
 bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) {
     return normalizer(env).is_convertible(expected, given, 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,7 +24,7 @@ public:
     normalizer(environment const & env, options const & opts);
     ~normalizer();
 
-    expr operator()(expr const & e, context const & ctx = context());
+    expr operator()(expr const & e, context const & ctx = context(), metavar_env const * menv = nullptr);
     bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context());
 
     void clear();
@@ -33,6 +34,6 @@ public:
     void reset_interrupt() { set_interrupt(false); }
 };
 /** \brief Normalize \c e using the environment \c env and context \c ctx */
-expr normalize(expr const & e, environment const & env, context const & ctx = context());
+expr normalize(expr const & e, environment const & env, context const & ctx = context(), metavar_env const * menv = nullptr);
 bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context());
 }

src/tests/kernel/metavar.cpp

@@ -12,6 +12,8 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/free_vars.h"
+#include "kernel/normalizer.h"
+#include "kernel/environment.h"
 #include "library/printer.h"
 using namespace lean;
 
@@ -246,6 +248,22 @@ static void tst11() {
     lean_assert(menv.get_timestamp() > t2);
 }
 
+static void tst12() {
+    environment env;
+    metavar_env menv;
+    expr m = menv.mk_metavar();
+    env.add_var("N", Type());
+    expr N = Const("N");
+    env.add_var("f", N >> N);
+    expr f = Const("f");
+    env.add_var("a", N);
+    expr a = Const("a");
+    expr x = Const("x");
+    expr F = Fun({x, N}, f(m))(a);
+    normalizer norm(env);
+    std::cout << norm(F) << "\n";
+}
+
 int main() {
     tst1();
     tst2();
@@ -258,5 +276,6 @@ int main() {
     tst9();
     tst10();
     tst11();
+    tst12();
     return has_violations() ? 1 : 0;
 }