refactor(kernel/constraint): rename choice constraint fields

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

src/kernel/constraint.cpp

@@ -29,12 +29,12 @@ struct level_constraint_cell : public constraint_cell {
         m_lhs(lhs), m_rhs(rhs) {}
 };
 struct choice_constraint_cell : public constraint_cell {
-    expr      m_mvar;
+    expr      m_expr;
     choice_fn m_fn;
     bool      m_delayed;
-    choice_constraint_cell(expr const & mvar, choice_fn const & fn, bool delayed, justification const & j):
+    choice_constraint_cell(expr const & e, choice_fn const & fn, bool delayed, justification const & j):
         constraint_cell(constraint_kind::Choice, j),
-        m_mvar(mvar), m_fn(fn), m_delayed(delayed) {}
+        m_expr(e), m_fn(fn), m_delayed(delayed) {}
 };
 
 void constraint_cell::dealloc() {
@@ -78,7 +78,7 @@ level const & cnstr_rhs_level(constraint const & c) {
     lean_assert(is_level_eq_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; }
+expr const & cnstr_expr(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_expr; }
 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;
 }
@@ -93,7 +93,7 @@ constraint update_justification(constraint const & c, justification const & j) {
     case constraint_kind::LevelEq:
         return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j);
     case constraint_kind::Choice:
-        return mk_choice_cnstr(cnstr_mvar(c), cnstr_choice_fn(c), cnstr_delayed(c), j);
+        return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delayed(c), j);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -109,7 +109,7 @@ std::ostream & operator<<(std::ostream & out, constraint const & c) {
     case constraint_kind::Choice:
         out << "choice ";
         if (cnstr_delayed(c)) out << "[delayed] ";
-        out << cnstr_mvar(c);
+        out << cnstr_expr(c);
         break;
     }
     return out;

src/kernel/constraint.h

