feat(library): add abstract_hash

library/init/meta/tactic.lean

@@ -165,6 +165,10 @@ meta_constant get_univ_assignment : level → tactic level
    Fail if argument is not a meta-variable or if it is not assigned. -/
 meta_constant get_assignment : expr → tactic expr
 meta_constant mk_fresh_name : tactic name
+/- Return a hash code for expr that ignores inst_implicit arguments,
+   and proofs. -/
+meta_constant abstract_hash : expr → tactic nat
+
 open list nat
 
 /- Add (H : T := pr) to the current goal -/

src/library/CMakeLists.txt

@@ -13,7 +13,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   aux_recursors.cpp norm_num.cpp trace.cpp
   attribute_manager.cpp error_handling.cpp unification_hint.cpp
   local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp lazy_abstraction.cpp
-  fun_info.cpp congr_lemma.cpp
+  fun_info.cpp congr_lemma.cpp abstract_expr.cpp
   # Legacy -- The following files will be eventually deleted
   normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp
   unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp

src/library/abstract_expr.cpp

@@ -0,0 +1,136 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/hash.h"
+#include "kernel/expr_maps.h"
+#include "kernel/instantiate.h"
+#include "library/abstract_expr.h"
+#include "library/cache_helper.h"
+#include "library/fun_info.h"
+
+namespace lean {
+struct abstract_expr_cache {
+    environment        m_env;
+    expr_map<unsigned> m_hash_cache;
+    expr_map<unsigned> m_weight_cache;
+    abstract_expr_cache(environment const & env):m_env(env) {}
+    environment const & env() const { return m_env; }
+};
+
+/* The abstract_expr_cache does not depend on the transparency mode */
+typedef transparencyless_cache_compatibility_helper<abstract_expr_cache>
+abstract_expr_cache_helper;
+
+MK_THREAD_LOCAL_GET_DEF(abstract_expr_cache_helper, get_aech);
+
+abstract_expr_cache & get_abstract_cache_for(type_context const & ctx) {
+    return get_aech().get_cache_for(ctx);
+}
+
+#define EASY_HASH(e) {                                  \
+    switch (e.kind()) {                                 \
+    case expr_kind::Constant: case expr_kind::Local:    \
+    case expr_kind::Meta:     case expr_kind::Sort:     \
+    case expr_kind::Var:                                \
+        return e.hash();                                \
+    default:                                            \
+        break;                                          \
+    }                                                   \
+}
+
+struct abstract_hash_fn {
+    type_context &                   m_ctx;
+    expr_map<unsigned> &             m_cache;
+    buffer<expr>                     m_locals;
+    type_context::transparency_scope m_scope;
+
+    abstract_hash_fn(type_context & ctx):
+        m_ctx(ctx),
+        m_cache(get_abstract_cache_for(ctx).m_hash_cache),
+        m_scope(m_ctx, transparency_mode::All) {}
+
+    expr instantiate_locals(expr const & e) {
+        return instantiate_rev(e, m_locals.size(), m_locals.data());
+    }
+
+    expr push_local(name const & pp_name, expr const & type) {
+        expr l = m_ctx.push_local(pp_name, instantiate_locals(type));
+        m_locals.push_back(l);
+        return l;
+    }
+
+    expr push_let(name const & pp_name, expr const & type, expr const & value) {
+        expr l = m_ctx.push_let(pp_name, instantiate_locals(type), instantiate_locals(value));
+        m_locals.push_back(l);
+        return l;
+    }
+
+    void pop() {
+        m_locals.pop_back();
+    }
+
+    unsigned hash(expr const & e) {
+        EASY_HASH(e);
+
+        auto it = m_cache.find(e);
+        if (it != m_cache.end())
+            return it->second;
+
+        unsigned r = 0;
+
+        switch (e.kind()) {
+        case expr_kind::Constant: case expr_kind::Local:
+        case expr_kind::Meta:     case expr_kind::Sort:
+        case expr_kind::Var:
+            lean_unreachable();
+        case expr_kind::Lambda:
+        case expr_kind::Pi:
+            r = hash(binding_domain(e));
+            push_local(binding_name(e), binding_domain(e));
+            r = ::lean::hash(r, hash(binding_body(e)));
+            pop();
+            break;
+        case expr_kind::Let:
+            r = ::lean::hash(hash(let_type(e)), hash(let_value(e)));
+            push_let(let_name(e), let_type(e), let_value(e));
+            r = ::lean::hash(r, hash(let_body(e)));
+            pop();
+            break;
+        case expr_kind::Macro:
+            r = lean::hash(macro_num_args(e), [&](unsigned i) { return hash(macro_arg(e, i)); },
+                           macro_def(e).hash());
+            break;
+        case expr_kind::App:
+            buffer<expr> args;
+            expr const & f = get_app_args(e, args);
+            r = hash(f);
+            fun_info info  = get_fun_info(m_ctx, instantiate_locals(f), args.size());
+            unsigned i = 0;
+            for (param_info const & pinfo : info.get_params_info()) {
+                lean_assert(i < args.size());
+                if (!pinfo.is_inst_implicit() && !pinfo.is_prop()) {
+                    r = ::lean::hash(r, hash(args[i]));
+                }
+                i++;
+            }
+            /* Remark: the property (i == args.size()) does not necessarily hold here.
+               This can happen whenever the arity of f depends on its arguments. */
+            break;
+        }
+        m_cache.insert(mk_pair(e, r));
+        return r;
+    }
+
+    unsigned operator()(expr const & e) {
+        return hash(e);
+    }
+};
+
+unsigned abstract_hash(type_context & ctx, expr const & e) {
+    EASY_HASH(e);
+    return abstract_hash_fn(ctx)(e);
+}
+}

