refactor(kernel): constraints

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

src/kernel/CMakeLists.txt

@@ -3,8 +3,8 @@ for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
 instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
 object.cpp environment.cpp replace_visitor.cpp io_state.cpp
 normalizer.cpp justification.cpp pos_info_provider.cpp metavar.cpp
+constraint.cpp
 # type_checker.cpp
-#  unification_constraint.cpp
 # type_checker_justification.cpp
 )
 

src/kernel/constraint.cpp

@@ -0,0 +1,140 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/rc.h"
+#include "kernel/constraint.h"
+namespace lean {
+struct constraint_cell {
+    void dealloc();
+    MK_LEAN_RC()
+    constraint_kind m_kind;
+    unsigned        m_hash;
+    justification   m_jst;
+    constraint_cell(constraint_kind k, unsigned h, justification const & j):m_rc(1), m_kind(k), m_hash(h), m_jst(j) {}
+};
+struct eqc_constraint_cell : public constraint_cell {
+    expr m_lhs;
+    expr m_rhs;
+    eqc_constraint_cell(constraint_kind k, expr const & lhs, expr const & rhs, justification const & j):
+        constraint_cell(k, hash(hash(lhs.hash(), rhs.hash()), static_cast<unsigned>(k)), j),
+        m_lhs(lhs), m_rhs(rhs) {}
+};
+struct level_constraint_cell : public constraint_cell {
+    level m_lhs;
+    level m_rhs;
+    level_constraint_cell(level const & lhs, level const & rhs, justification const & j):
+        constraint_cell(constraint_kind::Level, hash(hash(lhs), hash(rhs)), j),
+        m_lhs(lhs), m_rhs(rhs) {}
+};
+static unsigned hash(list<expr> const & ls) {
+    return is_nil(ls) ? 17 : hash(car(ls).hash(), hash(cdr(ls)));
+}
+struct choice_constraint_cell : public constraint_cell {
+    expr       m_expr;
+    list<expr> m_choices;
+    choice_constraint_cell(expr const & e, list<expr> const & s, justification const & j):
+        constraint_cell(constraint_kind::Choice, hash(e.hash(), hash(s)), j),
+        m_expr(e), m_choices(s) {}
+};
+
+constraint::constraint(constraint_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); }
+constraint::constraint(constraint const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+constraint::constraint(constraint && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+constraint::~constraint() { if (m_ptr) m_ptr->dec_ref(); }
+constraint & constraint::operator=(constraint const & c) { LEAN_COPY_REF(c); }
+constraint & constraint::operator=(constraint && c) { LEAN_MOVE_REF(c); }
+constraint_kind constraint::kind() const { lean_assert(m_ptr); return m_ptr->m_kind; }
+unsigned constraint::hash() const { lean_assert(m_ptr); return m_ptr->m_hash; }
+justification const & constraint::get_justification() const { lean_assert(m_ptr); return m_ptr->m_jst; }
+
+constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+    return constraint(new eqc_constraint_cell(constraint_kind::Eq, lhs, rhs, j));
+}
+constraint mk_conv_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+    return constraint(new eqc_constraint_cell(constraint_kind::Convertible, lhs, rhs, j));
+}
+constraint mk_level_cnstr(level const & lhs, level const & rhs, justification const & j) {
+    return constraint(new level_constraint_cell(lhs, rhs, j));
+}
+constraint mk_choice_cnstr(expr const & t, list<expr> const & s, justification const & j) {
+    return constraint(new choice_constraint_cell(t, s, j));
+}
+
+bool operator==(constraint const & c1, constraint const & c2) {
+    if (c1.kind() != c2.kind() || c1.hash() != c2.hash())
+        return false;
+    switch (c1.kind()) {
+    case constraint_kind::Eq: case constraint_kind::Convertible:
+        return cnstr_lhs_expr(c1) == cnstr_lhs_expr(c2) && cnstr_rhs_expr(c1) == cnstr_rhs_expr(c2);
+    case constraint_kind::Level:
+        return cnstr_lhs_level(c1) == cnstr_lhs_level(c2) && cnstr_rhs_level(c1) == cnstr_rhs_level(c2);
+    case constraint_kind::Choice:
+        return
+            cnstr_choice_expr(c1) == cnstr_choice_expr(c2) &&
+            compare(cnstr_choice_set(c1), cnstr_choice_set(c2), [](expr const & e1, expr const & e2) { return e1 == e2; });
+    }
+}
+
+expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eqc_cnstr(c)); return static_cast<eqc_constraint_cell*>(c.raw())->m_lhs; }
+expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eqc_cnstr(c)); return static_cast<eqc_constraint_cell*>(c.raw())->m_rhs; }
+level const & cnstr_lhs_level(constraint const & c) {
+    lean_assert(is_level_cnstr(c)); return static_cast<level_constraint_cell*>(c.raw())->m_lhs;
+}
+level const & cnstr_rhs_level(constraint const & c) {
+    lean_assert(is_level_cnstr(c)); return static_cast<level_constraint_cell*>(c.raw())->m_rhs;
+}
+expr const & cnstr_choice_expr(constraint const & c) {
+    lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_expr;
+}
+list<expr> const & cnstr_choice_set(constraint const & c) {
+    lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_choices;
+}
+
+constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst) {
+    lean_assert(is_eqc_cnstr(c));
+    if (!is_eqp(cnstr_lhs_expr(c), new_lhs) || !is_eqp(cnstr_rhs_expr(c), new_rhs)) {
+        if (is_eq_cnstr(c))
+            return mk_eq_cnstr(new_lhs, new_rhs, new_jst);
+        else
+            return mk_conv_cnstr(new_lhs, new_rhs, new_jst);
+    } else {
+        return c;
+    }
+}
+constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs) {
+    return updt_eqc_cnstr(c, new_lhs, new_rhs, c.get_justification());
+}
+constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level const & new_rhs, justification const & new_jst) {
+    lean_assert(is_level_cnstr(c));
+    if (!is_eqp(cnstr_lhs_level(c), new_lhs) || !is_eqp(cnstr_rhs_level(c), new_rhs))
+        return mk_level_cnstr(new_lhs, new_rhs, new_jst);
+    else
+        return c;
+}
+constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level const & new_rhs) {
+    return updt_level_cnstr(c, new_lhs, new_rhs, c.get_justification());
+}
+
+std::ostream & operator<<(std::ostream & out, constraint const & c) {
+    switch (c.kind()) {
+    case constraint_kind::Eq:
+        out << cnstr_lhs_expr(c) << " ≈ " << cnstr_rhs_expr(c);
+    case constraint_kind::Convertible:
+        out << cnstr_lhs_expr(c) << " ↠ " << cnstr_rhs_expr(c);
+    case constraint_kind::Level:
+        out << cnstr_lhs_level(c) << " ≤ " << cnstr_rhs_level(c);
+    case constraint_kind::Choice:
+        out << cnstr_choice_expr(c) << " ∊ {";
+        bool first = true;
+        for (expr const & e : cnstr_choice_set(c)) {
+            if (first) first = false; else out << ", ";
+            out << e;
+        }
+        out << "}";
+    }
+    return out;
+}
+}

