fix(kernel/metavar): add normalize assignment justification

We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.

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

src/frontends/lean/frontend_elaborator.cpp

@@ -309,7 +309,7 @@ class frontend_elaborator::imp {
         }
     };
 
-    substitution elaborate_core() {
+    metavar_env elaborate_core() {
         elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data());
         scoped_set_interruptable_ptr<elaborator> set(m_elaborator, &elb);
         return elb.next();
@@ -336,8 +336,8 @@ public:
             //     formatter fmt = mk_simple_formatter();
             //     std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
             // }
-            substitution s = elaborate_core();
-            return instantiate_metavars(new_e, s);
+            metavar_env new_menv = elaborate_core();
+            return instantiate_metavars(new_e, new_menv);
         } else {
             return new_e;
         }
@@ -358,11 +358,8 @@ public:
             //    formatter fmt = mk_simple_formatter();
             //    std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
             // }
-            substitution s = elaborate_core();
-            // s.for_each([&](name const & n, expr const & v) {
-            //        std::cout << n << " --> " << v << "\n";
-            //    });
-            return mk_pair(instantiate_metavars(new_t, s), instantiate_metavars(new_e, s));
+            metavar_env new_menv = elaborate_core();
+            return mk_pair(instantiate_metavars(new_t, new_menv), instantiate_metavars(new_e, new_menv));
         } else {
             return mk_pair(new_t, new_e);
         }

src/kernel/justification.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <vector>
 #include "util/buffer.h"
 #include "kernel/justification.h"
 
