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

refactor(kernel): rename get_weight to get_height at declaration

Browse source 
Motivation:
- It is the standard name for the concept: declaration height
- Avoid confusion with the expression weight
This commit is contained in:
Leonardo de Moura 2015-06-30 12:11:13 -07:00
parent 1e6550eda6
commit e635d9be9f
9 changed files with 75 additions and 76 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/kernel/declaration.cpp
View file

@ -16,8 +16,7 @@ struct declaration::cell {
expr m_type;
bool m_theorem;
optional<expr> m_value; // if none, then declaration is actually a postulate
// The following fields are only meaningful for definitions (which are not theorems)
unsigned m_weight;
unsigned m_height; // definitional height
// The following field affects the convertability checker.
// Let f be this definition, then if the following field is true,
// then whenever we are checking whether
@ -29,11 +28,11 @@ struct declaration::cell {
cell(name const & n, level_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_use_conv_opt(false) {}
m_height(0), m_use_conv_opt(false) {}
cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
unsigned w, bool use_conv_opt):
unsigned h, bool use_conv_opt):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
m_value(v), m_weight(w), m_use_conv_opt(use_conv_opt) {}
m_value(v), m_height(h), m_use_conv_opt(use_conv_opt) {}
};
static declaration * g_dummy = nullptr;
@ -58,37 +57,37 @@ unsigned declaration::get_num_univ_params() const { return length(get_univ_param
expr const & declaration::get_type() const { return m_ptr->m_type; }
expr const & declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
unsigned declaration::get_weight() const { return m_ptr->m_weight; }
unsigned declaration::get_height() const { return m_ptr->m_height; }
bool declaration::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
unsigned weight, bool use_conv_opt) {
return declaration(new declaration::cell(n, params, t, false, v, weight, use_conv_opt));
unsigned height, bool use_conv_opt) {
return declaration(new declaration::cell(n, params, t, false, v, height, use_conv_opt));
}
static unsigned get_max_weight(environment const & env, expr const & v) {
unsigned w = 0;
static unsigned get_max_height(environment const & env, expr const & v) {
unsigned h = 0;
for_each(v, [&](expr const & e, unsigned) {
if (is_constant(e)) {
auto d = env.find(const_name(e));
if (d && d->get_weight() > w)
w = d->get_weight();
if (d && d->get_height() > h)
h = d->get_height();
}
return true;
});
return w;
return h;
}
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool use_conv_opt) {
unsigned w = get_max_weight(env, v);
return mk_definition(n, params, t, v, w+1, use_conv_opt);
unsigned h = get_max_height(env, v);
return mk_definition(n, params, t, v, h+1, use_conv_opt);
}
declaration mk_theorem(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v) {
unsigned w = get_max_weight(env, v);
return declaration(new declaration::cell(n, params, t, true, v, w+1, true));
unsigned h = get_max_height(env, v);
return declaration(new declaration::cell(n, params, t, true, v, h+1, true));
}
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned weight) {
return declaration(new declaration::cell(n, params, t, true, v, weight, true));
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned height) {
return declaration(new declaration::cell(n, params, t, true, v, height, true));
}
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, true));

6
src/kernel/declaration.h
View file

@ -50,13 +50,13 @@ public:
expr const & get_type() const;
expr const & get_value() const;
unsigned get_weight() const;
unsigned get_height() const;
bool use_conv_opt() const;
friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool use_conv_opt);
friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
unsigned weight, bool use_conv_opt);
unsigned height, bool use_conv_opt);
friend declaration mk_theorem(environment const &, name const &, level_param_names const &, expr const &, expr const &);
friend declaration mk_theorem(name const &, level_param_names const &, expr const &, expr const &, unsigned);
friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
@ -68,7 +68,7 @@ inline optional<declaration> some_declaration(declaration const & o) { return op
inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
unsigned weight = 0, bool use_conv_opt = true);
unsigned height = 0, bool use_conv_opt = true);
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool use_conv_opt = true);
declaration mk_theorem(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v);