src/kernel/constraint.h

@@ -0,0 +1,97 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+#include "kernel/justification.h"
+namespace lean {
+/**
+   \brief The lean kernel type checker produces three kinds of constraints:
+
+   - Equality constraint:          t ≈ s
+        The terms t and s must be definitionally equal.
+   - Convertability constraint:    t ↠ s
+        The term t must be convertible to s
+   - Universe level constaint:     l ≤ m
+        The universe level l must be less than or equal to m.
+
+   \remark The first two kinds are only generated if the input term
+   contains metavariables.
+
+   Each constraint is associated with a justification object.
+
+   Finally, we also include a choice constraint. The choice is an auxiliary
+   constraint used to implement overloading and coercions in Lean.
+   This constraint is not generated by the kernel.
+   A choice constraint has the form:
+             t ∊ {s_1, ..., s_k}
+   It means, t must be definitionally equal to one of the terms in the (finite)
+   set {s_1, ..., s_k}.
+*/
+enum constraint_kind { Eq, Convertible, Level, Choice };
+struct constraint_cell;
+class constraint {
+    constraint_cell * m_ptr;
+    constraint(constraint_cell * ptr);
+public:
+    constraint(constraint const & c);
+    constraint(constraint && s);
+    ~constraint();
+
+    constraint_kind kind() const;
+    unsigned hash() const;
+    justification const & get_justification() const;
+
+    constraint & operator=(constraint const & c);
+    constraint & operator=(constraint && c);
+
+    friend bool is_eqp(constraint const & c1, constraint const & c2) { return c1.m_ptr == c2.m_ptr; }
+    friend void swap(constraint & l1, constraint & l2) { std::swap(l1, l2); }
+
+    friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+    friend constraint mk_conv_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+    friend constraint mk_level_cnstr(level const & lhs, level const & rhs, justification const & j);
+    friend constraint mk_choice_cnstr(expr const & t, list<expr> const & s, justification const & j);
+
+    constraint_cell * raw() const { return m_ptr; }
+};
+
+bool operator==(constraint const & c1, constraint const & c2);
+inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); }
+
+bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
+bool is_conv_cnstr(constraint const & c) { return c.kind() == constraint_kind::Convertible; }
+bool is_level_cnstr(constraint const & c) { return c.kind() == constraint_kind::Level; }
+bool is_choice_cnstr(constraint const & c) { return c.kind() == constraint_kind::Choice; }
+bool is_eqc_cnstr(constraint const & c) { return is_eq_cnstr(c) || is_conv_cnstr(c); }
+
+/** \brief Return the lhs of an equality/convertability constraint. */
+expr const & cnstr_lhs_expr(constraint const & c);
+/** \brief Return the rhs of an equality/convertability constraint. */
+expr const & cnstr_rhs_expr(constraint const & c);
+/** \brief Return the lhs of an level constraint. */
+level const & cnstr_lhs_level(constraint const & c);
+/** \brief Return the rhs of an level constraint. */
+level const & cnstr_rhs_level(constraint const & c);
+/** \brief Return the main term a choice constraint. */
+expr const & cnstr_choice_expr(constraint const & c);
+/** \brief Return the choice set of a choice constraint. */
+list<expr> const & cnstr_choice_set(constraint const & c);
+
+/** \brief Update equality/convertability constraint c with new_lhs, new_rhs and justification. */
+constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst);
+/** \brief Update equality/convertability constraint c with new_lhs and new_rhs, but keeping the same justification. */
+constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs);
+/** \brief Update level constraint c with new_lhs, new_rhs and justification. */
+constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level const & new_rhs, justification const & new_jst);
+/** \brief Update level constraint c with new_lhs and new_rhs, but keeping the same justification. */
+constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level const & new_rhs);
+
+/** \brief Printer for debugging purposes */
+std::ostream & operator<<(std::ostream & out, constraint const & c);
+
+typedef list<constraint> constraints;
+}

