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

refactor(kernel): remove convertability constraints

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-09 20:25:27 -07:00
parent d4400d6135
commit 9d96f24766
5 changed files with 35 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/kernel/constraint.cpp
View file

@ -15,11 +15,11 @@ struct constraint_cell {
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) {}
};
struct eqc_constraint_cell : public constraint_cell {
struct eq_constraint_cell : public constraint_cell {
expr m_lhs;
expr m_rhs;
eqc_constraint_cell(constraint_kind k, expr const & lhs, expr const & rhs, justification const & j):
constraint_cell(k, hash(hash(lhs.hash(), rhs.hash()), static_cast<unsigned>(k)), j),
eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j):
constraint_cell(constraint_kind::Eq, hash(lhs.hash(), rhs.hash()), j),
m_lhs(lhs), m_rhs(rhs) {}
};
struct level_constraint_cell : public constraint_cell {
@ -42,8 +42,8 @@ struct choice_constraint_cell : public constraint_cell {
void constraint_cell::dealloc() {
switch (m_kind) {
case constraint_kind::Eq: case constraint_kind::Convertible:
delete static_cast<eqc_constraint_cell*>(this); break;
case constraint_kind::Eq:
delete static_cast<eq_constraint_cell*>(this); break;
case constraint_kind::Level:
delete static_cast<level_constraint_cell*>(this); break;
case constraint_kind::Choice:
@ -62,10 +62,7 @@ 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) {
return constraint(new eqc_constraint_cell(constraint_kind::Eq, lhs, rhs, j));
}
constraint mk_conv_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
return constraint(new eqc_constraint_cell(constraint_kind::Convertible, lhs, rhs, j));
return constraint(new eq_constraint_cell(lhs, rhs, j));
}
constraint mk_level_cnstr(level const & lhs, level const & rhs, justification const & j) {
return constraint(new level_constraint_cell(lhs, rhs, j));
@ -78,7 +75,7 @@ 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: case constraint_kind::Convertible:
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);
@ -90,14 +87,10 @@ bool operator==(constraint const & c1, constraint const & c2) {
lean_unreachable(); // LCOV_EXCL_LINE
}
expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eqc_cnstr(c)); return static_cast<eqc_constraint_cell*>(c.raw())->m_lhs; }
expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eqc_cnstr(c)); return static_cast<eqc_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_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_choice_expr(constraint const & c) {
lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_expr;
}
@ -105,19 +98,15 @@ 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_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst) {
lean_assert(is_eqc_cnstr(c));
if (!is_eqp(cnstr_lhs_expr(c), new_lhs) || !is_eqp(cnstr_rhs_expr(c), new_rhs)) {
if (is_eq_cnstr(c))
return mk_eq_cnstr(new_lhs, new_rhs, new_jst);
else
return mk_conv_cnstr(new_lhs, new_rhs, new_jst);
} else {
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_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs) {
return updt_eqc_cnstr(c, new_lhs, new_rhs, c.get_justification());
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));
@ -135,11 +124,8 @@ std::ostream & operator<<(std::ostream & out, constraint const & c) {
case constraint_kind::Eq:
out << cnstr_lhs_expr(c) << " ≈ " << cnstr_rhs_expr(c);
break;
case constraint_kind::Convertible:
out << cnstr_lhs_expr(c) << " ↠ " << cnstr_rhs_expr(c);
break;
case constraint_kind::Level:
out << cnstr_lhs_level(c) << " ≤ " << cnstr_rhs_level(c);
out << cnstr_lhs_level(c) << " = " << cnstr_rhs_level(c);
break;
case constraint_kind::Choice:
out << cnstr_choice_expr(c) << " ∊ {";

28
src/kernel/constraint.h
View file

@ -10,17 +10,15 @@ Author: Leonardo de Moura
#include "kernel/justification.h"
namespace lean {
/**
\brief The lean kernel type checker produces three kinds of constraints:
\brief The lean kernel type checker produces two kinds of constraints:
- Equality constraint: t ≈ s
The terms t and s must be definitionally equal.
- Convertability constraint: t ↠ s
The term t must be convertible to s
- Universe level constaint: l ≤ m
- Universe level constaint: l = m
The universe level l must be less than or equal to m.
\remark The first two kinds are only generated if the input term
contains metavariables.
\remark The constraints are only generated if the input term contains
metavariables or level metavariables.
Each constraint is associated with a justification object.
@ -32,7 +30,7 @@ namespace lean {
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, Convertible, Level, Choice };
enum class constraint_kind { Eq, Level, Choice };
struct constraint_cell;
class constraint {
constraint_cell * m_ptr;
@ -53,7 +51,6 @@ 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_conv_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);
@ -64,19 +61,16 @@ 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_conv_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_conv_cnstr(constraint const & c) { return c.kind() == constraint_kind::Convertible; }
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; }
inline bool is_eqc_cnstr(constraint const & c) { return is_eq_cnstr(c) || is_conv_cnstr(c); }
/** \brief Return the lhs of an equality/convertability constraint. */
/** \brief Return the lhs of an equality constraint. */
expr const & cnstr_lhs_expr(constraint const & c);
/** \brief Return the rhs of an equality/convertability constraint. */
/** \brief Return the rhs of an equality constraint. */
expr const & cnstr_rhs_expr(constraint const & c);
/** \brief Return the lhs of an level constraint. */
level const & cnstr_lhs_level(constraint const & c);
@ -87,10 +81,10 @@ 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/convertability constraint c with new_lhs, new_rhs and justification. */
constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst);
/** \brief Update equality/convertability constraint c with new_lhs and new_rhs, but keeping the same justification. */
constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs);
/** \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. */