src/library/abstract_expr.h

@@ -0,0 +1,24 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/type_context.h"
+
+namespace lean {
+/** \brief Return a hash code for \c e that ignores instance parameters
+    (and proofs) in \c e.
+
+    Example: the following two instances have the same hashcode
+       (@add nat nat_has_add a b)
+       (@add nat (add_monoid_has_add nat nat_is_monoid) a b) */
+unsigned abstract_hash(type_context & ctx, expr const & e);
+/** \brief Weight function that ignores the type class instances in \c e.  */
+unsigned abstract_weight(type_context & ctx, expr const & e);
+/** \brief Equality function that ignores type class instances. */
+bool abstract_eq(type_context & ctx, expr const & e1, expr const & e2);
+/** \brief Less than function that ignores type class instances. */
+bool abstract_lt(type_context & ctx, expr const & e1, expr const & e2);
+}

src/library/cache_helper.h

@@ -31,4 +31,26 @@ public:
         for (unsigned i = 0; i < 4; i++) m_cache_ptr[i].reset();
     }
 };
+
+/** \brief Helper class for making sure we have a cache that is compatible
+    with a given environment. */
+template<typename Cache>
+class transparencyless_cache_compatibility_helper {
+    std::unique_ptr<Cache> m_cache_ptr;
+public:
+    Cache & get_cache_for(environment const & env) {
+        if (!m_cache_ptr || !is_eqp(env, m_cache_ptr->env())) {
+            m_cache_ptr.reset(new Cache(env));
+        }
+        return *m_cache_ptr.get();
+    }
+
+    Cache & get_cache_for(type_context const & ctx) {
+        return get_cache_for(ctx.env());
+    }
+
+    void clear() {
+        m_cache_ptr.reset();
+    }
+};
 }

src/library/tactic/CMakeLists.txt

@@ -2,5 +2,5 @@ add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp
   revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
   app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp
   change_tactic.cpp assert_tactic.cpp apply_tactic.cpp
-  fun_info_tactics.cpp congr_lemma_tactics.cpp
+  fun_info_tactics.cpp congr_lemma_tactics.cpp abstract_expr_tactics.cpp
   elaborate.cpp init_module.cpp)

src/library/tactic/abstract_expr_tactics.cpp

@@ -0,0 +1,24 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/abstract_expr.h"
+#include "library/vm/vm_expr.h"
+#include "library/vm/vm_nat.h"
+#include "library/tactic/tactic_state.h"
+
+namespace lean {
+vm_obj tactic_abstract_hash(vm_obj const & e, vm_obj const & s) {
+    type_context_scope ctx(s);
+    unsigned h = abstract_hash(ctx, to_expr(e)) % LEAN_MAX_SMALL_NAT;
+    return mk_tactic_success(mk_vm_simple(h), to_tactic_state(s));
+}
+
+void initialize_abstract_expr_tactics() {
+    DECLARE_VM_BUILTIN(name({"tactic", "abstract_hash"}), tactic_abstract_hash);
+}
+void finalize_abstract_expr_tactics() {
+}
+}

src/library/tactic/abstract_expr_tactics.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_abstract_expr_tactics();
+void finalize_abstract_expr_tactics();
+}

src/library/tactic/init_module.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/tactic/apply_tactic.h"
 #include "library/tactic/fun_info_tactics.h"
 #include "library/tactic/congr_lemma_tactics.h"
+#include "library/tactic/abstract_expr_tactics.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/defeq_simplifier/init_module.h"
 
@@ -35,12 +36,14 @@ void initialize_tactic_module() {
     initialize_apply_tactic();
     initialize_fun_info_tactics();
     initialize_congr_lemma_tactics();
+    initialize_abstract_expr_tactics();
     initialize_elaborate();
     initialize_defeq_simplifier_module();
 }
 void finalize_tactic_module() {
     finalize_defeq_simplifier_module();
     finalize_elaborate();
+    finalize_abstract_expr_tactics();
     finalize_congr_lemma_tactics();
     finalize_fun_info_tactics();
     finalize_apply_tactic();

tests/lean/run/ahash1.lean

@@ -0,0 +1,18 @@
+open tactic
+
+constant nat_has_add1 : has_add nat
+constant nat_has_add2 : has_add nat
+
+example (a b : nat)
+  (H1 : @add nat nat_has_add1 a b = 0)
+  (H2 : @add nat nat_has_add2 a b = 0)
+  (H3 : @add nat nat_has_add1 b a = 0)
+  : true :=
+by do
+  h₁ ← get_local "H1" >>= infer_type >>= abstract_hash,
+  h₂ ← get_local "H2" >>= infer_type >>= abstract_hash,
+  h₃ ← get_local "H3" >>= infer_type >>= abstract_hash,
+  trace $ to_string h₁ + " " + to_string h₂ + " " + to_string h₃,
+  if h₁ ≠ h₂ then fail "ERROR" else skip,
+  if h₁ = h₃ then fail "UNEXPECTED" else skip,
+  constructor