src/kernel/unification_constraint.cpp

@@ -1,174 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/unification_constraint.h"
-#include "kernel/metavar.h"
-
-namespace lean {
-unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j):
-    m_kind(k), m_ctx(c), m_justification(j), m_rc(1) {
-}
-unification_constraint_cell::~unification_constraint_cell() {
-}
-void unification_constraint_cell::dealloc() {
-    delete this;
-}
-
-static format add_context(formatter const & fmt, options const & opts, context const & ctx, format const & body, optional<metavar_env> const & menv) {
-    bool unicode     = get_pp_unicode(opts);
-    format ctx_fmt   = fmt(instantiate_metavars(menv, ctx), opts);
-    format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
-    return group(format{ctx_fmt, space(), turnstile, line(), body});
-}
-
-static format add_justification(formatter const & fmt, options const & opts, format const & body, justification const & jst, pos_info_provider const * p, bool include_justification, optional<metavar_env> const & menv) {
-    if (jst && include_justification) {
-        unsigned indent  = get_pp_indent(opts);
-        return format{body, line(), format("Justification:"), nest(indent, compose(line(), jst.pp(fmt, opts, p, true, menv)))};
-    } else {
-        return body;
-    }
-}
-
-static format mk_binary(formatter const & fmt, options const & opts, context const & ctx, expr const & lhs, expr const & rhs, format const & op,
-                        optional<metavar_env> const & menv) {
-    format lhs_fmt  = fmt(ctx, instantiate_metavars(menv, lhs), false, opts);
-    format rhs_fmt  = fmt(ctx, instantiate_metavars(menv, rhs), false, opts);
-    return group(format{lhs_fmt, space(), op, line(), rhs_fmt});
-}
-
-static format mk_unification_op(options const & opts) {
-    bool unicode = get_pp_unicode(opts);
-    return unicode ? format("\u2248") /* ≈ */ : format("=?=");
-}
-
-unification_constraint_eq::unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, justification const & j):
-    unification_constraint_cell(unification_constraint_kind::Eq, c, j),
-    m_lhs(lhs),
-    m_rhs(rhs) {
-}
-
-unification_constraint_eq::~unification_constraint_eq() {
-}
-
-format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                                     optional<metavar_env> const & menv) const {
-    format op   = mk_unification_op(opts);
-    format body = mk_binary(fmt, opts, m_ctx, m_lhs, m_rhs, op, menv);
-    body = add_context(fmt, opts, m_ctx, body, menv);
-    return add_justification(fmt, opts, body, m_justification, p, include_justification, menv);
-}
-
-unification_constraint unification_constraint_eq::updt_justification(justification const & j) const {
-    return mk_eq_constraint(m_ctx, m_lhs, m_rhs, j);
-}
-
-unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j):
-    unification_constraint_cell(unification_constraint_kind::Convertible, c, j),
-    m_from(from),
-    m_to(to) {
-}
-
-unification_constraint_convertible::~unification_constraint_convertible() {
-}
-
-format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p,
-                                              bool include_justification, optional<metavar_env> const & menv) const {
-    bool unicode = get_pp_unicode(opts);
-    format op    = unicode ? format("\u227A") /* ≺ */ : format("<<");
-    format body  = mk_binary(fmt, opts, m_ctx, m_from, m_to, op, menv);
-    body = add_context(fmt, opts, m_ctx, body, menv);
-    return add_justification(fmt, opts, body, m_justification, p, include_justification, menv);
-}
-
-unification_constraint unification_constraint_convertible::updt_justification(justification const & j) const {
-    return mk_convertible_constraint(m_ctx, m_from, m_to, j);
-}
-
-unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j):
-    unification_constraint_cell(unification_constraint_kind::Max, c, j),
-    m_lhs1(lhs1),
-    m_lhs2(lhs2),
-    m_rhs(rhs) {
-}
-
-unification_constraint_max::~unification_constraint_max() {
-}
-
-format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                                      optional<metavar_env> const & menv) const {
-    format op       = mk_unification_op(opts);
-    format lhs1_fmt = fmt(m_ctx, instantiate_metavars(menv, m_lhs1), false, opts);
-    format lhs2_fmt = fmt(m_ctx, instantiate_metavars(menv, m_lhs2), false, opts);
-    format rhs_fmt  = fmt(m_ctx, instantiate_metavars(menv, m_rhs), false, opts);
-    format body     = group(format{format("max"), lp(), lhs1_fmt, comma(), nest(4, compose(line(), lhs2_fmt)), rp(), space(), op, line(), rhs_fmt});
-    body = add_context(fmt, opts, m_ctx, body, menv);
-    return add_justification(fmt, opts, body, m_justification, p, include_justification, menv);
-}
-
-unification_constraint unification_constraint_max::updt_justification(justification const & j) const {
-    return mk_max_constraint(m_ctx, m_lhs1, m_lhs2, m_rhs, j);
-}
-
-unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j):
-    unification_constraint_cell(unification_constraint_kind::Choice, c, j),
-    m_mvar(mvar),
-    m_choices(choices, choices + num) {
-}
-
-unification_constraint_choice::~unification_constraint_choice() {
-}
-
-format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                                         optional<metavar_env> const & menv) const {
-    bool unicode    = get_pp_unicode(opts);
-    format m_fmt    = fmt(m_ctx, m_mvar, false, opts);
-    format eq_op    = mk_unification_op(opts);
-    format or_op    = unicode ? format("\u2295") : format("OR");
-    format body;
-    for (unsigned i = 0; i < m_choices.size(); i++) {
-        body += group(paren(format{m_fmt, space(), eq_op, compose(line(), fmt(m_ctx, instantiate_metavars(menv, m_choices[i]), false, opts))}));
-        if (i + 1 < m_choices.size())
-            body += format{space(), or_op, line()};
-    }
-    body = group(body);
-    body = add_context(fmt, opts, m_ctx, body, menv);
-    return add_justification(fmt, opts, body, m_justification, p, include_justification, menv);
-}
-
-unification_constraint unification_constraint_choice::updt_justification(justification const & j) const {
-    return mk_choice_constraint(m_ctx, m_mvar, m_choices.size(), m_choices.data(), j);
-}
-
-format unification_constraint::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                                  optional<metavar_env> const & menv) const {
-    return m_ptr->pp(fmt, opts, p, include_justification, menv);
-}
-
-format unification_constraint::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
-    return pp(fmt, opts, p, include_justification, optional<metavar_env>());
-}
-
-unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j) {
-    return unification_constraint(new unification_constraint_eq(c, lhs, rhs, j));
-}
-
-unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j) {
-    return unification_constraint(new unification_constraint_convertible(c, from, to, j));
-}
-
-unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j) {
-    return unification_constraint(new unification_constraint_max(c, lhs1, lhs2, rhs, j));
-}
-
-unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j) {
-    return unification_constraint(new unification_constraint_choice(c, mvar, num, choices, j));
-}
-
-unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, justification const & j) {
-    return mk_choice_constraint(c, mvar, choices.size(), choices.begin(), j);
-}
-}