38
src/kernel/default_converter.cpp
View file

@ -118,13 +118,13 @@ bool default_converter::is_opaque(declaration const &) const {
return false;
}
/** \brief Expand \c e if it is non-opaque constant with weight >= w */
expr default_converter::unfold_name_core(expr e, unsigned w) {
/** \brief Expand \c e if it is non-opaque constant with height >= h */
expr default_converter::unfold_name_core(expr e, unsigned h) {
if (is_constant(e)) {
if (auto d = m_env.find(const_name(e))) {
if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w &&
if (d->is_definition() && !is_opaque(*d) && d->get_height() >= h &&
length(const_levels(e)) == d->get_num_univ_params())
return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), w);
return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h);
}
}
return e;
@ -134,12 +134,12 @@ expr default_converter::unfold_name_core(expr e, unsigned w) {
\brief Expand constants and application where the function is a constant.
The unfolding is only performend if the constant corresponds to
a non-opaque definition with weight >= w.
a non-opaque definition with height >= h.
*/
expr default_converter::unfold_names(expr const & e, unsigned w) {
expr default_converter::unfold_names(expr const & e, unsigned h) {
if (is_app(e)) {
expr f0 = get_app_fn(e);
expr f = unfold_name_core(f0, w);
expr f = unfold_name_core(f0, h);
if (is_eqp(f, f0)) {
return e;
} else {
@ -148,7 +148,7 @@ expr default_converter::unfold_names(expr const & e, unsigned w) {
return mk_rev_app(f, args);
}
} else {
return unfold_name_core(e, w);
return unfold_name_core(e, h);
}
}
@ -168,15 +168,15 @@ optional<declaration> default_converter::is_delta(expr const & e) const {
/**
\brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
weight greater than or equal to \c w.
height greater than or equal to \c h.
This method is based on <tt>whnf_core(expr const &)</tt> and \c unfold_names.
\remark This method does not use normalization extensions attached in the environment.
*/
expr default_converter::whnf_core(expr e, unsigned w) {
expr default_converter::whnf_core(expr e, unsigned h) {
while (true) {
expr new_e = unfold_names(whnf_core(e), w);
expr new_e = unfold_names(whnf_core(e), h);
if (is_eqp(e, new_e))
return e;
e = new_e;
@ -489,13 +489,13 @@ auto default_converter::lazy_delta_reduction_step(expr & t_n, expr & s_n, constr
} else if (!d_t && d_s) {
s_n = whnf_core(unfold_names(s_n, 0));
} else if (!d_t->is_theorem() && d_s->is_theorem()) {
t_n = whnf_core(unfold_names(t_n, d_t->get_weight()));
t_n = whnf_core(unfold_names(t_n, d_t->get_height()));
} else if (!d_s->is_theorem() && d_t->is_theorem()) {
s_n = whnf_core(unfold_names(s_n, d_s->get_weight()));
} else if (!d_t->is_theorem() && d_t->get_weight() > d_s->get_weight()) {
t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1));
} else if (!d_s->is_theorem() && d_t->get_weight() < d_s->get_weight()) {
s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1));
s_n = whnf_core(unfold_names(s_n, d_s->get_height()));
} else if (!d_t->is_theorem() && d_t->get_height() > d_s->get_height()) {
t_n = whnf_core(unfold_names(t_n, d_s->get_height() + 1));
} else if (!d_s->is_theorem() && d_t->get_height() < d_s->get_height()) {
s_n = whnf_core(unfold_names(s_n, d_t->get_height() + 1));
} else {
if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) {
// If t_n and s_n are both applications of the same (non-opaque) definition,
@ -522,8 +522,8 @@ auto default_converter::lazy_delta_reduction_step(expr & t_n, expr & s_n, constr
}
}
}
t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1));
s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1));
t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1));
s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1));
}
switch (quick_is_def_eq(t_n, s_n, cs)) {
case l_true: return reduction_status::DefEqual;

38
src/library/kernel_bindings.cpp
View file

@ -749,7 +749,7 @@ static int declaration_get_value(lua_State * L) {
return push_expr(L, to_declaration(L, 1).get_value());
throw exception("arg #1 must be a definition");
}
static int declaration_get_weight(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_weight()); }
static int declaration_get_height(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_height()); }
static int mk_constant_assumption(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
@ -764,58 +764,58 @@ static int mk_axiom(lua_State * L) {
else
return push_declaration(L, mk_axiom(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
}
static void get_definition_args(lua_State * L, int idx, unsigned & weight, bool & use_conv_opt) {
static void get_definition_args(lua_State * L, int idx, unsigned & height, bool & use_conv_opt) {
use_conv_opt = get_bool_named_param(L, idx, "use_conv_opt", use_conv_opt);
weight = get_uint_named_param(L, idx, "weight", weight);
height = get_uint_named_param(L, idx, "height", height);
}
static int mk_definition(lua_State * L) {
int nargs = lua_gettop(L);
unsigned weight = 0; bool use_conv_opt = true;
unsigned height = 0; bool use_conv_opt = true;
if (nargs < 3) {
throw exception("mk_definition must have at least 3 arguments");
} else if (is_environment(L, 1)) {
if (nargs < 4) {
throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment");
} else if (is_expr(L, 3)) {
get_definition_args(L, 5, weight, use_conv_opt);
get_definition_args(L, 5, height, use_conv_opt);
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
to_expr(L, 3), to_expr(L, 4), use_conv_opt));
} else {
get_definition_args(L, 6, weight, use_conv_opt);
get_definition_args(L, 6, height, use_conv_opt);
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
to_expr(L, 4), to_expr(L, 5), use_conv_opt));
}
} else {
if (is_expr(L, 2)) {
get_definition_args(L, 4, weight, use_conv_opt);
get_definition_args(L, 4, height, use_conv_opt);
return push_declaration(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
to_expr(L, 3), weight, use_conv_opt));
to_expr(L, 3), height, use_conv_opt));
} else {
get_definition_args(L, 5, weight, use_conv_opt);
get_definition_args(L, 5, height, use_conv_opt);
return push_declaration(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
to_expr(L, 3), to_expr(L, 4), weight, use_conv_opt));
to_expr(L, 3), to_expr(L, 4), height, use_conv_opt));
}
}
}
static void get_definition_args(lua_State * L, int idx, unsigned & weight) {
weight = get_uint_named_param(L, idx, "weight", weight);
static void get_definition_args(lua_State * L, int idx, unsigned & height) {
height = get_uint_named_param(L, idx, "height", height);
}
static int mk_theorem(lua_State * L) {
int nargs = lua_gettop(L);
unsigned weight = 0;
unsigned height = 0;
if (nargs == 3) {
return push_declaration(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3), 0));
} else if (nargs == 4) {
if (is_expr(L, 4)) {
return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4),
weight));
height));
} else {
get_definition_args(L, 4, weight);
return push_declaration(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3), weight));
get_definition_args(L, 4, height);
return push_declaration(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3), height));
}
} else {
get_definition_args(L, 5, weight);
return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4), weight));
get_definition_args(L, 5, height);
return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4), height));
}
}
@ -830,7 +830,7 @@ static const struct luaL_Reg declaration_m[] = {
{"univ_params", safe_function<declaration_get_params>},
{"type", safe_function<declaration_get_type>},
{"value", safe_function<declaration_get_value>},
{"weight", safe_function<declaration_get_weight>},
{"height", safe_function<declaration_get_height>},
{0, 0}
};