5
src/kernel/converter.cpp
View file

@ -327,10 +327,7 @@ struct default_converter : public converter {
return l_true; // t and s are structurally equal
if (is_meta(t) || is_meta(s)) {
// if t or s is a metavariable (or the application of a metavariable), then add constraint
if (def_eq)
c.add_cnstr(mk_eq_cnstr(t, s, jst.get()));
else
c.add_cnstr(mk_conv_cnstr(t, s, jst.get()));
c.add_cnstr(mk_eq_cnstr(t, s, jst.get()));
return l_true;
}
if (t.kind() == s.kind()) {

15
src/library/kernel_bindings.cpp
View file

@ -1180,8 +1180,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_conv_cnstr)
CNSTR_PRED(is_eqc_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)); }
@ -1191,21 +1189,21 @@ static int constraint_hash(lua_State * L) { return push_integer(L, to_constraint
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);
if (is_eqc_cnstr(c))
if (is_eq_cnstr(c))
return push_expr(L, cnstr_lhs_expr(c));
else if (is_level_cnstr(c))
return push_level(L, cnstr_lhs_level(c));
else
throw exception("arg #1 must be an equality/convertability/level constraint");
throw exception("arg #1 must be an equality/level constraint");
}
static int constraint_rhs(lua_State * L) {
constraint const & c = to_constraint(L, 1);
if (is_eqc_cnstr(c))
if (is_eq_cnstr(c))
return push_expr(L, cnstr_rhs_expr(c));
else if (is_level_cnstr(c))
return push_level(L, cnstr_rhs_level(c));
else
throw exception("arg #1 must be an equality/convertability/level constraint");
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))); }
@ -1215,7 +1213,6 @@ 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_conv_cnstr(lua_State * L) { return push_constraint(L, mk_conv_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(L, 1), to_level(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))); }
@ -1224,8 +1221,6 @@ static const struct luaL_Reg constraint_m[] = {
{"__tostring", safe_function<constraint_tostring>},
{"__eq", safe_function<constraint_eq>},
{"is_eq", safe_function<constraint_is_eq_cnstr>},
{"is_conv", safe_function<constraint_is_conv_cnstr>},
{"is_eqc", safe_function<constraint_is_eqc_cnstr>},
{"is_level", safe_function<constraint_is_level_cnstr>},
{"is_choice", safe_function<constraint_is_choice_cnstr>},
{"is_eqp", safe_function<constraint_is_eqp>},
@ -1247,13 +1242,11 @@ 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_conv_cnstr, "mk_conv_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("Convertible", constraint_kind::Convertible);
SET_ENUM("Level", constraint_kind::Level);
SET_ENUM("Choice", constraint_kind::Choice);
lua_setglobal(L, "constraint_kind");

7
tests/lua/cnstr1.lua
View file

@ -4,19 +4,12 @@ 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(c:is_eqc())
assert(not c:is_choice())
assert(not c:is_level())
assert(c:lhs() == f(a))
assert(c:rhs() == m)
assert(c:justification():is_eqp(j))
print(c)
local c2 = mk_conv_cnstr(f(m), f(a), j)
print(c2)
assert(not c2:is_eq())
assert(c2:is_conv())
assert(c2:is_eqc())
assert(c2:lhs() == f(m))
local c3 = mk_level_cnstr(mk_level_zero(), mk_level_one(), j)
assert(c3:is_level())
print(c3)