From 3974a72a739512aefc457edddb672ab45ff38da5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jun 2016 14:50:23 -0700 Subject: [PATCH] feat(library/abstract_expr): add abstract_weight --- library/init/meta/tactic.lean | 4 +- src/library/abstract_expr.cpp | 93 +++++++++++++++++++- src/library/tactic/abstract_expr_tactics.cpp | 7 ++ tests/lean/run/ahash1.lean | 9 ++ tests/lean/run/aweight1.lean | 30 +++++++ 5 files changed, 139 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/aweight1.lean diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 94b4eb48cf..4ac72b520e 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -168,7 +168,9 @@ 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 - +/- Return the "weight" of the given expr while ignoring inst_implicit arguments, + and proofs. -/ +meta_constant abstract_weight : expr → tactic nat open list nat /- Add (H : T := pr) to the current goal -/ diff --git a/src/library/abstract_expr.cpp b/src/library/abstract_expr.cpp index 229137e1bb..972aba93d5 100644 --- a/src/library/abstract_expr.cpp +++ b/src/library/abstract_expr.cpp @@ -41,15 +41,15 @@ abstract_expr_cache & get_abstract_cache_for(type_context const & ctx) { } \ } -struct abstract_hash_fn { +struct abstract_fn { type_context & m_ctx; expr_map & m_cache; buffer m_locals; type_context::transparency_scope m_scope; - abstract_hash_fn(type_context & ctx): + abstract_fn(type_context & ctx, expr_map & cache): m_ctx(ctx), - m_cache(get_abstract_cache_for(ctx).m_hash_cache), + m_cache(cache), m_scope(m_ctx, transparency_mode::All) {} expr instantiate_locals(expr const & e) { @@ -71,6 +71,12 @@ struct abstract_hash_fn { void pop() { m_locals.pop_back(); } +}; + +struct abstract_hash_fn : public abstract_fn { + abstract_hash_fn(type_context & ctx): + abstract_fn(ctx, get_abstract_cache_for(ctx).m_hash_cache) { + } unsigned hash(expr const & e) { EASY_HASH(e); @@ -133,4 +139,85 @@ unsigned abstract_hash(type_context & ctx, expr const & e) { EASY_HASH(e); return abstract_hash_fn(ctx)(e); } + +#define EASY_WEIGHT(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 1; \ + default: \ + break; \ + } \ +} + +/* TODO(Leo): this class is too similar to abstract_hash_fn, both are folding expr. + We should try to merge both implementations. */ +struct abstract_weight_fn : public abstract_fn { + abstract_weight_fn(type_context & ctx): + abstract_fn(ctx, get_abstract_cache_for(ctx).m_weight_cache) {} + + unsigned weight(expr const & e) { + EASY_WEIGHT(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 = weight(binding_domain(e)); + push_local(binding_name(e), binding_domain(e)); + r += weight(binding_body(e)); + pop(); + break; + case expr_kind::Let: + r = weight(let_type(e)); + r += weight(let_value(e)); + push_let(let_name(e), let_type(e), let_value(e)); + r += weight(let_body(e)); + pop(); + break; + case expr_kind::Macro: + r = 0; + for (unsigned i = 0; i < macro_num_args(e); i++) + r += weight(macro_arg(e, i)); + break; + case expr_kind::App: + buffer args; + expr const & f = get_app_args(e, args); + r = weight(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 += weight(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 weight(e); + } +}; + +unsigned abstract_weight(type_context & ctx, expr const & e) { + EASY_WEIGHT(e); + return abstract_weight_fn(ctx)(e); +} } diff --git a/src/library/tactic/abstract_expr_tactics.cpp b/src/library/tactic/abstract_expr_tactics.cpp index 099ff5abae..598088d824 100644 --- a/src/library/tactic/abstract_expr_tactics.cpp +++ b/src/library/tactic/abstract_expr_tactics.cpp @@ -16,8 +16,15 @@ vm_obj tactic_abstract_hash(vm_obj const & e, vm_obj const & s) { return mk_tactic_success(mk_vm_simple(h), to_tactic_state(s)); } +vm_obj tactic_abstract_weight(vm_obj const & e, vm_obj const & s) { + type_context_scope ctx(s); + unsigned h = abstract_weight(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); + DECLARE_VM_BUILTIN(name({"tactic", "abstract_weight"}), tactic_abstract_weight); } void finalize_abstract_expr_tactics() { } diff --git a/tests/lean/run/ahash1.lean b/tests/lean/run/ahash1.lean index c543e9e2f2..db9e0e97f0 100644 --- a/tests/lean/run/ahash1.lean +++ b/tests/lean/run/ahash1.lean @@ -16,3 +16,12 @@ by do if h₁ ≠ h₂ then fail "ERROR" else skip, if h₁ = h₃ then fail "UNEXPECTED" else skip, constructor + +example (a b : nat) + (H1 : ∀ d c : nat, @add nat nat_has_add1 a b = c + d) + (H2 : ∀ d c : nat, @add nat nat_has_add2 a b = c + d) + : true := +by do + get_local "H1" >>= infer_type >>= abstract_hash >>= trace, + get_local "H2" >>= infer_type >>= abstract_hash >>= trace, + constructor diff --git a/tests/lean/run/aweight1.lean b/tests/lean/run/aweight1.lean new file mode 100644 index 0000000000..d30048ae2c --- /dev/null +++ b/tests/lean/run/aweight1.lean @@ -0,0 +1,30 @@ +import data.nat +open tactic nat decidable + +constant nat_has_add1 : has_add nat +constant nat_has_add2 : nat → has_add nat + +constant foo (a : nat) : a > 0 → Prop + +set_option pp.all true + +example (a b : nat) + (H1 : @add nat nat_has_add1 a b = 0) + (H2 : @add nat (nat_has_add2 (0 + a + b)) a b = 0) + (H3 : @add nat nat_has_add1 b (a + b) = 0) + (H4 : foo (succ (succ (succ zero))) dec_trivial) + (H5 : foo (succ (succ (succ zero))) sorry) + : true := +by do + h₁ ← get_local "H1" >>= infer_type >>= abstract_weight, + h₂ ← get_local "H2" >>= infer_type >>= abstract_weight, + h₃ ← get_local "H3" >>= infer_type >>= abstract_weight, + h₄ ← get_local "H4" >>= infer_type >>= abstract_weight, + h₅ ← get_local "H5" >>= infer_type >>= abstract_weight, + trace $ to_string h₁ + " " + to_string h₂ + " " + to_string h₃, + trace $ to_string h₄ + " " + to_string h₅, + get_local "H4" >>= infer_type >>= trace, + get_local "H5" >>= infer_type >>= trace, + if h₁ ≠ h₂ then fail "ERROR" else skip, + if h₁ = h₃ then fail "ERROR" else skip, + constructor