2
src/library/kernel_serializer.cpp
View file

@ -288,7 +288,7 @@ serializer & operator<<(serializer & s, declaration const & d) {
s << k << d.get_name() << d.get_univ_params() << d.get_type();
if (d.is_definition()) {
s << d.get_value();
s << d.get_weight();
s << d.get_height();
}
return s;
}

4
src/library/unfold_macros.cpp
View file

@ -144,11 +144,11 @@ declaration unfold_untrusted_macros(environment const & env, declaration const &
if (d.is_theorem()) {
expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v,
d.get_weight());
d.get_height());
} else if (d.is_definition()) {
expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
return mk_definition(d.get_name(), d.get_univ_params(), new_t, new_v,
d.get_weight(), d.use_conv_opt());
d.get_height(), d.use_conv_opt());
} else if (d.is_axiom()) {
return mk_axiom(d.get_name(), d.get_univ_params(), new_t);
} else if (d.is_constant_assumption()) {

4
src/library/update_declaration.cpp
View file

@ -28,10 +28,10 @@ static declaration update_declaration(declaration d, optional<level_param_names>
if (is_eqp(d.get_type(), _type) && is_eqp(d.get_value(), _value) && is_eqp(d.get_univ_params(), _ps))
return d;
if (d.is_theorem())
return mk_theorem(d.get_name(), _ps, _type, _value, d.get_weight());
return mk_theorem(d.get_name(), _ps, _type, _value, d.get_height());
else
return mk_definition(d.get_name(), _ps, _type, _value,
d.get_weight(), d.use_conv_opt());
d.get_height(), d.use_conv_opt());
}
}

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

