max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/abstract_expr): add abstract_weight

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-23 14:50:23 -07:00
parent facdf99e86
commit 3974a72a73
5 changed files with 139 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/meta/tactic.lean
View file

@ -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 -/

93
src/library/abstract_expr.cpp
View file

@ -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<unsigned> & m_cache;
buffer<expr> m_locals;
type_context::transparency_scope m_scope;
abstract_hash_fn(type_context & ctx):
abstract_fn(type_context & ctx, expr_map<unsigned> & 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<expr> 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);
}
}

7
src/library/tactic/abstract_expr_tactics.cpp
View file

@ -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() {
}

9
tests/lean/run/ahash1.lean
View file

@ -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

30
tests/lean/run/aweight1.lean Normal file
View file

@ -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