@@ -34,7 +34,7 @@ namespace lean {
 enum class constraint_kind { Eq, LevelEq, Choice };
 class constraint;
 typedef list<constraint> constraints;
-typedef std::tuple<expr, justification, constraints> choice_fn_result;
+typedef std::tuple<expr, justification, constraints> a_choice; // a choice produced by the choice_fn
 /**
    \brief A choice_fn is used to enumerate the possible solutions for a metavariable.
    The input arguments are:
@@ -49,7 +49,7 @@ typedef std::tuple<expr, justification, constraints> choice_fn_result;
 
    One application of choice constraints is overloaded notation.
 */
-typedef std::function<lazy_list<choice_fn_result>(expr const &, substitution const &, name_generator const &)> choice_fn;
+typedef std::function<lazy_list<a_choice>(expr const &, substitution const &, name_generator const &)> choice_fn;
 
 struct constraint_cell;
 class constraint {
@@ -94,8 +94,8 @@ 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 Return the expression associated with a choice constraint */
-expr const & cnstr_mvar(constraint const & c);
+expr const & cnstr_expr(constraint const & c);
 /** \brief Return the choice_fn associated with a choice constraint. */
 choice_fn const & cnstr_choice_fn(constraint const & c);
 /** \brief Return true iff choice constraint must be delayed. */

src/library/kernel_bindings.cpp

@@ -1643,7 +1643,7 @@ static choice_fn to_choice_fn(lua_State * L, int idx) {
             push_substitution(L, s);
             push_name_generator(L, ngen);
             pcall(L, 3, 1, 0);
-            buffer<choice_fn_result> r;
+            buffer<a_choice> r;
             if (lua_isnil(L, -1)) {
                 // do nothing
             } else if (lua_istable(L, -1)) {
@@ -1652,7 +1652,7 @@ static choice_fn to_choice_fn(lua_State * L, int idx) {
                 for (int i = 1; i <= num; i++) {
                     lua_rawgeti(L, -1, i);
                     if (is_expr(L, -1)) {
-                        r.push_back(choice_fn_result(to_expr(L, -1), justification(), constraints()));
+                        r.push_back(a_choice(to_expr(L, -1), justification(), constraints()));
                     } else if (lua_istable(L, -1) && objlen(L, -1) == 3) {
                         lua_rawgeti(L, -1, 1);
                         expr c = to_expr(L, -1);
@@ -1676,7 +1676,7 @@ static choice_fn to_choice_fn(lua_State * L, int idx) {
                                             "where the third element of each triple is an array of constraints");
                         }
                         lua_pop(L, 1);
-                        r.push_back(choice_fn_result(c, j, to_list(cs.begin(), cs.end())));
+                        r.push_back(a_choice(c, j, to_list(cs.begin(), cs.end())));
                     } else {
                         throw exception("invalid choice function, result must be an array of triples");
                     }
@@ -1704,6 +1704,22 @@ static int mk_choice_cnstr(lua_State * L) {
         return push_constraint(L, mk_choice_cnstr(m, fn, lua_toboolean(L, 3), to_justification(L, 4)));
 }
 
+static int constraint_expr(lua_State * L) {
+    constraint const & c = to_constraint(L, 1);
+    if (is_choice_cnstr(c))
+        return push_expr(L, cnstr_expr(c));
+    else
+        throw exception("arg #1 must be a choice constraint");
+}
+
+static int constraint_delayed(lua_State * L) {
+    constraint const & c = to_constraint(L, 1);
+    if (is_choice_cnstr(c))
+        return push_boolean(L, cnstr_delayed(c));
+    else
+        throw exception("arg #1 must be a choice constraint");
+}
+
 static const struct luaL_Reg constraint_m[] = {
     {"__gc",            constraint_gc}, // never throws
     {"__tostring",      safe_function<constraint_tostring>},
@@ -1715,6 +1731,8 @@ static const struct luaL_Reg constraint_m[] = {
     {"lhs",             safe_function<constraint_lhs>},
     {"rhs",             safe_function<constraint_rhs>},
     {"justification",   safe_function<constraint_jst>},
+    {"expr",            safe_function<constraint_expr>},
+    {"delayed",         safe_function<constraint_delayed>},
     {0, 0}
 };
 

src/library/unifier.cpp

@@ -262,11 +262,11 @@ struct unifier_fn {
     };
 
     struct choice_case_split : public case_split {
-        expr                        m_mvar;
+        expr                 m_expr;
-        justification               m_jst;
+        justification        m_jst;
-        lazy_list<choice_fn_result> m_tail;
+        lazy_list<a_choice>  m_tail;
-        choice_case_split(unifier_fn & u, expr const & mvar, justification const & j, lazy_list<choice_fn_result> const & tail):
+        choice_case_split(unifier_fn & u, expr const & expr, justification const & j, lazy_list<a_choice> const & tail):
-            case_split(u), m_mvar(mvar), m_jst(j), m_tail(tail) {}
+            case_split(u), m_expr(expr), m_jst(j), m_tail(tail) {}
         virtual bool next(unifier_fn & u) { return u.next_choice_case_split(*this); }
     };
 
@@ -716,7 +716,7 @@ struct unifier_fn {
         return !in_conflict();
     }
 
-    bool process_choice_result(expr const & m, choice_fn_result const & r, justification j) {
+    bool process_choice_result(expr const & m, a_choice const & r, justification j) {
         j = mk_composite1(j, std::get<1>(r));
         return
             process_constraint(mk_eq_cnstr(m, std::get<0>(r), j)) &&
@@ -730,7 +730,7 @@ struct unifier_fn {
             lean_assert(!in_conflict());
             cs.m_tail = r->second;
             justification a = mk_assumption_justification(cs.m_assumption_idx);
-            return process_choice_result(cs.m_mvar, r->first, mk_composite1(cs.m_jst, a));
+            return process_choice_result(cs.m_expr, r->first, mk_composite1(cs.m_jst, a));
         } else {
             // update conflict
             update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications));
@@ -740,9 +740,8 @@ struct unifier_fn {
 
     bool process_choice_constraint(constraint const & c) {
         lean_assert(is_choice_cnstr(c));
-        expr const &   m     = cnstr_mvar(c);
+        expr const &   m     = cnstr_expr(c);
         choice_fn const & fn = cnstr_choice_fn(c);
-        lean_assert(is_meta(m));
         auto m_type_jst      = m_subst.instantiate_metavars(m_tc.infer(m), nullptr, nullptr);
         auto rlist           = fn(m_type_jst.first, m_subst, m_ngen.mk_child());
         auto r               = rlist.pull();