@ -109,7 +109,7 @@ static void tst2() {
expr c2 = mk_local("c2", Prop);
expr id = Const("id");
std::cout << checker.whnf(mk_app(f3, c1, c2)).first << "\n";
lean_assert_eq(env.find(name(base, 98))->get_weight(), 98);
lean_assert_eq(env.find(name(base, 98))->get_height(), 98);
lean_assert(checker.is_def_eq(mk_app(f98, c1, c2), mk_app(f97, mk_app(f97, c1, c2), mk_app(f97, c2, c1))).first);
lean_assert(checker.is_def_eq(mk_app(f98, c1, mk_app(id, Prop, mk_app(id, Prop, c2))), mk_app(f97, mk_app(f97, c1, mk_app(id, Prop, c2)), mk_app(f97, c2, c1))).first);
name_set s;

20
tests/lua/def1.lua
View file

@ -29,31 +29,31 @@ assert(th2:name() == name("t2"))
local d = mk_definition("d1", A, B)
assert(d:is_definition())
assert(not d:is_theorem())
assert(d:weight() == 0)
assert(d:height() == 0)
assert(d:use_conv_opt())
assert(d:name() == name("d1"))
assert(d:value() == B)
local d2 = mk_definition("d2", A, B, nil)
local d3 = mk_definition("d3", A, B, {weight=100, use_conv_opt=false})
assert(d3:weight() == 100)
local d3 = mk_definition("d3", A, B, {height=100, use_conv_opt=false})
assert(d3:height() == 100)
assert(not d3:use_conv_opt())
local env = bare_environment()
local d4 = mk_definition(env, "bool", Type, Prop)
assert(d4:weight() == 1)
local d5 = mk_definition(env, "bool", Type, Prop, {weight=100, use_conv_opt=true})
assert(d5:weight() == 1)
assert(d4:height() == 1)
local d5 = mk_definition(env, "bool", Type, Prop, {height=100, use_conv_opt=true})
assert(d5:height() == 1)
assert(d5:use_conv_opt())
local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {weight=5})
local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {height=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:weight() == 5)
local d7 = mk_definition(env, "d7", {"l1", "l2"}, A, B, {weight=5})
assert(d6:height() == 5)
local d7 = mk_definition(env, "d7", {"l1", "l2"}, A, B, {height=5})
assert(d7:type() == A)
assert(d7:value() == B)
assert(d7:weight() == 1)
assert(d7:height() == 1)
assert(#(d7:univ_params()) == 2)
assert(d7:univ_params():head() == name("l1"))
assert(d7:univ_params():tail():head() == name("l2"))