diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp index 7f7683141..325db3e88 100644 --- a/src/kernel/constraint.cpp +++ b/src/kernel/constraint.cpp @@ -25,7 +25,7 @@ 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, j), + constraint_cell(constraint_kind::LevelEq, j), m_lhs(lhs), m_rhs(rhs) {} }; struct choice_constraint_cell : public constraint_cell { @@ -40,7 +40,7 @@ void constraint_cell::dealloc() { switch (m_kind) { case constraint_kind::Eq: delete static_cast(this); break; - case constraint_kind::Level: + case constraint_kind::LevelEq: delete static_cast(this); break; case constraint_kind::Choice: delete static_cast(this); break; @@ -59,7 +59,7 @@ justification const & constraint::get_justification() const { lean_assert(m_ptr) constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) { return constraint(new eq_constraint_cell(lhs, rhs, j)); } -constraint mk_level_cnstr(level const & lhs, level const & rhs, justification const & j) { +constraint mk_level_eq_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) { @@ -69,40 +69,25 @@ constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, justification c 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; } +level const & cnstr_lhs_level(constraint const & c) { + lean_assert(is_level_eq_cnstr(c)); + return static_cast(c.raw())->m_lhs; +} +level const & cnstr_rhs_level(constraint const & c) { + lean_assert(is_level_eq_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)); - if (!is_eqp(cnstr_lhs_expr(c), new_lhs) || !is_eqp(cnstr_rhs_expr(c), new_rhs)) - return mk_eq_cnstr(new_lhs, new_rhs, new_jst); - else - return c; -} -constraint updt_eq_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs) { - return updt_eq_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); break; - case constraint_kind::Level: + case constraint_kind::LevelEq: out << cnstr_lhs_level(c) << " = " << cnstr_rhs_level(c); break; case constraint_kind::Choice: diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index 70d8c5359..b00df593b 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -31,7 +31,7 @@ namespace lean { the possible solutions for a metavariable. The choice constraints are not used by the kernel. */ -enum class constraint_kind { Eq, Level, Choice }; +enum class constraint_kind { Eq, LevelEq, Choice }; class constraint; typedef list constraints; typedef std::tuple choice_fn_result; @@ -70,18 +70,18 @@ public: 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_level_cnstr(level const & lhs, level const & rhs, justification const & j); + friend constraint mk_level_eq_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; } }; 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_level_eq_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_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; } inline bool is_choice_cnstr(constraint const & c) { return c.kind() == constraint_kind::Choice; } /** \brief Return the lhs of an equality constraint. */ diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index fa6304a0b..93a7ee5a8 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -309,7 +309,7 @@ struct default_converter : public converter { if (is_equivalent(sort_level(t), sort_level(s))) { return l_true; } else if (has_meta(sort_level(t)) || has_meta(sort_level(s))) { - c.add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), jst.get())); + c.add_cnstr(mk_level_eq_cnstr(sort_level(t), sort_level(s), jst.get())); return l_true; } else { return l_false; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index fb73e691c..6be2f2d82 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1594,7 +1594,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) +CNSTR_PRED(is_level_eq_cnstr) +CNSTR_PRED(is_choice_cnstr) 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_jst(lua_State * L) { return push_justification(L, to_constraint(L, 1).get_justification()); } @@ -1602,7 +1603,7 @@ static int constraint_lhs(lua_State * L) { constraint const & c = to_constraint(L, 1); if (is_eq_cnstr(c)) return push_expr(L, cnstr_lhs_expr(c)); - else if (is_level_cnstr(c)) + else if (is_level_eq_cnstr(c)) return push_level(L, cnstr_lhs_level(c)); else throw exception("arg #1 must be an equality/level constraint"); @@ -1611,7 +1612,7 @@ static int constraint_rhs(lua_State * L) { constraint const & c = to_constraint(L, 1); if (is_eq_cnstr(c)) return push_expr(L, cnstr_rhs_expr(c)); - else if (is_level_cnstr(c)) + else if (is_level_eq_cnstr(c)) return push_level(L, cnstr_rhs_level(c)); else throw exception("arg #1 must be an equality/level constraint"); @@ -1622,13 +1623,14 @@ static int constraint_tostring(lua_State * L) { return push_string(L, out.str().c_str()); } static int mk_eq_cnstr(lua_State * L) { return push_constraint(L, mk_eq_cnstr(to_expr(L, 1), to_expr(L, 2), to_justification(L, 3))); } -static int mk_level_cnstr(lua_State * L) { return push_constraint(L, mk_level_cnstr(to_level_ext(L, 1), to_level_ext(L, 2), - to_justification(L, 3))); } +static int mk_level_eq_cnstr(lua_State * L) { return push_constraint(L, mk_level_eq_cnstr(to_level_ext(L, 1), to_level_ext(L, 2), + to_justification(L, 3))); } static const struct luaL_Reg constraint_m[] = { {"__gc", constraint_gc}, // never throws {"__tostring", safe_function}, {"is_eq", safe_function}, - {"is_level", safe_function}, + {"is_level_eq", safe_function}, + {"is_choice", safe_function}, {"is_eqp", safe_function}, {"kind", safe_function}, {"lhs", safe_function}, @@ -1643,13 +1645,14 @@ static void open_constraint(lua_State * L) { lua_setfield(L, -2, "__index"); setfuncs(L, constraint_m, 0); - SET_GLOBAL_FUN(constraint_pred, "is_constraint"); - SET_GLOBAL_FUN(mk_eq_cnstr, "mk_eq_cnstr"); - SET_GLOBAL_FUN(mk_level_cnstr, "mk_level_cnstr"); + SET_GLOBAL_FUN(constraint_pred, "is_constraint"); + SET_GLOBAL_FUN(mk_eq_cnstr, "mk_eq_cnstr"); + SET_GLOBAL_FUN(mk_level_eq_cnstr, "mk_level_eq_cnstr"); lua_newtable(L); SET_ENUM("Eq", constraint_kind::Eq); - SET_ENUM("Level", constraint_kind::Level); + SET_ENUM("LevelEq", constraint_kind::LevelEq); + SET_ENUM("Choice", constraint_kind::Choice); lua_setglobal(L, "constraint_kind"); } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index fa4194096..d098d0c23 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -140,7 +140,7 @@ std::pair unify_simple(substitution const & s, level std::pair unify_simple(substitution const & s, constraint const & c) { if (is_eq_cnstr(c)) return unify_simple(s, cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification()); - else if (is_level_cnstr(c)) + else if (is_level_eq_cnstr(c)) return unify_simple(s, cnstr_lhs_level(c), cnstr_rhs_level(c), c.get_justification()); else return mk_pair(unify_status::Unsupported, s); @@ -393,7 +393,7 @@ struct unifier_fn { return true; case constraint_kind::Eq: return process_eq_constraint(c); - case constraint_kind::Level: + case constraint_kind::LevelEq: return process_lvl_constraint(c); } lean_unreachable(); // LCOV_EXCL_LINE diff --git a/tests/lua/cnstr1.lua b/tests/lua/cnstr1.lua index 7ba29111a..e84d34699 100644 --- a/tests/lua/cnstr1.lua +++ b/tests/lua/cnstr1.lua @@ -4,13 +4,13 @@ local m = mk_metavar("m", Bool) local j = justification("type match") local c = mk_eq_cnstr(f(a), m, j) assert(c:is_eq()) -assert(not c:is_level()) +assert(not c:is_level_eq()) assert(c:lhs() == f(a)) assert(c:rhs() == m) assert(c:justification():is_eqp(j)) print(c) -local c3 = mk_level_cnstr(mk_level_zero(), mk_level_one(), j) -assert(c3:is_level()) +local c3 = mk_level_eq_cnstr(mk_level_zero(), mk_level_one(), j) +assert(c3:is_level_eq()) print(c3) assert(c:is_eqp(c)) assert(not c:is_eqp(mk_eq_cnstr(f(a), m, j)))