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

refactor(kernel): remove level constraints from definitions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-09 20:11:50 -07:00
parent 23ed003389
commit 7b6d555433
6 changed files with 63 additions and 91 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
src/kernel/definition.cpp
View file

@ -16,7 +16,6 @@ struct definition::cell {
MK_LEAN_RC();
name m_name;
param_names m_params;
level_cnstrs m_cnstrs;
expr m_type;
bool m_theorem;
optional<expr> m_value; // if none, then definition is actually a postulate
@ -33,12 +32,12 @@ struct definition::cell {
bool m_use_conv_opt;
void dealloc() { delete this; }
cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, bool is_axiom):
m_rc(1), m_name(n), m_params(params), m_cnstrs(cs), m_type(t), m_theorem(is_axiom),
cell(name const & n, param_names const & params, expr const & t, bool is_axiom):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
m_weight(0), m_module_idx(0), m_opaque(true), m_use_conv_opt(false) {}
cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, bool is_thm, expr const & v,
cell(name const & n, param_names const & params, expr const & t, bool is_thm, expr const & v,
bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
m_rc(1), m_name(n), m_params(params), m_cnstrs(cs), m_type(t), m_theorem(is_thm),
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
void write(serializer & s) const {
@ -52,7 +51,7 @@ struct definition::cell {
}
if (m_theorem)
k |= 8;
s << k << m_name << m_params << m_cnstrs << m_type;
s << k << m_name << m_params << m_type;
if (m_value) {
s << *m_value;
if (!m_theorem)
@ -61,7 +60,7 @@ struct definition::cell {
}
};
definition g_dummy = mk_axiom(name(), param_names(), level_cnstrs(), expr());
definition g_dummy = mk_axiom(name(), param_names(), expr());
definition::definition():definition(g_dummy) {}
definition::definition(cell * ptr):m_ptr(ptr) {}
@ -79,7 +78,6 @@ bool definition::is_theorem() const { return is_definition() && m_ptr->m_theo
name definition::get_name() const { return m_ptr->m_name; }
param_names const & definition::get_params() const { return m_ptr->m_params; }
level_cnstrs const & definition::get_level_cnstrs() const { return m_ptr->m_cnstrs; }
expr definition::get_type() const { return m_ptr->m_type; }
bool definition::is_opaque() const { return m_ptr->m_opaque; }
@ -90,10 +88,12 @@ bool definition::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
void definition::write(serializer & s) const { m_ptr->write(s); }
definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
return definition(new definition::cell(n, params, cs, t, false, v, opaque, weight, mod_idx, use_conv_opt));
definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v,
bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
return definition(new definition::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
}
definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt) {
definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t, expr const & v,
bool opaque, module_idx mod_idx, bool use_conv_opt) {
unsigned w = 0;
for_each(v, [&](expr const & e, unsigned) {
if (is_constant(e)) {
@ -103,16 +103,16 @@ definition mk_definition(environment const & env, name const & n, param_names co
}
return true;
});
return mk_definition(n, params, cs, t, v, opaque, w+1, mod_idx, use_conv_opt);
return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
}
definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v) {
return definition(new definition::cell(n, params, cs, t, true, v, true, 0, 0, false));
definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v) {
return definition(new definition::cell(n, params, t, true, v, true, 0, 0, false));
}
definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t) {
return definition(new definition::cell(n, params, cs, t, true));
definition mk_axiom(name const & n, param_names const & params, expr const & t) {
return definition(new definition::cell(n, params, t, true));
}
definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t) {
return definition(new definition::cell(n, params, cs, t, false));
definition mk_var_decl(name const & n, param_names const & params, expr const & t) {
return definition(new definition::cell(n, params, t, false));
}
definition read_definition(deserializer & d, unsigned module_idx) {
@ -121,23 +121,22 @@ definition read_definition(deserializer & d, unsigned module_idx) {
bool is_theorem = (k & 8) != 0;
name n = read_name(d);
param_names ps = read_params(d);
level_cnstrs cs = read_level_cnstrs(d);
expr t = read_expr(d);
if (has_value) {
expr v = read_expr(d);
if (is_theorem) {
return mk_theorem(n, ps, cs, t, v);
return mk_theorem(n, ps, t, v);
} else {
unsigned w = d.read_unsigned();
bool is_opaque = (k & 2) != 0;
bool use_conv_opt = (k & 4) != 0;
return mk_definition(n, ps, cs, t, v, is_opaque, w, module_idx, use_conv_opt);
return mk_definition(n, ps, t, v, is_opaque, w, module_idx, use_conv_opt);
}
} else {
if (is_theorem)
return mk_axiom(n, ps, cs, t);
return mk_axiom(n, ps, t);
else
return mk_var_decl(n, ps, cs, t);
return mk_var_decl(n, ps, t);
}
}
}

23
src/kernel/definition.h
View file

@ -59,7 +59,6 @@ public:
name get_name() const;
param_names const & get_params() const;
level_cnstrs const & get_level_cnstrs() const;
expr get_type() const;
expr get_value() const;
@ -68,13 +67,13 @@ public:
module_idx get_module_idx() const;
bool use_conv_opt() const;
friend definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t,
friend definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t,
expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
friend definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque,
friend definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v, bool opaque,
unsigned weight, module_idx mod_idx, bool use_conv_opt);
friend definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v);
friend definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
friend definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
friend definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v);
friend definition mk_axiom(name const & n, param_names const & params, expr const & t);
friend definition mk_var_decl(name const & n, param_names const & params, expr const & t);
void write(serializer & s) const;
};
@ -83,9 +82,11 @@ inline optional<definition> none_definition() { return optional<definition>(); }
inline optional<definition> some_definition(definition const & o) { return optional<definition>(o); }
inline optional<definition> some_definition(definition && o) { return optional<definition>(std::forward<definition>(o)); }
definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v);
definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v,
bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t, expr const & v,
bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v);
definition mk_axiom(name const & n, param_names const & params, expr const & t);
definition mk_var_decl(name const & n, param_names const & params, expr const & t);
}

