feat(kernel/expr): add hash_bi function that takes binder information into account

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<unsigned>::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");

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,

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_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_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(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_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<expr_is_equal>},
     {"is_bi_equal",      safe_function<expr_is_bi_equal>},
     {"hash",             safe_function<expr_hash>},
+    {"hash_bi",          safe_function<expr_hash_bi>},
     {"tag",              safe_function<expr_tag>},
     {"set_tag",          safe_function<expr_set_tag>},
     {0, 0}

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())
+*)