From a0c37b231fed9302c7b6811688aee898508a366c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Sep 2014 16:19:01 -0700 Subject: [PATCH] feat(kernel/expr): add hash_bi function that takes binder information into account --- src/kernel/expr.cpp | 20 ++++++++++++++++++++ src/kernel/expr.h | 5 +++++ src/library/kernel_bindings.cpp | 10 ++++++---- tests/lean/run/hash.lean | 9 +++++++++ 4 files changed, 40 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/hash.lean diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 6a324e11f..dda693d42 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -133,6 +133,10 @@ void expr_const::dealloc() { get_const_allocator().recycle(this); } +unsigned binder_info::hash() const { + return (m_implicit << 3) | (m_cast << 2) | (m_contextual << 1) | m_strict_implicit; +} + // Expr metavariables and local variables DEF_THREAD_MEMORY_POOL(get_mlocal_allocator, sizeof(expr_mlocal)); expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t): @@ -637,6 +641,22 @@ expr infer_implicit(expr const & t, bool strict) { return infer_implicit(t, std::numeric_limits::max(), strict); } +unsigned hash_bi(expr const & e) { + unsigned h = e.hash(); + for_each(e, [&](expr const & e, unsigned) { + if (is_binding(e)) { + h = hash(h, hash(binding_name(e).hash(), binding_info(e).hash())); + } else if (is_local(e)) { + h = hash(h, hash(mlocal_name(e).hash(), local_info(e).hash())); + return false; // do not visit type + } else if (is_metavar(e)) { + return false; // do not visit type + } + return true; + }); + return h; +} + void initialize_expr() { g_dummy = new expr(mk_var(0)); g_default_name = new name("a"); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index ff3aecf80..f0cead70d 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -238,6 +238,7 @@ public: bool is_cast() const { return m_cast; } bool is_contextual() const { return m_contextual; } bool is_strict_implicit() const { return m_strict_implicit; } + unsigned hash() const; binder_info update_contextual(bool f) const { return binder_info(m_implicit, m_cast, f, m_strict_implicit); } }; @@ -249,6 +250,10 @@ inline binder_info mk_contextual_info(bool f) { return binder_info(false, false, bool operator==(binder_info const & i1, binder_info const & i2); inline bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); } +/** \brief Compute a hash code that takes binder_info into account. + \remark This information is not cached like hash(). */ +unsigned hash_bi(expr const & e); + /** \brief expr_mlocal subclass for local constants. */ class expr_local : public expr_mlocal { // The name used in the binder that generate this local, diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 211e9f1da..f3aee9954 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -580,10 +580,11 @@ static int binding_domain(lua_State * L) { return push_expr(L, binding_domain(to static int binding_body(lua_State * L) { return push_expr(L, binding_body(to_binding(L, 1))); } static int binding_info(lua_State * L) { return push_binder_info(L, binding_info(to_binding(L, 1))); } -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_weight(lua_State * L) { return push_integer(L, get_weight(to_expr(L, 1))); } +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_hash_bi(lua_State * L) { return push_integer(L, hash_bi(to_expr(L, 1))); } +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))); @@ -653,6 +654,7 @@ static const struct luaL_Reg expr_m[] = { {"is_equal", safe_function}, {"is_bi_equal", safe_function}, {"hash", safe_function}, + {"hash_bi", safe_function}, {"tag", safe_function}, {"set_tag", safe_function}, {0, 0} diff --git a/tests/lean/run/hash.lean b/tests/lean/run/hash.lean new file mode 100644 index 000000000..0fb3fb789 --- /dev/null +++ b/tests/lean/run/hash.lean @@ -0,0 +1,9 @@ +definition id1 {A : Type} (a : A) : A := a +definition id2 (A : Type) (a : A) : A := a + +(* + local t1 = get_env():find("id1"):type() + local t2 = get_env():find("id2"):type() + assert(t1:hash() == t2:hash()) + assert(t1:hash_bi() ~= t2:hash_bi()) +*)