Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env

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

src/kernel/metavar.cpp

@@ -12,9 +12,9 @@ Author: Leonardo de Moura
 #include "kernel/for_each.h"
 
 namespace lean {
-expr metavar_env::mk_metavar() {
+expr metavar_env::mk_metavar(context const & ctx) {
     unsigned midx = m_env.size();
-    m_env.push_back(mk_pair(expr(), expr()));
+    m_env.push_back(data(ctx));
     return ::lean::mk_metavar(midx);
 }
 
@@ -23,34 +23,34 @@ bool metavar_env::contains(unsigned midx) const {
 }
 
 bool metavar_env::is_assigned(unsigned midx) const {
-    return m_env[midx].first;
+    return m_env[midx].m_subst;
 }
 
 expr metavar_env::get_subst(unsigned midx) const {
-    return m_env[midx].first;
+    return m_env[midx].m_subst;
 }
 
 expr metavar_env::get_type(unsigned midx, unification_problems & up) {
     auto p = m_env[midx];
-    expr t = p->second;
+    expr t = p->m_type;
     if (t) {
         return t;
     } else {
         t = mk_metavar();
-        expr s = p->first;
-        m_env[midx] = mk_pair(s, t);
+        expr s = p->m_subst;
+        m_env[midx] = data(s, t, p->m_ctx);
         if (s)
-            up.add_type_of_eq(s, t);
+            up.add_type_of_eq(p->m_ctx, s, t);
         else
-            up.add_type_of_eq(::lean::mk_metavar(midx), t);
+            up.add_type_of_eq(p->m_ctx, ::lean::mk_metavar(midx), t);
         return t;
     }
 }
 
-void metavar_env::assign(unsigned midx, expr const & t) {
+void metavar_env::assign(unsigned midx, expr const & v) {
     lean_assert(!is_assigned(midx));
     auto p = m_env[midx];
-    m_env[midx] = mk_pair(t, p->second);
+    m_env[midx] = data(v, p->m_type, p->m_ctx);
 }
 
 expr subst(expr const & a, unsigned i, expr const & c) {

src/kernel/metavar.h

@@ -5,35 +5,29 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <utility>
-#include <vector>
 #include "util/pair.h"
 #include "util/pvector.h"
 #include "kernel/expr.h"
+#include "kernel/context.h"
 
 namespace lean {
 /**
    \brief Set of unification problems that need to be solved.
    It store two kinds of problems:
-   1. <tt>lhs == rhs</tt>
-   2. <tt>typeof(n) == t</tt>
+   1. <tt>ctx |- lhs == rhs</tt>
+   2. <tt>ctx |- typeof(n) == t</tt>
 */
 class unification_problems {
-    std::vector<std::pair<expr, expr>> m_eqs;
-    std::vector<std::pair<expr, expr>> m_type_of_eqs;
 public:
+    virtual ~unification_problems() {}
     /**
-       \brief Add a new unification problem of the form <tt>lhs == rhs</tt>
+       \brief Add a new unification problem of the form <tt>ctx |- lhs == rhs</tt>
     */
-    void add_eq(expr const & lhs, expr const & rhs) { m_eqs.push_back(mk_pair(lhs, rhs)); }
-
+    virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) = 0;
     /**
-       \brief Add a new unification problem of the form <tt>typeof(n) == t</tt>
+       \brief Add a new unification problem of the form <tt>ctx |- typeof(n) == t</tt>
     */
-    void add_type_of_eq(expr const & n, expr const & t) { m_type_of_eqs.push_back(mk_pair(n, t)); }
-
-    std::vector<std::pair<expr, expr>> const & eqs() const { return m_eqs; }
-    std::vector<std::pair<expr, expr>> const & type_of_eqs() const { return m_type_of_eqs; }
+    virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) = 0;
 };
 
 /**
@@ -41,12 +35,19 @@ public:
    from metavariables to assignments and types.
 */
 class metavar_env {
-    pvector<std::pair<expr, expr>> m_env;
+    struct data {
+        expr    m_subst;
+        expr    m_type;
+        context m_ctx;
+        data(context const & ctx):m_ctx(ctx) {}
+        data(expr const & s, expr const & t, context const & ctx):m_subst(s), m_type(t), m_ctx(ctx) {}
+    };
+    pvector<data> m_env;
 public:
     /**
        \brief Create new metavariable in this environment.
     */
-    expr mk_metavar();
+    expr mk_metavar(context const & ctx = context());
 
     /**
        \brief Return true if this environment contains a metavariable

src/tests/kernel/metavar.cpp

@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
+#include <vector>
+#include <utility>
 #include "util/test.h"
 #include "kernel/metavar.h"
 #include "kernel/instantiate.h"
@@ -13,8 +15,20 @@ Author: Leonardo de Moura
 #include "library/printer.h"
 using namespace lean;
 
+class unification_problems_dbg : public unification_problems {
+    std::vector<std::pair<expr, expr>> m_eqs;
+    std::vector<std::pair<expr, expr>> m_type_of_eqs;
+public:
+    unification_problems_dbg() {}
+    virtual ~unification_problems_dbg() {}
+    virtual void add_eq(context const &, expr const & lhs, expr const & rhs) { m_eqs.push_back(mk_pair(lhs, rhs)); }
+    virtual void add_type_of_eq(context const &, expr const & n, expr const & t) { m_type_of_eqs.push_back(mk_pair(n, t)); }
+    std::vector<std::pair<expr, expr>> const & eqs() const { return m_eqs; }
+    std::vector<std::pair<expr, expr>> const & type_of_eqs() const { return m_type_of_eqs; }
+};
+
 static void tst1() {
-    unification_problems u;
+    unification_problems_dbg u;
     metavar_env          menv;
     expr m1 = menv.mk_metavar();
     lean_assert(!menv.is_assigned(m1));