@@ -43,7 +44,7 @@ assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {}
 void assumption_justification::get_children(buffer<justification_cell*> &) const {}
 expr const & assumption_justification::get_main_expr() const { return expr::null(); }
 format assumption_justification::pp_header(formatter const &, options const &) const {
-    return format{format("assumption"), space(), format(m_idx)};
+    return format{format("Assumption"), space(), format(m_idx)};
 }
 
 bool depends_on(justification const & t, justification const & d) {

src/kernel/justification.h

@@ -85,4 +85,16 @@ inline justification mk_assumption_justification(unsigned idx) { return justific
    That is \c t is a descendant of \c d.
 */
 bool depends_on(justification const & t, justification const & d);
+
+/** \brief Add \c t to \c r */
+inline void push_back(buffer<justification_cell*> & r, justification const & t) {
+    if (t) r.push_back(t.raw());
+}
+
+/** \brief Add justifications in the collection \c s into r. */
+template<typename T>
+void append(buffer<justification_cell*> & r, T const & s) {
+    for (auto t : s)
+        push_back(r, t);
+}
 }

src/kernel/metavar.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <vector>
 #include <limits>
 #include <algorithm>
 #include "util/exception.h"
@@ -14,81 +15,47 @@ Author: Leonardo de Moura
 #include "kernel/for_each.h"
 
 namespace lean {
-void swap(substitution & s1, substitution & s2) {
-    swap(s1.m_subst, s2.m_subst);
-    std::swap(s1.m_size, s2.m_size);
-}
-
-substitution::substitution(bool beta_reduce_mv):
-    m_size(0),
-    m_beta_reduce_mv(beta_reduce_mv) {
-}
-
-bool substitution::is_assigned(name const & m) const {
-    return const_cast<substitution*>(this)->m_subst.splay_find(m);
-}
-
-bool substitution::is_assigned(expr const & m) const {
-    return is_assigned(metavar_name(m));
-}
-
-void substitution::assign(name const & m, expr const & t) {
-    lean_assert(!is_assigned(m));
-    m_subst.insert(m, t);
-    m_size++;
-}
-
-void substitution::assign(expr const & m, expr const & t) {
-    lean_assert(is_metavar(m));
-    lean_assert(!has_local_context(m));
-    assign(metavar_name(m), t);
-}
-
-expr apply_local_context(expr const & a, local_context const & lctx) {
-    if (lctx) {
-        if (is_metavar(a)) {
-            return mk_metavar(metavar_name(a), append(lctx, metavar_lctx(a)));
-        } else {
-            expr r = apply_local_context(a, tail(lctx));
-            local_entry const & e = head(lctx);
-            if (e.is_lift()) {
-                return lift_free_vars(r, e.s(), e.n());
-            } else {
-                lean_assert(e.is_inst());
-                return instantiate(r, e.s(), e.v());
-            }
-        }
-    } else {
-        return a;
+/**
+   \brief Assignment normalization justification. That is, when other assignments are applied to an existing assignment.
+*/
+class normalize_assignment_justification : public justification_cell {
+    context                    m_ctx;
+    expr                       m_expr;
+    std::vector<justification> m_jsts;
+public:
+    normalize_assignment_justification(context const & ctx, expr const & e,
+                                       justification const & jst,
+                                       unsigned num_assignment_jsts, justification const * assignment_jsts):
+        m_ctx(ctx),
+        m_expr(e),
+        m_jsts(assignment_jsts, assignment_jsts + num_assignment_jsts) {
+        m_jsts.push_back(jst);
+        std::reverse(m_jsts.begin(), m_jsts.end());
     }
-}
 
-expr substitution::get_subst(expr const & m) const {
-    lean_assert(is_metavar(m));
-    auto it = const_cast<substitution*>(this)->m_subst.splay_find(metavar_name(m));
-    if (it) {
-        if (has_assigned_metavar(*it, *this)) {
-            *it = instantiate_metavars(*it, *this);
-        }
-        local_context const & lctx = metavar_lctx(m);
-        expr r = *it;
-        if (lctx) {
-            r = apply_local_context(r, lctx);
-            if (has_assigned_metavar(r, *this))
-                r = instantiate_metavars(r, *this);
-        }
+    virtual format pp_header(formatter const & fmt, options const & opts) const {
+        unsigned indent = get_pp_indent(opts);
+        format expr_fmt = fmt(m_ctx, m_expr, false, opts);
+        format r;
+        r += format("Normalize assignment");
+        r += nest(indent, compose(line(), expr_fmt));
         return r;
-    } else {
-        return expr();
     }
-}
+
+    virtual void get_children(buffer<justification_cell*> & r) const {
+        append(r, m_jsts);
+    }
+
+    virtual expr const & get_main_expr() const { return m_expr; }
+};
 
 static name g_unique_name = name::mk_internal_unique_name();
 
 void swap(metavar_env & a, metavar_env & b) {
     swap(a.m_name_generator,         b.m_name_generator);
-    swap(a.m_substitution,           b.m_substitution);
     swap(a.m_metavar_data,           b.m_metavar_data);
+    std::swap(a.m_size,              b.m_size);
+    std::swap(a.m_beta_reduce_mv,    b.m_beta_reduce_mv);
     std::swap(a.m_timestamp,         b.m_timestamp);
 }
 
@@ -102,6 +69,8 @@ void metavar_env::inc_timestamp() {
 
 metavar_env::metavar_env(name const & prefix):
     m_name_generator(prefix),
+    m_size(0),
+    m_beta_reduce_mv(true),
     m_timestamp(0) {
 }
 
@@ -178,7 +147,8 @@ justification metavar_env::get_justification(name const & m) const {
 }
 
 bool metavar_env::is_assigned(name const & m) const {
-    return m_substitution.is_assigned(m);
+    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    return it && it->m_subst;
 }
 
 bool metavar_env::is_assigned(expr const & m) const {
@@ -186,15 +156,14 @@ bool metavar_env::is_assigned(expr const & m) const {
     return is_assigned(metavar_name(m));
 }
 
-void metavar_env::assign(name const & m, expr const & t, justification const & j) {
+void metavar_env::assign(name const & m, expr const & t, justification const & jst) {
     lean_assert(!is_assigned(m));
     inc_timestamp();
-    m_substitution.assign(m, t);
-    if (j) {
-        auto it = m_metavar_data.splay_find(m);
-        lean_assert(it);
-        it->m_justification = j;
-    }
+    m_size++;
+    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    lean_assert(it);
+    it->m_subst         = t;
+    it->m_justification = jst;
 }
 
 void metavar_env::assign(expr const & m, expr const & t, justification const & j) {
@@ -203,60 +172,103 @@ void metavar_env::assign(expr const & m, expr const & t, justification const & j
     assign(metavar_name(m), t, j);
 }
 
-struct found_unassigned{};
-name metavar_env::find_unassigned_metavar() const {
-    name r;
-    try {
-        m_metavar_data.for_each([&](name const & m, data const &) {
-                if (!m_substitution.is_assigned(m)) {
-                    r = m;
-                    throw found_unassigned();
-                }
-            });
-    } catch (found_unassigned &) {
-    }
-    return r;
-}
-
-
-void instantiate_metavars_proc::instantiated_metavar(expr const &) {
-}
-
-expr instantiate_metavars_proc::visit_metavar(expr const & m, context const &) {
-    if (is_metavar(m) && m_subst.is_assigned(m)) {
-        instantiated_metavar(m);
-        return m_subst.get_subst(m);
+expr apply_local_context(expr const & a, local_context const & lctx) {
+    if (lctx) {
+        if (is_metavar(a)) {
+            return mk_metavar(metavar_name(a), append(lctx, metavar_lctx(a)));
+        } else {
+            expr r = apply_local_context(a, tail(lctx));
+            local_entry const & e = head(lctx);
+            if (e.is_lift()) {
+                return lift_free_vars(r, e.s(), e.n());
+            } else {
+                lean_assert(e.is_inst());
+                return instantiate(r, e.s(), e.v());
+            }
+        }
     } else {
-        return m;
+        return a;
     }
 }
 
-expr instantiate_metavars_proc::visit_app(expr const & e, context const & ctx) {
-    if (m_subst.beta_reduce_metavar_application() && is_metavar(arg(e, 0)) && m_subst.is_assigned(arg(e, 0))) {
-        instantiated_metavar(arg(e, 0));
-        expr new_f = m_subst.get_subst(arg(e, 0));
-        if (is_lambda(new_f)) {
-            buffer<expr> new_args;
-            for (unsigned i = 1; i < num_args(e); i++)
-                new_args.push_back(visit(arg(e, i), ctx));
-            return apply_beta(new_f, new_args.size(), new_args.data());
+expr metavar_env::get_subst(expr const & m) const {
+    lean_assert(is_metavar(m));
+    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(metavar_name(m));
+    if (it->m_subst) {
+        if (has_assigned_metavar(it->m_subst, *this)) {
+            buffer<justification> jsts;
+            expr new_subst = instantiate_metavars(it->m_subst, *this, jsts);
+            if (!jsts.empty()) {
+                it->m_justification = justification(new normalize_assignment_justification(it->m_context, it->m_subst, it->m_justification,
+                                                                                           jsts.size(), jsts.data()));
+                it->m_subst         = new_subst;
+            }
+        }
+        local_context const & lctx = metavar_lctx(m);
+        expr r = it->m_subst;
+        if (lctx)
+            r = apply_local_context(r, lctx);
+        return r;
+    } else {
+        return expr();
+    }
+}
+
+class instantiate_metavars_proc : public replace_visitor {
+protected:
+    metavar_env const &     m_menv;
+    buffer<justification> & m_jsts;
+
+    void push_back(justification const & jst) {
+        if (jst)
+            m_jsts.push_back(jst);
+    }
+
+    virtual expr visit_metavar(expr const & m, context const & ctx) {
+        if (is_metavar(m) && m_menv.is_assigned(m)) {
+            push_back(m_menv.get_justification(m));
+            expr r = m_menv.get_subst(m);
+            if (has_assigned_metavar(r, m_menv)) {
+                return visit(r, ctx);
+            } else {
+                return r;
+            }
+        } else {
+            return m;
         }
     }
-    return replace_visitor::visit_app(e, ctx);
-}
 
-instantiate_metavars_proc::instantiate_metavars_proc(substitution const & s):m_subst(s) {
-}
+    virtual expr visit_app(expr const & e, context const & ctx) {
+        expr const & f = arg(e, 0);
+        if (m_menv.beta_reduce_metavar_application() && is_metavar(f) && m_menv.is_assigned(f)) {
+            buffer<expr> new_args;
+            for (unsigned i = 0; i < num_args(e); i++)
+                new_args.push_back(visit(arg(e, i), ctx));
+            if (is_lambda(new_args[0]))
+                return apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
+            else
+                return mk_app(new_args);
+        } else {
+            return replace_visitor::visit_app(e, ctx);
+        }
+    }
 
-expr instantiate_metavars(expr const & e, substitution const & s) {
+public:
+    instantiate_metavars_proc(metavar_env const & menv, buffer<justification> & jsts):
+        m_menv(menv),
+        m_jsts(jsts) {
+    }
+};
+
+expr instantiate_metavars(expr const & e, metavar_env const & menv, buffer<justification> & jsts) {
     if (!has_metavar(e)) {
         return e;
     } else {
-        return instantiate_metavars_proc(s)(e);
+        return instantiate_metavars_proc(menv, jsts)(e);
     }
 }
 
-bool has_assigned_metavar(expr const & e, substitution const & s) {
+bool has_assigned_metavar(expr const & e, metavar_env const & menv) {
     if (!has_metavar(e)) {
         return false;
     } else {
@@ -266,7 +278,7 @@ bool has_assigned_metavar(expr const & e, substitution const & s) {
                 return false;
             if (!has_metavar(n))
                 return false;
-            if (is_metavar(n) && s.is_assigned(n)) {
+            if (is_metavar(n) && menv.is_assigned(n)) {
                 result = true;
                 return false;
             }
@@ -333,16 +345,16 @@ expr pop_meta_context(expr const & m) {
 */
 struct found_metavar {};
 
-bool has_metavar(expr const & e, expr const & m, substitution const & s) {
+bool has_metavar(expr const & e, expr const & m, metavar_env const & menv) {
     if (has_metavar(e)) {
         lean_assert(is_metavar(m));
-        lean_assert(!s.is_assigned(m));
+        lean_assert(!menv.is_assigned(m));
         auto f = [&](expr const & m2, unsigned) {
             if (is_metavar(m2)) {
                 if (metavar_name(m) == metavar_name(m2))
                     throw found_metavar();
-                if (s.is_assigned(m2) &&
-                    has_metavar(s.get_subst(m2), m, s))
+                if (menv.is_assigned(m2) &&
+                    has_metavar(menv.get_subst(m2), m, menv))
                     throw found_metavar();
             }
             return true;

src/kernel/metavar.h

@@ -14,82 +14,6 @@ Author: Leonardo de Moura
 #include "kernel/replace_visitor.h"
 
 namespace lean {
-/**
-   \brief Metavariable substitution. It is essentially a mapping from
-   metavariables to expressions.
-*/
-class substitution {
-    typedef splay_map<name, expr, name_quick_cmp> name2expr;
-    name2expr m_subst;
-    unsigned  m_size;
-    // If the following flag is true, then beta-reduction is automatically applied
-    // when we apply a substitution containing ?m <- fun (x : T), ...
-    // to an expression containing (?m a)
-    // The motivation is that higher order unification and matching produces a
-    // bunch of assignments of the form ?m <- fun (x : T), ...
-    bool      m_beta_reduce_mv;
-public:
-    substitution(bool beta_reduce_mv = true);
-
-    bool beta_reduce_metavar_application() const { return m_beta_reduce_mv; }
-    void set_beta_reduce_metavar_application(bool f) { m_beta_reduce_mv = f; }
-
-    friend void swap(substitution & s1, substitution & s2);
-
-    /**
-       \brief Return the number of assigned metavariables in this substitution.
-    */
-    unsigned size() const { return m_size; }
-
-    /**
-       \brief Return true iff the metavariable named \c m is assigned in this substitution.
-    */
-    bool is_assigned(name const & m) const;
-
-    /**
-       \brief Return true if the given metavariable is assigned in this
-       substitution.
-
-       \pre is_metavar(m)
-    */
-    bool is_assigned(expr const & m) const;
-
-    /**
-       \brief Assign metavariable named \c m.
-
-       \pre !is_assigned(m)
-    */
-    void assign(name const & m, expr const & t);
-
-    /**
-       \brief Assign metavariable \c m to \c t.
-
-       \pre is_metavar(m)
-       \pre !has_meta_context(m)
-       \pre !is_assigned(m)
-    */
-    void assign(expr const & m, expr const & t);
-
-    /**
-       \brief Return the substitution associated with the given metavariable
-       in this substitution.
-
-       If the metavariable is not assigned in this substitution, then it returns the null
-       expression.
-
-       \pre is_metavar(m)
-    */
-    expr get_subst(expr const & m) const;
-
-    /**
-       \brief Apply f to each entry in this substitution.
-    */
-    template<typename F>
-    void for_each(F f) const { m_subst.for_each(f); }
-};
-
-void swap(substitution & s1, substitution & s2);
-
 /**
    \brief Metavar environment. It is an auxiliary datastructure used for:
 
@@ -100,6 +24,7 @@ void swap(substitution & s1, substitution & s2);
 */
 class metavar_env {
     struct data {
+        expr          m_subst;         // substitution
         expr          m_type;          // type of the metavariable
         context       m_context;       // context where the metavariable was defined
         justification m_justification; // justification for assigned metavariables.
@@ -108,8 +33,14 @@ class metavar_env {
     typedef splay_map<name, data, name_quick_cmp> name2data;
 
     name_generator     m_name_generator;
-    substitution       m_substitution;
     name2data          m_metavar_data;
+    unsigned           m_size;
+    // If the following flag is true, then beta-reduction is automatically applied
+    // when we apply a substitution containing ?m <- fun (x : T), ...
+    // to an expression containing (?m a)
+    // The motivation is that higher order unification and matching produces a
+    // bunch of assignments of the form ?m <- fun (x : T), ...
+    bool               m_beta_reduce_mv;
     unsigned           m_timestamp;
 
     void inc_timestamp();
@@ -117,6 +48,9 @@ public:
     metavar_env(name const & prefix);
     metavar_env();
 
+    bool beta_reduce_metavar_application() const { return m_beta_reduce_mv; }
+    void set_beta_reduce_metavar_application(bool f) { m_beta_reduce_mv = f; }
+
     friend void swap(metavar_env & a, metavar_env & b);
 
     /**
@@ -195,13 +129,6 @@ public:
     */
     void assign(expr const & m, expr const & t, justification const & j = justification());
 
-    /**
-       \brief Return the set of substitutions.
-    */
-    substitution const & get_substitutions() const { return m_substitution; }
-
-    operator substitution const &() const { return get_substitutions(); }
-
     /**
        \brief Return the substitution associated with the given metavariable
        in this substitution.
@@ -211,14 +138,18 @@ public:
 
        \pre is_metavar(m)
     */
-    expr get_subst(expr const & m) const { return m_substitution.get_subst(m); }
+    expr get_subst(expr const & m) const;
 
     /**
-       \brief Return a unassigned metavariable (if one exists). Only metavariables
-       that have types are considered. Return the anonymous name if all metavariables (with types)
-       are assigned.
+       \brief Apply f to each substitution in the metavariable environment.
     */
-    name find_unassigned_metavar() const;
+    template<typename F>
+    void for_each_subst(F f) const {
+        m_metavar_data.for_each([&](name const & k, data const & d) {
+                if (d.m_subst)
+                    f(k, d.m_subst);
+            });
+    }
 };
 
 void swap(metavar_env & a, metavar_env & b);
@@ -228,23 +159,15 @@ void swap(metavar_env & a, metavar_env & b);
 */
 expr apply_local_context(expr const & a, local_context const & lctx);
 
-class instantiate_metavars_proc : public replace_visitor {
-protected:
-    substitution const & m_subst;
-    virtual expr visit_metavar(expr const & m, context const &);
-    virtual expr visit_app(expr const & e, context const & ctx);
-    // The following method is invoked whenever the visitor instantiates
-    // a metavariable \c m
-    virtual void instantiated_metavar(expr const & m);
-public:
-    instantiate_metavars_proc(substitution const & s);
-};
-
 /**
    \brief Instantiate the metavariables occurring in \c e with the substitutions
-   provided by \c s.
+   provided by \c menv. Store the justification of replace variables in jsts.
 */
-expr instantiate_metavars(expr const & e, substitution const & s);
+expr instantiate_metavars(expr const & e, metavar_env const & menv, buffer<justification> & jsts);
+inline expr instantiate_metavars(expr const & e, metavar_env const & menv) {
+    buffer<justification> tmp;
+    return instantiate_metavars(e, menv, tmp);
+}
 
 /**
     \brief Extend the local context \c lctx with the entry <tt>lift:s:n</tt>
@@ -287,15 +210,15 @@ bool has_local_context(expr const & m);
 expr pop_meta_context(expr const & m);
 
 /**
-   \brief Return true iff \c e has a metavariable that is assigned in \c s.
+   \brief Return true iff \c e has a metavariable that is assigned in \c menv.
 */
-bool has_assigned_metavar(expr const & e, substitution const & s);
+bool has_assigned_metavar(expr const & e, metavar_env const & menv);
 
 /**
    \brief Return true iff \c e contains the metavariable \c m.
-   The substitutions in \c s are taken into account.
+   The substitutions in \c menv are taken into account.
 
    \brief is_metavar(m)
 */
-bool has_metavar(expr const & e, expr const & m, substitution const & s = substitution());
+bool has_metavar(expr const & e, expr const & m, metavar_env const & menv);
 }

src/library/elaborator/elaborator.cpp

@@ -209,7 +209,7 @@ class elaborator::imp {
        The substitutions in the current state are taken into account.
     */
     bool has_metavar(expr const & e, expr const & m) const {
-        return ::lean::has_metavar(e, m, m_state.m_menv.get_substitutions());
+        return ::lean::has_metavar(e, m, m_state.m_menv);
     }
 
     static bool has_metavar(expr const & e) {
@@ -221,15 +221,7 @@ class elaborator::imp {
        the current state.
     */
     bool has_assigned_metavar(expr const & e) const {
-        return ::lean::has_assigned_metavar(e, m_state.m_menv.get_substitutions());
-    }
-
-    /**
-        \brief Return a unassigned metavariable in the current state.
-        Return the anonymous name if the state does not contain unassigned metavariables.
-    */
-    name find_unassigned_metavar() const {
-        return m_state.m_menv.find_unassigned_metavar();
+        return ::lean::has_assigned_metavar(e, m_state.m_menv);
     }
 
     /** \brief Return true if \c a is of the form <tt>(?m ...)</tt> */
@@ -444,7 +436,7 @@ class elaborator::imp {
             justification new_jst(new substitution_justification(c, get_mvar_justification(arg(a, 0))));
             expr new_f = get_mvar_subst(arg(a, 0));
             expr new_a = update_app(a, 0, new_f);
-            if (m_state.m_menv.get_substitutions().beta_reduce_metavar_application())
+            if (m_state.m_menv.beta_reduce_metavar_application())
                 new_a = head_beta_reduce(new_a);
             push_updated_constraint(c, is_lhs, new_a, new_jst);
             return Processed;
@@ -460,27 +452,13 @@ class elaborator::imp {
         }
     }
 
-    class instantiate_metavars_tracking_justifications_proc : public instantiate_metavars_proc {
-        metavar_env &           m_menv;
-        buffer<justification> & m_jsts;
-    protected:
-        virtual void instantiated_metavar(expr const & m) {
-            justification t = m_menv.get_justification(m);
-            if (t)
-                m_jsts.push_back(t);
-        }
-    public:
-        instantiate_metavars_tracking_justifications_proc(metavar_env & menv, buffer<justification> & js):
-            instantiate_metavars_proc(menv.get_substitutions()), m_menv(menv), m_jsts(js) {}
-    };
-
     /**
        \brief Instantiate the assigned metavariables in \c a, and store the justifications
        in \c jsts.
     */
     expr instantiate_metavars(expr const & a, buffer<justification> & jsts) {
         lean_assert(has_assigned_metavar(a));
-        return instantiate_metavars_tracking_justifications_proc(m_state.m_menv, jsts)(a);
+        return ::lean::instantiate_metavars(a, m_state.m_menv, jsts);
     }
 
     /**
@@ -1373,7 +1351,7 @@ public:
         // display(std::cout);
     }
 
-    substitution next() {
+    metavar_env next() {
         check_interrupted(m_interrupted);
         if (m_conflict)
             throw elaborator_exception(m_conflict);
@@ -1395,15 +1373,8 @@ public:
             check_interrupted(m_interrupted);
             cnstr_queue & q = m_state.m_queue;
             if (q.empty() || m_quota < - static_cast<int>(q.size()) - 10) {
-                name m = find_unassigned_metavar();
-                // std::cout << "Queue is empty\n"; display(std::cout); std::cout << "\n\n";
-                if (m) {
-                    // TODO(Leo)
-                    // erase the following line, and implement interface with synthesizer
-                    return m_state.m_menv.get_substitutions();
-                } else {
-                    return m_state.m_menv.get_substitutions();
-                }
+                // TODO(Leo): implement interface with synthesizer
+                return m_state.m_menv;
             } else {
                 unification_constraint c = q.front();
                 // std::cout << "Processing, quota: " << m_quota << ", depth: " << m_case_splits.size() << " "; display(std::cout, c);
@@ -1427,7 +1398,7 @@ public:
     }
 
     void display(std::ostream & out) const {
-        m_state.m_menv.get_substitutions().for_each([&](name const & m, expr const & e) {
+        m_state.m_menv.for_each_subst([&](name const & m, expr const & e) {
                 out << m << " <- " << e << "\n";
             });
         for (auto c : m_state.m_queue)
@@ -1454,7 +1425,7 @@ elaborator::elaborator(environment const & env,
 elaborator::~elaborator() {
 }
 
-substitution elaborator::next() {
+metavar_env elaborator::next() {
     return m_ptr->next();
 }
 

src/library/elaborator/elaborator.h

@@ -60,7 +60,7 @@ public:
 
     ~elaborator();
 
-    substitution next();
+    metavar_env next();
     void interrupt();
     void set_interrupt(bool ) { interrupt(); }
 };

src/library/elaborator/elaborator_justification.cpp

@@ -7,17 +7,6 @@ Author: Leonardo de Moura
 #include "library/elaborator/elaborator_justification.h"
 
 namespace lean {
-static void push_back(buffer<justification_cell*> & r, justification const & t) {
-    if (t)
-        r.push_back(t.raw());
-}
-
-template<typename T>
-static void append(buffer<justification_cell*> & r, T const & s) {
-    for (auto t : s)
-        push_back(r, t);
-}
-
 // -------------------------
 // Propagation justification
 // -------------------------

src/tests/kernel/metavar.cpp

@@ -24,9 +24,9 @@ Author: Leonardo de Moura
 #include "library/all/all.h"
 using namespace lean;
 
-static std::ostream & operator<<(std::ostream & out, substitution const & env) {
+static std::ostream & operator<<(std::ostream & out, metavar_env const & menv) {
     bool first = true;
-    env.for_each([&](name const & n, expr const & v) {
+    menv.for_each_subst([&](name const & n, expr const & v) {
             if (first) first = false; else out << "\n";
             out << "?M" << n << " <- " << v;
         });
@@ -80,7 +80,7 @@ static void tst2() {
     std::cout << instantiate_metavars(m11, menv) << "\n";
     menv.assign(m2, g(a, Var(1)));
     std::cout << instantiate_metavars(h(m11), menv) << "\n";
-    lean_assert(instantiate_metavars(h(m11), menv) == h(f(f(a, g(a, Var(1))))));
+    lean_assert_eq(instantiate_metavars(h(m11), menv), h(f(f(a, g(a, Var(1))))));
 }
 
 static void tst3() {

src/tests/library/elaborator/elaborator.cpp

@@ -55,7 +55,7 @@ static void tst1() {
     ucs.push_back(mk_choice_constraint(context(), m2, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
     ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    elb.next();
 }
 
 static void tst2() {
@@ -97,7 +97,7 @@ static void tst2() {
     ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
     ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    elb.next();
 }
 
 static void tst3() {
@@ -140,7 +140,7 @@ static void tst3() {
     ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
     ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    elb.next();
 }
 
 static void tst4() {
@@ -184,7 +184,7 @@ static void tst4() {
     ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
     ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    elb.next();
 }
 
 static void tst5() {
@@ -225,7 +225,7 @@ static void tst5() {
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
     ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    elb.next();
 }
 
 static void tst6() {
@@ -262,7 +262,7 @@ static void tst6() {
     expr given    = checker.infer_type(V, context(), &menv, ucs);
     ucs.push_back(mk_eq_constraint(context(), expected, given, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    metavar_env s = elb.next();
     std::cout << instantiate_metavars(V, s) << "\n";
 }
 
@@ -275,7 +275,7 @@ static expr elaborate(expr const & e, environment const & env) {
     expr e2 = replace_placeholders_with_metavars(e, menv);
     checker.infer_type(e2, context(), &menv, ucs);
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    metavar_env s = elb.next();
     return instantiate_metavars(e2, s);
 }
 
@@ -832,7 +832,7 @@ void tst26() {
     std::cout << F << "\n";
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    metavar_env s = elb.next();
     std::cout << instantiate_metavars(F, s) << "\n";
     lean_assert_eq(instantiate_metavars(F, s), Eq(g(Type(level()+1), a), a));
 }
@@ -867,7 +867,7 @@ void tst27() {
     std::cout << F << "\n";
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
     elaborator elb(env, menv, ucs.size(), ucs.data());
-    substitution s = elb.next();
+    metavar_env s = elb.next();
     std::cout << instantiate_metavars(F, s) << "\n";
     lean_assert_eq(instantiate_metavars(F, s),
                    Fun({f, TypeM >> TypeM}, eq(TypeM, g(TypeM >> TypeM, f)(a), a)));
@@ -903,4 +903,3 @@ int main() {
     tst27();
     return has_violations() ? 1 : 0;
 }
-

tests/lean/elab1.lean.expected.out

@@ -40,7 +40,7 @@ Failed to solve
                                         Propagate type, ?M3::1 : ?M3::3
                                             Assignment
                                              ⊢ ?M3::1 ≈ λ x : ℕ, x
-                                                assumption 0
+                                                Assumption 0
     Failed to solve
      ⊢ Bool ≺ ℤ
         Substitution
@@ -76,7 +76,7 @@ Failed to solve
                                         Propagate type, ?M3::1 : ?M3::3
                                             Assignment
                                              ⊢ ?M3::1 ≈ nat_to_int
-                                                assumption 1
+                                                Assumption 1
     Failed to solve
      ⊢ Bool ≺ ℝ
         Substitution
@@ -112,7 +112,7 @@ Failed to solve
                                         Propagate type, ?M3::1 : ?M3::3
                                             Assignment
                                              ⊢ ?M3::1 ≈ nat_to_real
-                                                assumption 2
+                                                Assumption 2
   Assumed: g
 Error (line: 7, pos: 8) unexpected metavariable occurrence
   Assumed: h
@@ -169,7 +169,7 @@ Failed to solve
             Propagate type, ?M3::0 : ?M3::1
                 Assignment
                  ⊢ ?M3::0 ≈ Type
-                    assumption 0
+                    Assumption 0
         Failed to solve
          ⊢ Type 1 ≺ Type
             Substitution
@@ -182,7 +182,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 1
-                    assumption 1
+                    Assumption 1
         Failed to solve
          ⊢ Type 2 ≺ Type
             Substitution
@@ -195,7 +195,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 2
-                    assumption 2
+                    Assumption 2
         Failed to solve
          ⊢ Type 3 ≺ Type
             Substitution
@@ -208,7 +208,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 3
-                    assumption 3
+                    Assumption 3
         Failed to solve
          ⊢ Type M ≺ Type
             Substitution
@@ -221,7 +221,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type M
-                    assumption 4
+                    Assumption 4
         Failed to solve
          ⊢ Type U ≺ Type
             Substitution
@@ -234,7 +234,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type U
-                    assumption 5
+                    Assumption 5
     Failed to solve
      ⊢
     (?M3::1 ≈ Type 2) ⊕ (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type 4) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U)
@@ -243,7 +243,7 @@ Failed to solve
             Propagate type, ?M3::0 : ?M3::1
                 Assignment
                  ⊢ ?M3::0 ≈ Type 1
-                    assumption 6
+                    Assumption 6
         Failed to solve
          ⊢ Type 2 ≺ Type
             Substitution
@@ -256,7 +256,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 2
-                    assumption 7
+                    Assumption 7
         Failed to solve
          ⊢ Type 3 ≺ Type
             Substitution
@@ -269,7 +269,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 3
-                    assumption 8
+                    Assumption 8
         Failed to solve
          ⊢ Type 4 ≺ Type
             Substitution
@@ -282,7 +282,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 4
-                    assumption 9
+                    Assumption 9
         Failed to solve
          ⊢ Type M ≺ Type
             Substitution
@@ -295,7 +295,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type M
-                    assumption 10
+                    Assumption 10
         Failed to solve
          ⊢ Type U ≺ Type
             Substitution
@@ -308,7 +308,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type U
-                    assumption 11
+                    Assumption 11
     Failed to solve
      ⊢
     (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type 4) ⊕ (?M3::1 ≈ Type 5) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U)
@@ -317,7 +317,7 @@ Failed to solve
             Propagate type, ?M3::0 : ?M3::1
                 Assignment
                  ⊢ ?M3::0 ≈ Type 2
-                    assumption 12
+                    Assumption 12
         Failed to solve
          ⊢ Type 3 ≺ Type
             Substitution
@@ -330,7 +330,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 3
-                    assumption 13
+                    Assumption 13
         Failed to solve
          ⊢ Type 4 ≺ Type
             Substitution
@@ -343,7 +343,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 4
-                    assumption 14
+                    Assumption 14
         Failed to solve
          ⊢ Type 5 ≺ Type
             Substitution
@@ -356,7 +356,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type 5
-                    assumption 15
+                    Assumption 15
         Failed to solve
          ⊢ Type M ≺ Type
             Substitution
@@ -369,7 +369,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type M
-                    assumption 16
+                    Assumption 16
         Failed to solve
          ⊢ Type U ≺ Type
             Substitution
@@ -382,7 +382,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type U
-                    assumption 17
+                    Assumption 17
     Failed to solve
      ⊢
     (?M3::1 ≈ Type M+1) ⊕
@@ -395,7 +395,7 @@ Failed to solve
             Propagate type, ?M3::0 : ?M3::1
                 Assignment
                  ⊢ ?M3::0 ≈ Type M
-                    assumption 18
+                    Assumption 18
         Failed to solve
          ⊢ Type M+1 ≺ Type
             Substitution
@@ -408,7 +408,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type M+1
-                    assumption 19
+                    Assumption 19
         Failed to solve
          ⊢ Type M+2 ≺ Type
             Substitution
@@ -421,7 +421,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type M+2
-                    assumption 20
+                    Assumption 20
         Failed to solve
          ⊢ Type M+3 ≺ Type
             Substitution
@@ -434,7 +434,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type M+3
-                    assumption 21
+                    Assumption 21
         Failed to solve
          ⊢ Type M ≺ Type
             Substitution
@@ -447,7 +447,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type M
-                    assumption 22
+                    Assumption 22
         Failed to solve
          ⊢ Type U ≺ Type
             Substitution
@@ -460,7 +460,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type U
-                    assumption 23
+                    Assumption 23
     Failed to solve
      ⊢
     (?M3::1 ≈ Type U+1) ⊕
@@ -473,7 +473,7 @@ Failed to solve
             Propagate type, ?M3::0 : ?M3::1
                 Assignment
                  ⊢ ?M3::0 ≈ Type U
-                    assumption 24
+                    Assumption 24
         Failed to solve
          ⊢ Type U+1 ≺ Type
             Substitution
@@ -486,7 +486,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type U+1
-                    assumption 25
+                    Assumption 25
         Failed to solve
          ⊢ Type U+2 ≺ Type
             Substitution
@@ -499,7 +499,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type U+2
-                    assumption 26
+                    Assumption 26
         Failed to solve
          ⊢ Type U+3 ≺ Type
             Substitution
@@ -512,7 +512,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type U+3
-                    assumption 27
+                    Assumption 27
         Failed to solve
          ⊢ Type M ≺ Type
             Substitution
@@ -525,7 +525,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type M
-                    assumption 28
+                    Assumption 28
         Failed to solve
          ⊢ Type U ≺ Type
             Substitution
@@ -538,7 +538,7 @@ Failed to solve
                     Bool
                 Assignment
                  ⊢ ?M3::1 ≈ Type U
-                    assumption 29
+                    Assumption 29
 Failed to solve
 a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≺ if Bool (if Bool a b ⊤) a ⊤
     Substitution
@@ -627,14 +627,25 @@ a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≺ if Bool (if Bool a b ⊤
                                 EM a
                                 λ H_a : ?M3::6, H
                                 λ H_na : ?M3::7, NotImp1 (MT H H_na)
-                        Assignment
-                        a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0
-                            Destruct/Decompose
-                            a : Bool, b : Bool ⊢ Π H : ?M3::2, ?M3::5 ≺ Π _ : ?M3::0, ?M3::1[lift:0:1]
-                                (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
-                                    Discharge::explicit
-                                with arguments:
-                                    ?M3::0
-                                    ?M3::1
-                                    λ H : ?M3::2,
-                                      DisjCases (EM a) (λ H_a : ?M3::6, H) (λ H_na : ?M3::7, NotImp1 (MT H H_na))
+                         Normalize assignment
+                            ?M3::0
+                            Assignment
+                            a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0
+                                Destruct/Decompose
+                                a : Bool, b : Bool ⊢ Π H : ?M3::2, ?M3::5 ≺ Π _ : ?M3::0, ?M3::1[lift:0:1]
+                                    (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
+                                        Discharge::explicit
+                                    with arguments:
+                                        ?M3::0
+                                        ?M3::1
+                                        λ H : ?M3::2,
+                                          DisjCases (EM a) (λ H_a : ?M3::6, H) (λ H_na : ?M3::7, NotImp1 (MT H H_na))
+                            Assignment
+                            a : Bool, b : Bool ⊢ ?M3::0 ≈ (a ⇒ b) ⇒ a
+                                Destruct/Decompose
+                                a : Bool, b : Bool ⊢ ?M3::0 ⇒ ?M3::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
+                                    Destruct/Decompose
+                                    a : Bool ⊢ Π b : Bool, ?M3::0 ⇒ ?M3::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
+                                        Destruct/Decompose
+                                         ⊢ Π a b : Bool, ?M3::0 ⇒ ?M3::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
+                                            (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.

tests/lean/overload2.lean.expected.out

@@ -36,7 +36,7 @@ Failed to solve
                                             Propagate type, ?M3::0 : ?M3::2
                                                 Assignment
                                                  ⊢ ?M3::0 ≈ Nat::add
-                                                    assumption 0
+                                                    Assumption 0
     Failed to solve
      ⊢ Bool ≺ ℤ
         Substitution
@@ -69,7 +69,7 @@ Failed to solve
                                             Propagate type, ?M3::0 : ?M3::2
                                                 Assignment
                                                  ⊢ ?M3::0 ≈ Int::add
-                                                    assumption 2
+                                                    Assumption 2
     Failed to solve
      ⊢ Bool ≺ ℝ
         Substitution
@@ -102,7 +102,7 @@ Failed to solve
                                             Propagate type, ?M3::0 : ?M3::2
                                                 Assignment
                                                  ⊢ ?M3::0 ≈ Real::add
-                                                    assumption 5
+                                                    Assumption 5
   Assumed: R
   Assumed: T
   Assumed: r2t