refactor(kernel/constraint): simplify constraint interface, and add choice constraint

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

src/kernel/constraint.cpp

@@ -11,24 +11,30 @@ 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) {}
+    constraint_cell(constraint_kind k, justification const & j):m_rc(1), m_kind(k), m_jst(j) {}
 };
 struct eq_constraint_cell : public constraint_cell {
     expr m_lhs;
     expr m_rhs;
     eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j):
-        constraint_cell(constraint_kind::Eq, hash(lhs.hash(), rhs.hash()), j),
+        constraint_cell(constraint_kind::Eq, 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),
+        constraint_cell(constraint_kind::Level, j),
         m_lhs(lhs), m_rhs(rhs) {}
 };
+struct choice_constraint_cell : public constraint_cell {
+    expr      m_mvar;
+    choice_fn m_fn;
+    choice_constraint_cell(expr const & mvar, choice_fn const & fn, justification const & j):
+        constraint_cell(constraint_kind::Choice, j),
+        m_mvar(mvar), m_fn(fn) {}
+};
 
 void constraint_cell::dealloc() {
     switch (m_kind) {
@@ -36,6 +42,8 @@ void constraint_cell::dealloc() {
         delete static_cast<eq_constraint_cell*>(this); break;
     case constraint_kind::Level:
         delete static_cast<level_constraint_cell*>(this); break;
+    case constraint_kind::Choice:
+        delete static_cast<choice_constraint_cell*>(this); break;
     }
 }
 
@@ -46,7 +54,6 @@ 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) {
@@ -55,23 +62,19 @@ constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const &
 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 & m, choice_fn const & fn, justification const & j) {
-bool operator==(constraint const & c1, constraint const & c2) {
+    lean_assert(is_meta(m));
-    if (c1.kind() != c2.kind() || c1.hash() != c2.hash())
+    return constraint(new choice_constraint_cell(m, fn, j));
-        return false;
-    switch (c1.kind()) {
-    case constraint_kind::Eq:
-        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);
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_lhs; }
 expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_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_mvar(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_mvar; }
+choice_fn const & cnstr_choice_fn(constraint const & c) {
+    lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_fn;
+}
 
 constraint updt_eq_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst) {
     lean_assert(is_eq_cnstr(c));
@@ -102,6 +105,9 @@ std::ostream & operator<<(std::ostream & out, constraint const & c) {
     case constraint_kind::Level:
         out << cnstr_lhs_level(c) << " = " << cnstr_rhs_level(c);
         break;
+    case constraint_kind::Choice:
+        out << "choice " << cnstr_mvar(c);
+        break;
     }
     return out;
 }

src/kernel/constraint.h

@@ -6,8 +6,13 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <algorithm>
+#include "util/lazy_list.h"
+#include "util/list.h"
+#include "util/name_generator.h"
 #include "kernel/expr.h"
 #include "kernel/justification.h"
+#include "kernel/metavar.h"
+
 namespace lean {
 /**
    \brief The lean kernel type checker produces two kinds of constraints:
@@ -21,8 +26,31 @@ namespace lean {
    metavariables or level metavariables.
 
    Each constraint is associated with a justification object.
+
+   \remark We also have choice constraints that are used by elaborator to specify
+   the possible solutions for a metavariable. The choice constraints are not used by
+   the kernel.
 */
-enum class constraint_kind { Eq, Level };
+enum class constraint_kind { Eq, Level, Choice };
+class constraint;
+typedef list<constraint> constraints;
+typedef std::tuple<expr, justification, constraints> choice_fn_result;
+/**
+   \brief A choice_fn is used to enumerate the possible solutions for a metavariable.
+   The input arguments are:
+        - an inferred type (if available)
+        - substitution map (metavar -> value)
+        - name generator
+
+   The result is a lazy_list of choices, i.e., tuples containing:
+        - an expression representing one of the possible solutions
+        - a justification for it (this is used to accumulate the justification for the substitutions used).
+        - a list of new constraints (that is, the solution is only valid if the additional constraints can be solved)
+
+   One application of choice constraints is overloaded notation.
+*/
+typedef std::function<lazy_list<choice_fn_result>(optional<expr> const &, substitution const &, name_generator const &)> choice_fn;
+
 struct constraint_cell;
 class constraint {
     constraint_cell * m_ptr;
@@ -33,7 +61,6 @@ public:
     ~constraint();
 
     constraint_kind kind() const;
-    unsigned hash() const;
     justification const & get_justification() const;
 
     constraint & operator=(constraint const & c);
@@ -44,18 +71,18 @@ public:
 
     friend constraint mk_eq_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 & m, choice_fn const & fn, 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); }
