From facdf99e8660e40953c93e5cc26c681f392b3b94 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jun 2016 14:25:29 -0700 Subject: [PATCH] feat(library): add abstract_hash --- library/init/meta/tactic.lean | 4 + src/library/CMakeLists.txt | 2 +- src/library/abstract_expr.cpp | 136 +++++++++++++++++++ src/library/abstract_expr.h | 24 ++++ src/library/cache_helper.h | 22 +++ src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/abstract_expr_tactics.cpp | 24 ++++ src/library/tactic/abstract_expr_tactics.h | 11 ++ src/library/tactic/init_module.cpp | 3 + tests/lean/run/ahash1.lean | 18 +++ 10 files changed, 244 insertions(+), 2 deletions(-) create mode 100644 src/library/abstract_expr.cpp create mode 100644 src/library/abstract_expr.h create mode 100644 src/library/tactic/abstract_expr_tactics.cpp create mode 100644 src/library/tactic/abstract_expr_tactics.h create mode 100644 tests/lean/run/ahash1.lean diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index bdb86afd7d..94b4eb48cf 100644 --- a/library/init/meta/tactic.lean +++ b/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 -/ diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 7b1d36f50e..8457de3d59 100644 --- a/src/library/CMakeLists.txt +++ b/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 diff --git a/src/library/abstract_expr.cpp b/src/library/abstract_expr.cpp new file mode 100644 index 0000000000..229137e1bb --- /dev/null +++ b/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 m_hash_cache; + expr_map 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_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 & m_cache; + buffer 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 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); +} +} diff --git a/src/library/abstract_expr.h b/src/library/abstract_expr.h new file mode 100644 index 0000000000..f028ec56bb --- /dev/null +++ b/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); +} diff --git a/src/library/cache_helper.h b/src/library/cache_helper.h index c733178ce0..22f20b05a7 100644 --- a/src/library/cache_helper.h +++ b/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 +class transparencyless_cache_compatibility_helper { + std::unique_ptr 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(); + } +}; } diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 54ee2a64f4..79ed0a1b78 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/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) diff --git a/src/library/tactic/abstract_expr_tactics.cpp b/src/library/tactic/abstract_expr_tactics.cpp new file mode 100644 index 0000000000..099ff5abae --- /dev/null +++ b/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() { +} +} diff --git a/src/library/tactic/abstract_expr_tactics.h b/src/library/tactic/abstract_expr_tactics.h new file mode 100644 index 0000000000..e7c2803714 --- /dev/null +++ b/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(); +} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 927db5a4cd..cff53ca73a 100644 --- a/src/library/tactic/init_module.cpp +++ b/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(); diff --git a/tests/lean/run/ahash1.lean b/tests/lean/run/ahash1.lean new file mode 100644 index 0000000000..c543e9e2f2 --- /dev/null +++ b/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