10
src/kernel/type_checker.cpp
View file

@ -341,16 +341,6 @@ struct type_checker::imp {
definition d = m_env.get(const_name(e));
auto const & ps = d.get_params();
auto const & ls = const_level_params(e);
auto const & cs = d.get_level_cnstrs();
if (!infer_only && !is_nil(cs)) {
// add level constraints associated with the definition
for (auto const & c : cs) {
level lhs = lean::instantiate(c.first, ps, ls);
level rhs = lean::instantiate(c.second, ps, ls);
if (!is_trivial(lhs, rhs))
add_cnstr(mk_level_cnstr(lhs, rhs, mk_lvl_cnstr_jst(e, lhs, rhs)));
}
}
r = instantiate_params(d.get_type(), ps, ls);
break;
}

29
src/library/kernel_bindings.cpp
View file

@ -621,7 +621,6 @@ DEFINITION_PRED(is_opaque)
DEFINITION_PRED(use_conv_opt)
static int definition_get_name(lua_State * L) { return push_name(L, to_definition(L, 1).get_name()); }
static int definition_get_params(lua_State * L) { return push_list_name(L, to_definition(L, 1).get_params()); }
static int definition_get_level_cnstrs(lua_State * L) { return push_list_pair_level(L, to_definition(L, 1).get_level_cnstrs()); }
static int definition_get_type(lua_State * L) { return push_expr(L, to_definition(L, 1).get_type()); }
static int definition_get_value(lua_State * L) {
if (to_definition(L, 1).is_definition())
@ -633,23 +632,23 @@ static int definition_get_module_idx(lua_State * L) { return push_integer(L, to_
static int mk_var_decl(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_definition(L, mk_var_decl(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2)));
return push_definition(L, mk_var_decl(to_name_ext(L, 1), param_names(), to_expr(L, 2)));
else
return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4)));
return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_list_name_ext(L, 2), to_expr(L, 3)));
}
static int mk_axiom(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_definition(L, mk_axiom(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2)));
return push_definition(L, mk_axiom(to_name_ext(L, 1), param_names(), to_expr(L, 2)));
else
return push_definition(L, mk_axiom(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4)));
return push_definition(L, mk_axiom(to_name_ext(L, 1), to_list_name_ext(L, 2), to_expr(L, 3)));
}
static int mk_theorem(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 3)
return push_definition(L, mk_theorem(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2), to_expr(L, 3)));
return push_definition(L, mk_theorem(to_name_ext(L, 1), param_names(), to_expr(L, 2), to_expr(L, 3)));
else
return push_definition(L, mk_theorem(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4), to_expr(L, 5)));
return push_definition(L, mk_theorem(to_name_ext(L, 1), to_list_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4)));
}
static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, module_idx & mod_idx, bool & use_conv_opt) {
opaque = get_bool_named_param(L, idx, "opaque", opaque);
@ -663,23 +662,22 @@ static int mk_definition(lua_State * L) {
if (is_environment(L, 1)) {
if (nargs <= 5) {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), param_names(), level_cnstrs(),
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), param_names(),
to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt));
} else {
get_definition_args(L, 7, opaque, weight, mod_idx, use_conv_opt);
get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_list_name_ext(L, 3),
to_list_pair_level_ext(L, 4), to_expr(L, 5), to_expr(L, 6),
opaque, mod_idx, use_conv_opt));
to_expr(L, 4), to_expr(L, 5), opaque, mod_idx, use_conv_opt));
}
} else {
if (nargs <= 4) {
get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2),
return push_definition(L, mk_definition(to_name_ext(L, 1), param_names(), to_expr(L, 2),
to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt));
} else {
get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3),
to_expr(L, 4), to_expr(L, 5), opaque, weight, mod_idx, use_conv_opt));
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), to_list_name_ext(L, 2),
to_expr(L, 3), to_expr(L, 4), opaque, weight, mod_idx, use_conv_opt));
}
}
}
@ -694,7 +692,6 @@ static const struct luaL_Reg definition_m[] = {
{"use_conv_opt", safe_function<definition_use_conv_opt>},
{"name", safe_function<definition_get_name>},
{"univ_params", safe_function<definition_get_params>},
{"univ_cnstrs", safe_function<definition_get_level_cnstrs>},
{"type", safe_function<definition_get_type>},
{"value", safe_function<definition_get_value>},
{"weight", safe_function<definition_get_weight>},

22
src/tests/kernel/environment.cpp
View file

@ -20,43 +20,43 @@ static environment add_def(environment const & env, definition const & d) {
static void tst1() {
environment env1;
auto env2 = add_def(env1, mk_definition("Bool", param_names(), level_cnstrs(), mk_Type(), mk_Bool()));
auto env2 = add_def(env1, mk_definition("Bool", param_names(), mk_Type(), mk_Bool()));
lean_assert(!env1.find("Bool"));
lean_assert(env2.find("Bool"));
lean_assert(env2.find("Bool")->get_value() == mk_Bool());
try {
auto env3 = add_def(env2, mk_definition("Bool", param_names(), level_cnstrs(), mk_Type(), mk_Bool()));
auto env3 = add_def(env2, mk_definition("Bool", param_names(), mk_Type(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env4 = add_def(env2, mk_definition("BuggyBool", param_names(), level_cnstrs(), mk_Bool(), mk_Bool()));
auto env4 = add_def(env2, mk_definition("BuggyBool", param_names(), mk_Bool(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env5 = add_def(env2, mk_definition("Type1", param_names(), level_cnstrs(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type()));
auto env5 = add_def(env2, mk_definition("Type1", param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env6 = add_def(env2, mk_definition("Type1", param_names(), level_cnstrs(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l")))));
auto env6 = add_def(env2, mk_definition("Type1", param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l")))));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env7 = add_def(env2, mk_definition("foo", param_names(), level_cnstrs(), mk_Type() >> mk_Type(), mk_Bool()));
auto env7 = add_def(env2, mk_definition("foo", param_names(), mk_Type() >> mk_Type(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
expr A = Const("A");
expr x = Const("x");
auto env3 = add_def(env2, mk_definition("id", param_names(), level_cnstrs(),
auto env3 = add_def(env2, mk_definition("id", param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
expr c = mk_local("c", Bool);
@ -73,16 +73,16 @@ static void tst1() {
static void tst2() {
environment env;
name base("base");
env = add_def(env, mk_var_decl(name(base, 0u), param_names(), level_cnstrs(), Bool >> (Bool >> Bool)));
env = add_def(env, mk_var_decl(name(base, 0u), param_names(), Bool >> (Bool >> Bool)));
expr x = Const("x");
expr y = Const("y");
for (unsigned i = 1; i <= 100; i++) {
expr prev = Const(name(base, i-1));
env = add_def(env, mk_definition(env, name(base, i), param_names(), level_cnstrs(), Bool >> (Bool >> Bool),
env = add_def(env, mk_definition(env, name(base, i), param_names(), Bool >> (Bool >> Bool),
Fun({{x, Bool}, {y, Bool}}, prev(prev(x, y), prev(y, x)))));
}
expr A = Const("A");
env = add_def(env, mk_definition("id", param_names(), level_cnstrs(),
env = add_def(env, mk_definition("id", param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
type_checker checker(env, name_generator("tmp"));
@ -129,7 +129,7 @@ static void tst3() {
expr A = Const("A");
expr x = Const("x");
expr id = Const("id");
env = add_def(env, mk_definition("id", param_names(), level_cnstrs(),
env = add_def(env, mk_definition("id", param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
expr mk = Const("mk");

25
tests/lua/def1.lua
View file

@ -1,7 +1,7 @@
local b = mk_var_decl("bit", Type)
local l1 = mk_param_univ("l1")
local l2 = mk_param_univ("l2")
local p = mk_var_decl("tst", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, mk_arrow(mk_sort(l1), mk_sort(l2)))
local p = mk_var_decl("tst", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)))
assert(p:is_var_decl())
assert(not p:is_axiom())
assert(p:name() == name("tst"))
@ -10,16 +10,11 @@ assert(p:type() == mk_arrow(mk_sort(l1), mk_sort(l2)))
assert(#(p:univ_params()) == 2)
assert(p:univ_params():head() == name("l1"))
assert(p:univ_params():tail():head() == name("l2"))
assert(#(p:univ_cnstrs()) == 2)
assert(p:univ_cnstrs():head():first() == l1)
assert(p:univ_cnstrs():head():second() == l2)
assert(p:univ_cnstrs():tail():head():first() == l2)
assert(p:univ_cnstrs():tail():head():second() == l1)
local ax = mk_axiom("ax", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, mk_arrow(mk_sort(l1), mk_sort(l2)))
local ax = mk_axiom("ax", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)))
assert(ax:is_var_decl())
assert(ax:is_axiom())
assert(ax:name() == name("ax"))
local th = mk_theorem("t1", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0)))
local th = mk_theorem("t1", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0)))
assert(th:is_theorem())
assert(th:is_definition())
assert(th:value() == mk_lambda("x", mk_sort(l1), Var(0)))
@ -53,30 +48,20 @@ assert(not d5:opaque())
assert(d5:weight() == 1)
assert(d5:module_idx() == 3)
assert(d5:use_conv_opt())
local d6 = mk_definition("d6", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, A, B, {opaque=true, weight=5})
local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {opaque=true, weight=5})
assert(d6:type() == A)
assert(d6:value() == B)
assert(#(d6:univ_params()) == 2)
assert(d6:univ_params():head() == name("l1"))
assert(d6:univ_params():tail():head() == name("l2"))
assert(#(d6:univ_cnstrs()) == 2)
assert(d6:univ_cnstrs():head():first() == l1)
assert(d6:univ_cnstrs():head():second() == l2)
assert(d6:univ_cnstrs():tail():head():first() == l2)
assert(d6:univ_cnstrs():tail():head():second() == l1)
assert(d6:opaque())
assert(d6:weight() == 5)
local d7 = mk_definition(env, "d7", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, A, B, {opaque=true, weight=5})
local d7 = mk_definition(env, "d7", {"l1", "l2"}, A, B, {opaque=true, weight=5})
assert(d7:type() == A)
assert(d7:value() == B)
assert(d7:weight() == 1)
assert(#(d7:univ_params()) == 2)
assert(d7:univ_params():head() == name("l1"))
assert(d7:univ_params():tail():head() == name("l2"))
assert(#(d7:univ_cnstrs()) == 2)
assert(d7:univ_cnstrs():head():first() == l1)
assert(d7:univ_cnstrs():head():second() == l2)
assert(d7:univ_cnstrs():tail():head():first() == l2)
assert(d7:univ_cnstrs():tail():head():second() == l1)
assert(d7:opaque())
print("done")