From 0d5e346143909fd9415ff88b4711a309dbf6fc93 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Aug 2014 15:48:24 -0700 Subject: [PATCH] fix(library/expr_lt): make sure the builtin order is AC-compatible Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 41 +++++++++++++++++++++------------ src/kernel/expr.h | 8 +++---- src/library/expr_lt.cpp | 8 +++---- src/library/kernel_bindings.cpp | 6 ++--- src/tests/kernel/expr.cpp | 9 ++++---- tests/lua/expr3.lua | 2 +- tests/lua/order.lua | 8 +++++++ 7 files changed, 51 insertions(+), 31 deletions(-) create mode 100644 tests/lua/order.lua diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 63b752735..c63d38806 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -26,6 +26,20 @@ Author: Leonardo de Moura #endif namespace lean { +unsigned add_weight(unsigned w1, unsigned w2) { + unsigned r = w1 + w2; + if (r < w1) + r = std::numeric_limits::max(); // overflow + return r; +} + +unsigned inc_weight(unsigned w) { + if (w < std::numeric_limits::max()) + return w+1; + else + return w; +} + static expr g_dummy(mk_var(0)); expr::expr():expr(g_dummy) {} @@ -150,9 +164,9 @@ void expr_local::dealloc(buffer & todelete) { // Composite expressions expr_composite::expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, - bool has_local, bool has_param_univ, unsigned d, unsigned fv_range): + bool has_local, bool has_param_univ, unsigned w, unsigned fv_range): expr_cell(k, h, has_expr_mv, has_univ_mv, has_local, has_param_univ), - m_depth(d), + m_weight(w), m_free_var_range(fv_range) {} // Expr applications @@ -164,10 +178,10 @@ expr_app::expr_app(expr const & fn, expr const & arg): fn.has_univ_metavar() || arg.has_univ_metavar(), fn.has_local() || arg.has_local(), fn.has_param_univ() || arg.has_param_univ(), - std::max(get_depth(fn), get_depth(arg)) + 1, + inc_weight(add_weight(get_weight(fn), get_weight(arg))), std::max(get_free_var_range(fn), get_free_var_range(arg))), m_fn(fn), m_arg(arg) { - m_hash = ::lean::hash(m_hash, m_depth); + m_hash = ::lean::hash(m_hash, m_weight); } void expr_app::dealloc(buffer & todelete) { dec_ref(m_fn, todelete); @@ -195,11 +209,11 @@ expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr con t.has_univ_metavar() || b.has_univ_metavar(), t.has_local() || b.has_local(), t.has_param_univ() || b.has_param_univ(), - std::max(get_depth(t), get_depth(b)) + 1, + inc_weight(add_weight(get_weight(t), get_weight(b))), std::max(get_free_var_range(t), dec(get_free_var_range(b)))), m_binder(n, t, i), m_body(b) { - m_hash = ::lean::hash(m_hash, m_depth); + m_hash = ::lean::hash(m_hash, m_weight); lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi); } void expr_binding::dealloc(buffer & todelete) { @@ -245,13 +259,10 @@ bool macro_definition::operator<(macro_definition const & other) const { return get_name() < other.get_name(); } -static unsigned max_depth(unsigned num, expr const * args) { +static unsigned add_weight(unsigned num, expr const * args) { unsigned r = 0; - for (unsigned i = 0; i < num; i++) { - unsigned d = get_depth(args[i]); - if (d > r) - r = d; - } + for (unsigned i = 0; i < num; i++) + r = add_weight(r, get_weight(args[i])); return r; } @@ -272,7 +283,7 @@ expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * ar std::any_of(args, args+num, [](expr const & e) { return e.has_univ_metavar(); }), std::any_of(args, args+num, [](expr const & e) { return e.has_local(); }), std::any_of(args, args+num, [](expr const & e) { return e.has_param_univ(); }), - max_depth(num, args) + 1, + inc_weight(add_weight(num, args)), get_free_var_range(num, args)), m_definition(m), m_num_args(num) { @@ -471,14 +482,14 @@ expr mk_Type() { expr Prop = mk_Prop(); expr Type = mk_Type(); -unsigned get_depth(expr const & e) { +unsigned get_weight(expr const & e) { switch (e.kind()) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: return 1; case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Macro: case expr_kind::App: - return static_cast(e.raw())->m_depth; + return static_cast(e.raw())->m_weight; } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 688d6172e..f71e7fa9b 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -200,13 +200,13 @@ public: /** \brief Composite expressions */ class expr_composite : public expr_cell { protected: - unsigned m_depth; + unsigned m_weight; unsigned m_free_var_range; - friend unsigned get_depth(expr const & e); + friend unsigned get_weight(expr const & e); friend unsigned get_free_var_range(expr const & e); public: expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_local, - bool has_param_univ, unsigned d, unsigned fv_range); + bool has_param_univ, unsigned w, unsigned fv_range); }; /** \brief Metavariables and local constants */ @@ -589,7 +589,7 @@ inline bool has_univ_metavar(expr const & e) { return e.has_univ_metavar(); } bool has_expr_metavar_strict(expr const & e); inline bool has_local(expr const & e) { return e.has_local(); } inline bool has_param_univ(expr const & e) { return e.has_param_univ(); } -unsigned get_depth(expr const & e); +unsigned get_weight(expr const & e); /** \brief Return \c R s.t. the de Bruijn index of all free variables occurring in \c e is in the interval [0, R). diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index ee45fcdde..9c0f534e8 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -10,10 +10,10 @@ Author: Leonardo de Moura namespace lean { bool is_lt(expr const & a, expr const & b, bool use_hash) { if (is_eqp(a, b)) return false; - unsigned da = get_depth(a); - unsigned db = get_depth(b); - if (da < db) return true; - if (da > db) return false; + unsigned wa = get_weight(a); + unsigned wb = get_weight(b); + if (wa < wb) return true; + if (wa > wb) return false; if (a.kind() != b.kind()) return a.kind() < b.kind(); if (use_hash) { if (a.hash() < b.hash()) return true; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 6f068db66..36202e9ea 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -581,8 +581,8 @@ static int binding_info(lua_State * L) { return push_binder_info(L, binding_info static int expr_occurs(lua_State * L) { return push_boolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); } static int expr_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); } -static int expr_hash(lua_State * L) { return push_integer(L, to_expr(L, 1).hash()); } -static int expr_depth(lua_State * L) { return push_integer(L, get_depth(to_expr(L, 1))); } +static int expr_hash(lua_State * L) { return push_integer(L, to_expr(L, 1).hash()); } +static int expr_weight(lua_State * L) { return push_integer(L, get_weight(to_expr(L, 1))); } static int expr_is_lt(lua_State * L) { int nargs = lua_gettop(L); return push_boolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), nargs == 3 && lua_toboolean(L, 3))); @@ -630,7 +630,7 @@ static const struct luaL_Reg expr_m[] = { {"fn", safe_function}, {"fields", safe_function}, {"data", safe_function}, - {"depth", safe_function}, + {"weight", safe_function}, {"binding_name", safe_function}, {"binding_domain", safe_function}, {"binding_body", safe_function}, diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index d4d489b9c..16107d0f4 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "util/test.h" #include "kernel/expr.h" #include "kernel/expr_sets.h" @@ -68,11 +69,11 @@ static expr mk_dag(unsigned depth, bool _closed = false) { } static void tst2() { - expr r1 = mk_dag(20); - expr r2 = mk_dag(20); + expr r1 = mk_dag(40); + expr r2 = mk_dag(40); lean_assert(r1 == r2); - std::cout << get_depth(r1) << "\n"; - lean_assert_eq(get_depth(r1), 41); + std::cout << get_weight(r1) << "\n"; + lean_assert(get_weight(r1) == std::numeric_limits::max()); } static expr mk_big(expr f, unsigned depth, unsigned val) { diff --git a/tests/lua/expr3.lua b/tests/lua/expr3.lua index 245388455..9b97b502a 100644 --- a/tests/lua/expr3.lua +++ b/tests/lua/expr3.lua @@ -95,5 +95,5 @@ assert(a:occurs(f(a))) enable_expr_caching(false) assert(not f(a):is_eqp(f(a))) assert(f(a):arg():is_eqp(a)) -assert(f(a):depth() == 2) +assert(f(a):weight() == 3) print(f(a):hash()) diff --git a/tests/lua/order.lua b/tests/lua/order.lua new file mode 100644 index 000000000..ec2be1b2a --- /dev/null +++ b/tests/lua/order.lua @@ -0,0 +1,8 @@ +local mul = Const("mul") +local div = Const("div") +local z = Const("z") +local x = Const("x") +local y = Const("y") +local t1 = mul(z, mul(div(x, y), y)) +local t2 = mul(div(x, y), mul(z, y)) +assert(t1 < t2)