From 67088b130ee47177c4987b26a0b5e6bced95b881 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 21 Jun 2014 08:15:47 -0700 Subject: [PATCH] refactor(kernel/constraint): simplify constraint interface, and add choice constraint Signed-off-by: Leonardo de Moura --- src/kernel/constraint.cpp | 38 +++++++++++++---------- src/kernel/constraint.h | 53 ++++++++++++++++++++++----------- src/library/kernel_bindings.cpp | 4 --- tests/lua/cnstr1.lua | 3 -- 4 files changed, 58 insertions(+), 40 deletions(-) diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp index 53350875b..7f7683141 100644 --- a/src/kernel/constraint.cpp +++ b/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(this); break; case constraint_kind::Level: delete static_cast(this); break; + case constraint_kind::Choice: + delete static_cast(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)); } - -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: - 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 +constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, justification const & j) { + lean_assert(is_meta(m)); + return constraint(new choice_constraint_cell(m, fn, j)); } expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast(c.raw())->m_lhs; } expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast(c.raw())->m_rhs; } level const & cnstr_lhs_level(constraint const & c) { lean_assert(is_level_cnstr(c)); return static_cast(c.raw())->m_lhs; } level const & cnstr_rhs_level(constraint const & c) { lean_assert(is_level_cnstr(c)); return static_cast(c.raw())->m_rhs; } +expr const & cnstr_mvar(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_mvar; } +choice_fn const & cnstr_choice_fn(constraint const & c) { + lean_assert(is_choice_cnstr(c)); return static_cast(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; } diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index 54dd158d2..70d8c5359 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -6,8 +6,13 @@ Author: Leonardo de Moura */ #pragma once #include +#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 constraints; +typedef std::tuple 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(optional 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 Update equality constraint c with new_lhs, new_rhs and justification. */ -constraint updt_eq_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst); -/** \brief Update equality constraint c with new_lhs and new_rhs, but keeping the same justification. */ -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 Return the metavariable associated with a choice constraint */ +expr const & cnstr_mvar(constraint const & c); +/** \brief Return the choice_fn associated with a choice constraint. */ +choice_fn const & cnstr_choice_fn(constraint const & c); /** \brief Printer for debugging purposes */ std::ostream & operator<<(std::ostream & out, constraint const & c); - -typedef list constraints; -inline constraints add(constraints const & cs, constraint const & c) { return cons(c, cs); } } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 195236291..f915b64eb 100644 --- a/src/library/kernel_bindings.cpp +++ b/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(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}, - {"__eq", safe_function}, {"is_eq", safe_function}, {"is_level", safe_function}, {"is_eqp", safe_function}, {"kind", safe_function}, - {"hash", safe_function}, {"lhs", safe_function}, {"rhs", safe_function}, {"justification", safe_function}, diff --git a/tests/lua/cnstr1.lua b/tests/lua/cnstr1.lua index 2e5550033..7ba29111a 100644 --- a/tests/lua/cnstr1.lua +++ b/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())