-
 constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
 constraint mk_level_cnstr(level const & lhs, level const & rhs, justification const & j);
+constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, justification const & j);
 
 inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
 inline bool is_level_cnstr(constraint const & c) { return c.kind() == constraint_kind::Level; }
+inline bool is_choice_cnstr(constraint const & c) { return c.kind() == constraint_kind::Choice; }
 
 /** \brief Return the lhs of an equality constraint. */
 expr const & cnstr_lhs_expr(constraint const & c);
@@ -65,19 +92,11 @@ expr const & cnstr_rhs_expr(constraint const & c);
 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 metavariable associated with a choice constraint */
-/** \brief Update equality constraint c with new_lhs, new_rhs and justification. */
+expr const & cnstr_mvar(constraint const & c);
-constraint updt_eq_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst);
+/** \brief Return the choice_fn associated with a choice constraint. */
-/** \brief Update equality constraint c with new_lhs and new_rhs, but keeping the same justification. */
+choice_fn const & cnstr_choice_fn(constraint const & c);
-constraint updt_eq_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;
-inline constraints add(constraints const & cs, constraint const & c) { return cons(c, cs); }
 }

src/library/kernel_bindings.cpp

@@ -1595,10 +1595,8 @@ DECL_UDATA(constraint)
 #define CNSTR_PRED(P) static int constraint_ ## P(lua_State * L) { check_num_args(L, 1); return push_boolean(L, P(to_constraint(L, 1))); }
 CNSTR_PRED(is_eq_cnstr)
 CNSTR_PRED(is_level_cnstr)
-static int constraint_eq(lua_State * L) { return push_boolean(L, to_constraint(L, 1) == to_constraint(L, 2)); }
 static int constraint_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_constraint(L, 1), to_constraint(L, 2))); }
 static int constraint_get_kind(lua_State * L) { return push_integer(L, static_cast<int>(to_constraint(L, 1).kind())); }
-static int constraint_hash(lua_State * L) { return push_integer(L, to_constraint(L, 1).hash()); }
 static int constraint_jst(lua_State * L) { return push_justification(L, to_constraint(L, 1).get_justification()); }
 static int constraint_lhs(lua_State * L) {
     constraint const & c = to_constraint(L, 1);
@@ -1629,12 +1627,10 @@ static int mk_level_cnstr(lua_State * L) { return push_constraint(L, mk_level_cn
 static const struct luaL_Reg constraint_m[] = {
     {"__gc",            constraint_gc}, // never throws
     {"__tostring",      safe_function<constraint_tostring>},
-    {"__eq",            safe_function<constraint_eq>},
     {"is_eq",           safe_function<constraint_is_eq_cnstr>},
     {"is_level",        safe_function<constraint_is_level_cnstr>},
     {"is_eqp",          safe_function<constraint_is_eqp>},
     {"kind",            safe_function<constraint_get_kind>},
-    {"hash",            safe_function<constraint_hash>},
     {"lhs",             safe_function<constraint_lhs>},
     {"rhs",             safe_function<constraint_rhs>},
     {"justification",   safe_function<constraint_jst>},

tests/lua/cnstr1.lua

@@ -12,8 +12,5 @@ print(c)
 local c3 = mk_level_cnstr(mk_level_zero(), mk_level_one(), j)
 assert(c3:is_level())
 print(c3)
-assert(c ~= c2)
-assert(c == mk_eq_cnstr(f(a), m, j))
 assert(c:is_eqp(c))
 assert(not c:is_eqp(mk_eq_cnstr(f(a), m, j)))
-assert(c:hash() == mk_eq_cnstr(f(a), m, j):hash())