From e635d9be9fc414f5882addcefeea239def0680f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 30 Jun 2015 12:11:13 -0700 Subject: [PATCH] refactor(kernel): rename get_weight to get_height at declaration Motivation: - It is the standard name for the concept: declaration height - Avoid confusion with the expression weight --- src/kernel/declaration.cpp | 37 ++++++++++++++--------------- src/kernel/declaration.h | 6 ++--- src/kernel/default_converter.cpp | 38 +++++++++++++++--------------- src/library/kernel_bindings.cpp | 38 +++++++++++++++--------------- src/library/kernel_serializer.cpp | 2 +- src/library/unfold_macros.cpp | 4 ++-- src/library/update_declaration.cpp | 4 ++-- src/tests/kernel/environment.cpp | 2 +- tests/lua/def1.lua | 20 ++++++++-------- 9 files changed, 75 insertions(+), 76 deletions(-) diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 742190036c..9053949a8c 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -16,8 +16,7 @@ struct declaration::cell { expr m_type; bool m_theorem; optional 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)); diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index bc2cfcd48c..3df4a43dc8 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -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 some_declaration(declaration const & o) { return op inline optional some_declaration(declaration && o) { return optional(std::forward(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); diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index 9ce58ba696..ca561a0db4 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -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 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 whnf_core(expr const &) 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; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index e1180b8725..69b5336672 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -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}, {"type", safe_function}, {"value", safe_function}, - {"weight", safe_function}, + {"height", safe_function}, {0, 0} }; diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 9510b346fb..b95d69ad45 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -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; } diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp index 3b22de4335..2135ae6eeb 100644 --- a/src/library/unfold_macros.cpp +++ b/src/library/unfold_macros.cpp @@ -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()) { diff --git a/src/library/update_declaration.cpp b/src/library/update_declaration.cpp index 25338ddfb5..14689d587c 100644 --- a/src/library/update_declaration.cpp +++ b/src/library/update_declaration.cpp @@ -28,10 +28,10 @@ static declaration update_declaration(declaration d, optional 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()); } } diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index e5e0edf376..597fa6a467 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -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; diff --git a/tests/lua/def1.lua b/tests/lua/def1.lua index 519cf57038..ec50c074c6 100644 --- a/tests/lua/def1.lua +++ b/tests/lua/def1.lua @@ -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"))