michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/constraint): remove choice constraints from the kernel, the kernel does not use them, we will implement them in elaborator

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-03 00:46:28 -07:00
parent 931ebf9637
commit ab5f570924
4 changed files with 1 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/kernel/constraint.cpp
View file

@ -29,16 +29,6 @@ struct level_constraint_cell : public constraint_cell {
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) {}
};
void constraint_cell::dealloc() {
switch (m_kind) {
@ -46,8 +36,6 @@ 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;
}
}
@ -67,9 +55,6 @@ 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 & 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())
@ -79,10 +64,6 @@ bool operator==(constraint const & c1, constraint const & c2) {
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; });
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -91,12 +72,6 @@ expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c));
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_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_eq_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst) {
lean_assert(is_eq_cnstr(c));
@ -127,15 +102,6 @@ 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 << cnstr_choice_expr(c) << " ∊ {";
bool first = true;
for (expr const & e : cnstr_choice_set(c)) {
if (first) first = false; else out << ", ";
out << e;
}
out << "}";
break;
}
return out;
}

17
src/kernel/constraint.h
View file

@ -21,16 +21,8 @@ namespace lean {
metavariables or level 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 class constraint_kind { Eq, Level, Choice };
enum class constraint_kind { Eq, Level };
struct constraint_cell;
class constraint {
constraint_cell * m_ptr;
@ -52,7 +44,6 @@ 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 & t, list<expr> const & s, justification const & j);
constraint_cell * raw() const { return m_ptr; }
};
@ -62,11 +53,9 @@ inline bool operator!=(constraint const & c1, constraint const & c2) { return !(
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 & t, list<expr> const & s, 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);
@ -76,10 +65,6 @@ 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 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 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);

10
src/library/kernel_bindings.cpp
View file

@ -1558,7 +1558,6 @@ DECL_UDATA(constraint)
#define CNSTR_PRED(P) static int constraint_ ## P(lua_State * L) { return push_boolean(L, P(to_constraint(L, 1))); }
CNSTR_PRED(is_eq_cnstr)
CNSTR_PRED(is_level_cnstr)
CNSTR_PRED(is_choice_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())); }
@ -1582,8 +1581,6 @@ static int constraint_rhs(lua_State * L) {
else
throw exception("arg #1 must be an equality/level constraint");
}
static int constraint_choice_expr(lua_State * L) { return push_expr(L, cnstr_choice_expr(to_constraint(L, 1))); }
static int constraint_choice_set(lua_State * L) { return push_list_expr(L, cnstr_choice_set(to_constraint(L, 1))); }
static int constraint_tostring(lua_State * L) {
std::ostringstream out;
out << to_constraint(L, 1);
@ -1592,23 +1589,18 @@ static int constraint_tostring(lua_State * L) {
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_choice_cnstr(lua_State * L) { return push_constraint(L, mk_choice_cnstr(to_expr(L, 1), to_list_expr_ext(L, 2), to_justification(L, 3))); }
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_choice", safe_function<constraint_is_choice_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>},
{"choice_expr", safe_function<constraint_choice_expr>},
{"choice_set", safe_function<constraint_choice_set>},
{0, 0}
};
@ -1621,12 +1613,10 @@ static void open_constraint(lua_State * L) {
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(mk_choice_cnstr, "mk_choice_cnstr");
lua_newtable(L);
SET_ENUM("Eq", constraint_kind::Eq);
SET_ENUM("Level", constraint_kind::Level);
SET_ENUM("Choice", constraint_kind::Choice);
lua_setglobal(L, "constraint_kind");
}

9
tests/lua/cnstr1.lua
View file

@ -4,7 +4,6 @@ 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_choice())
assert(not c:is_level())
assert(c:lhs() == f(a))
assert(c:rhs() == m)
@ -18,11 +17,3 @@ 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())
local c4 = mk_choice_cnstr(m, {a, f(a), f(f(a))}, j)
print(c4)
assert(c4:is_choice())
assert(c4:choice_expr() == m)
print(c4:choice_set():head())
assert(c4:choice_set():head() == a)
assert(c4:choice_set():tail():head() == f(a))
assert(#(c4:choice_set()) == 3)