src/kernel/unification_constraint.h

@@ -1,214 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <algorithm>
-#include <vector>
-#include "kernel/expr.h"
-#include "kernel/context.h"
-#include "kernel/justification.h"
-
-namespace lean {
-class metavar_env;
-class unification_constraint;
-/**
-   \brief There are four kinds of unification constraints in Lean
-
-   1-  ctx |- t == s                         t is (definitionally) equal to s
-   2-  ctx |- t << s                         t is convertible to s (this is weaker than equality)
-   3-  ctx |- max(t1, t2) == s               The maximum of t1 and t2 is equal to s, if t2 is Bool, then s is Bool.
-   4-  ctx |- ?m == t_1 Or ... Or ?m == t_k  The metavariable ?m is equal to t_1, ..., or t_k
-
-   \remark The constraint <tt>ctx |- t == s</tt> implies that <tt>ctx |- t << s</tt>, but
-   the converse is not true. Example: <tt>ctx |- Type 1 << Type 2</tt>, but
-   we don't have <tt>ctx |- Type 1 == Type 2</tt>.
-
-   \remark In the max constraint, \c t1 and \c t2 must be eventually unifiable with a Type term or Bool.
-   For example, assume the constraint <tt>ctx |- max(?m1, Type 1) == ?m2</tt>. Now, suppose
-   <tt>?m2</tt> is assigned to <tt>Type 1</tt>. Then, <tt>?m1</tt> can be assigned to <tt>Type 0</tt>
-   or <tt>Type 1</tt>.
-
-   \remark The max constraint is produced when type checking Pi expressions of the form (Pi x : A, B),
-   and the type of A is t1 and the type of B is t2. So, if t2 == Bool, then max(t1, t2) == Bool
-*/
-enum class unification_constraint_kind { Eq, Convertible, Max, Choice };
-
-/**
-   \brief Base class for all Lean unification constraints.
-*/
-class unification_constraint_cell {
-protected:
-    unification_constraint_kind m_kind;
-    context                     m_ctx;
-    justification               m_justification; //!< justification for this constraint
-    MK_LEAN_RC();
-    void dealloc();
-public:
-    unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j);
-    virtual ~unification_constraint_cell();
-    unification_constraint_kind kind() const { return m_kind; }
-    justification const & get_justification() const { return m_justification; }
-    context const & get_context() const { return m_ctx; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                      optional<metavar_env> const & menv) const = 0;
-    void set_justification(justification const & j) { lean_assert(!m_justification); m_justification = j; }
-    /** \brief Return a new constraint equal to this one, but with the new justification */
-    virtual unification_constraint updt_justification(justification const & j) const = 0;
-};
-
-class unification_constraint_eq;
-class unification_constraint_convertible;
-class unification_constraint_max;
-class unification_constraint_choice;
-
-class unification_constraint {
-private:
-    unification_constraint_cell * m_ptr;
-    explicit unification_constraint(unification_constraint_cell * ptr):m_ptr(ptr) {}
-public:
-    unification_constraint(unification_constraint const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    unification_constraint(unification_constraint && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
-    ~unification_constraint() { if (m_ptr) m_ptr->dec_ref(); }
-
-    friend void swap(unification_constraint & a, unification_constraint & b) { std::swap(a.m_ptr, b.m_ptr); }
-
-    unification_constraint & operator=(unification_constraint const & s) { LEAN_COPY_REF(s); }
-    unification_constraint & operator=(unification_constraint && s) { LEAN_MOVE_REF(s); }
-
-    unification_constraint_kind kind() const { return m_ptr->kind(); }
-
-    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-              optional<metavar_env> const & menv) const;
-    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const;
-    justification const & get_justification() const { return m_ptr->get_justification(); }
-    void set_justification(justification const & j) { lean_assert(!get_justification()); lean_assert(m_ptr); m_ptr->set_justification(j); }
-
-    context const & get_context() const { return m_ptr->get_context(); }
-
-    virtual unification_constraint updt_justification(justification const & j) const { lean_assert(m_ptr); return m_ptr->updt_justification(j); }
-
-    friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j);
-    friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j);
-    friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
-    friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
-
-    friend unification_constraint_eq * to_eq(unification_constraint const & c);
-    friend unification_constraint_convertible * to_convertible(unification_constraint const & c);
-    friend unification_constraint_max * to_max(unification_constraint const & c);
-    friend unification_constraint_choice * to_choice(unification_constraint const & c);
-};
-
-/**
-   \brief Unification constraint of the form <tt>ctx |- lhs == rhs</tt>
-*/
-class unification_constraint_eq : public unification_constraint_cell {
-    expr m_lhs;
-    expr m_rhs;
-public:
-    unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, justification const & j);
-    virtual ~unification_constraint_eq();
-    expr const & get_lhs() const { return m_lhs; }
-    expr const & get_rhs() const { return m_rhs; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                      optional<metavar_env> const & menv) const;
-    virtual unification_constraint updt_justification(justification const & j) const;
-};
-
-/**
-   \brief Unification constraint of the form <tt>ctx |- from << to</tt>.
-   The meaning is \c from is convertible to \c to. Example: <tt>ctx |- Type 1 << Type 2</tt>.
-   It is weaker than <tt>ctx |- from == rhs</tt>.
-*/
-class unification_constraint_convertible : public unification_constraint_cell {
-    expr m_from;
-    expr m_to;
-public:
-    unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j);
-    virtual ~unification_constraint_convertible();
-    expr const & get_from() const { return m_from; }
-    expr const & get_to() const   { return m_to; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                      optional<metavar_env> const & menv) const;
-    virtual unification_constraint updt_justification(justification const & j) const;
-};
-
-/**
-   \brief Unification constraint of the form <tt>ctx |- max(lhs1, lhs2) == rhs</tt>.
-*/
-class unification_constraint_max : public unification_constraint_cell {
-    expr m_lhs1;
-    expr m_lhs2;
-    expr m_rhs;
-public:
-    unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
-    virtual ~unification_constraint_max();
-    expr const & get_lhs1() const { return m_lhs1; }
-    expr const & get_lhs2() const { return m_lhs2; }
-    expr const & get_rhs() const  { return m_rhs; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                      optional<metavar_env> const & menv) const;
-    virtual unification_constraint updt_justification(justification const & j) const;
-};
-
-/**
-   \brief Unification constraint of the form <tt>ctx |- mvar == choices[0] OR ... OR mvar == choices[size-1]</tt>.
-*/
-class unification_constraint_choice : public unification_constraint_cell {
-    expr              m_mvar;
-    std::vector<expr> m_choices;
-public:
-    unification_constraint_choice(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
-    virtual ~unification_constraint_choice();
-    expr const & get_mvar() const               { return m_mvar; }
-    unsigned     get_num_choices() const        { return m_choices.size(); }
-    expr const & get_choice(unsigned idx) const { return m_choices[idx]; }
-    std::vector<expr>::const_iterator begin_choices() const { return m_choices.begin(); }
-    std::vector<expr>::const_iterator end_choices() const   { return m_choices.end(); }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification,
-                      optional<metavar_env> const & menv) const;
-    virtual unification_constraint updt_justification(justification const & j) const;
-};
-
-unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j);
-unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j);
-unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
-unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
-unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, justification const & j);
-
-inline bool is_eq(unification_constraint const & c)          { return c.kind() == unification_constraint_kind::Eq; }
-inline bool is_convertible(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Convertible; }
-inline bool is_max(unification_constraint const & c)         { return c.kind() == unification_constraint_kind::Max; }
-inline bool is_choice(unification_constraint const & c)      { return c.kind() == unification_constraint_kind::Choice; }
-
-inline unification_constraint_eq * to_eq(unification_constraint const & c) {
-    lean_assert(is_eq(c)); return static_cast<unification_constraint_eq*>(c.m_ptr);
-}
-
-inline unification_constraint_convertible * to_convertible(unification_constraint const & c) {
-    lean_assert(is_convertible(c)); return static_cast<unification_constraint_convertible*>(c.m_ptr);
-}
-
-inline unification_constraint_max * to_max(unification_constraint const & c) {
-    lean_assert(is_max(c)); return static_cast<unification_constraint_max*>(c.m_ptr);
-}
-
-inline unification_constraint_choice * to_choice(unification_constraint const & c) {
-    lean_assert(is_choice(c)); return static_cast<unification_constraint_choice*>(c.m_ptr);
-}
-
-inline context const & get_context(unification_constraint const & c) { return c.get_context(); }
-inline justification   const & get_justification(unification_constraint const & c) { return c.get_justification(); }
-inline expr const & eq_lhs(unification_constraint const & c) { return to_eq(c)->get_lhs(); }
-inline expr const & eq_rhs(unification_constraint const & c) { return to_eq(c)->get_rhs(); }
-inline expr const & convertible_from(unification_constraint const & c) { return to_convertible(c)->get_from(); }
-inline expr const & convertible_to(unification_constraint const & c) { return to_convertible(c)->get_to(); }
-inline expr const & max_lhs1(unification_constraint const & c) { return to_max(c)->get_lhs1(); }
-inline expr const & max_lhs2(unification_constraint const & c) { return to_max(c)->get_lhs2(); }
-inline expr const & max_rhs(unification_constraint const & c) { return to_max(c)->get_rhs(); }
-inline expr const & choice_mvar(unification_constraint const & c) { return to_choice(c)->get_mvar(); }
-inline unsigned     choice_size(unification_constraint const & c) { return to_choice(c)->get_num_choices(); }
-inline expr const & choice_ith(unification_constraint const & c, unsigned i) { return to_choice(c)->get_choice(i); }
-}