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

refactor(library/init/meta/smt): move ematch stuff to new file, and remove priority from hinst_lemma

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-04 17:09:50 -08:00
parent 9435762643
commit 384e8bc795
8 changed files with 71 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/interactive.lean
View file

@ -5,7 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
import init.meta.smt.congruence_tactics
import init.meta.smt.congruence_closure
namespace interactive
namespace types

36
library/init/meta/smt/congruence_tactics.lean → library/init/meta/smt/congruence_closure.lean
View file

@ -122,39 +122,3 @@ do (lhs, rhs) ← target >>= match_eq,
} else do {
fail "ac_refl failed"
}
/- Heuristic instantiation lemma -/
meta constant hinst_lemma : Type
/- (mk_core m e as_simp prio) -/
meta constant hinst_lemma.mk_core : transparency → expr → bool → nat → tactic hinst_lemma
meta constant hinst_lemma.mk_from_decl_core : transparency → name → bool → nat → tactic hinst_lemma
meta constant hinst_lemma.pp : hinst_lemma → tactic format
meta def hinst_lemma.mk (h : expr) : tactic hinst_lemma :=
hinst_lemma.mk_core semireducible h ff 0
meta def hinst_lemma.mk_from_decl (h : name) : tactic hinst_lemma :=
hinst_lemma.mk_from_decl_core semireducible h ff 0
structure ematch_config :=
(max_instances : nat)
def default_ematch_config : ematch_config :=
{max_instances := 10000}
/- Ematching -/
meta constant ematch_state : Type
meta constant ematch_state.mk : ematch_config → ematch_state
meta constant ematch_state.internalize : ematch_state → expr → tactic ematch_state
namespace tactic
meta constant ematch_core : transparency → cc_state → ematch_state → hinst_lemma → expr → tactic (list (expr × expr) × cc_state × ematch_state)
meta constant ematch_all_core : transparency → cc_state → ematch_state → hinst_lemma → bool → tactic (list (expr × expr) × cc_state × ematch_state)
meta def ematch : cc_state → ematch_state → hinst_lemma → expr → tactic (list (expr × expr) × cc_state × ematch_state) :=
ematch_core reducible
meta def ematch_all : cc_state → ematch_state → hinst_lemma → bool → tactic (list (expr × expr) × cc_state × ematch_state) :=
ematch_all_core reducible
end tactic

5
library/init/meta/smt/default.lean
View file

@ -4,5 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.smt.congruence_tactics init.meta.smt.smt_tactic
import init.meta.smt.interactive init.cc_lemmas
import init.meta.smt.congruence_closure init.cc_lemmas
import init.meta.smt.ematch
import init.meta.smt.smt_tactic init.meta.smt.interactive

44
library/init/meta/smt/ematch.lean Normal file
View file

@ -0,0 +1,44 @@
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.smt.congruence_closure
open tactic
/- Heuristic instantiation lemma -/
meta constant hinst_lemma : Type
/- (mk_core m e as_simp prio) -/
meta constant hinst_lemma.mk_core : transparency → expr → bool → tactic hinst_lemma
meta constant hinst_lemma.mk_from_decl_core : transparency → name → bool → tactic hinst_lemma
meta constant hinst_lemma.pp : hinst_lemma → tactic format
meta def hinst_lemma.mk (h : expr) : tactic hinst_lemma :=
hinst_lemma.mk_core semireducible h ff
meta def hinst_lemma.mk_from_decl (h : name) : tactic hinst_lemma :=
hinst_lemma.mk_from_decl_core semireducible h ff
structure ematch_config :=
(max_instances : nat)
def default_ematch_config : ematch_config :=
{max_instances := 10000}
/- Ematching -/
meta constant ematch_state : Type
meta constant ematch_state.mk : ematch_config → ematch_state
meta constant ematch_state.internalize : ematch_state → expr → tactic ematch_state
namespace tactic
meta constant ematch_core : transparency → cc_state → ematch_state → hinst_lemma → expr → tactic (list (expr × expr) × cc_state × ematch_state)
meta constant ematch_all_core : transparency → cc_state → ematch_state → hinst_lemma → bool → tactic (list (expr × expr) × cc_state × ematch_state)
meta def ematch : cc_state → ematch_state → hinst_lemma → expr → tactic (list (expr × expr) × cc_state × ematch_state) :=
ematch_core reducible
meta def ematch_all : cc_state → ematch_state → hinst_lemma → bool → tactic (list (expr × expr) × cc_state × ematch_state) :=
ematch_all_core reducible
end tactic

4
library/init/meta/smt/smt_tactic.lean
View file

@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.simp_tactic init.meta.smt.congruence_tactics
import init.meta.simp_tactic
import init.meta.smt.congruence_closure
import init.meta.smt.ematch
universe variables u

16
src/library/tactic/smt/congruence_tactics.cpp
View file

@ -234,18 +234,18 @@ vm_obj to_obj(hinst_lemma const & s) {
return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_hinst_lemma))) vm_hinst_lemma(s));
}
vm_obj hinst_lemma_mk_core(vm_obj const & m, vm_obj const & lemma, vm_obj const & simp, vm_obj const & prio, vm_obj const & s) {
vm_obj hinst_lemma_mk_core(vm_obj const & m, vm_obj const & lemma, vm_obj const & simp, vm_obj const & s) {
LEAN_TACTIC_TRY;
type_context ctx = mk_type_context_for(s, m);
hinst_lemma h = mk_hinst_lemma(ctx, to_expr(lemma), to_bool(simp), force_to_unsigned(prio, 0));
hinst_lemma h = mk_hinst_lemma(ctx, to_expr(lemma), to_bool(simp));
return mk_tactic_success(to_obj(h), to_tactic_state(s));
LEAN_TACTIC_CATCH(to_tactic_state(s));
}
vm_obj hinst_lemma_mk_from_decl_core(vm_obj const & m, vm_obj const & lemma_name, vm_obj const & simp, vm_obj const & prio, vm_obj const & s) {
vm_obj hinst_lemma_mk_from_decl_core(vm_obj const & m, vm_obj const & lemma_name, vm_obj const & simp, vm_obj const & s) {
LEAN_TACTIC_TRY;
type_context ctx = mk_type_context_for(s, m);
hinst_lemma h = mk_hinst_lemma(ctx, to_name(lemma_name), to_bool(simp), force_to_unsigned(prio, 0));
hinst_lemma h = mk_hinst_lemma(ctx, to_name(lemma_name), to_bool(simp));
return mk_tactic_success(to_obj(h), to_tactic_state(s));
LEAN_TACTIC_CATCH(to_tactic_state(s));
}
@ -282,20 +282,20 @@ vm_obj hinst_lemmas_mk() {
return to_obj(hinst_lemmas());
}
vm_obj hinst_lemmas_add_core(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & simp, vm_obj const & prio, vm_obj const & s) {
vm_obj hinst_lemmas_add_core(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & simp, vm_obj const & s) {
LEAN_TACTIC_TRY;
type_context ctx = mk_type_context_for(s, m);
hinst_lemma h = mk_hinst_lemma(ctx, to_expr(lemma), to_bool(simp), force_to_unsigned(prio, 0));
hinst_lemma h = mk_hinst_lemma(ctx, to_expr(lemma), to_bool(simp));
hinst_lemmas new_lemmas = to_hinst_lemmas(lemmas);
new_lemmas.insert(h);
return mk_tactic_success(to_obj(new_lemmas), to_tactic_state(s));
LEAN_TACTIC_CATCH(to_tactic_state(s));
}
vm_obj hinst_lemmas_add_decl_core(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & simp, vm_obj const & prio, vm_obj const & s) {
vm_obj hinst_lemmas_add_decl_core(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & simp, vm_obj const & s) {
LEAN_TACTIC_TRY;
type_context ctx = mk_type_context_for(s, m);
hinst_lemma h = mk_hinst_lemma(ctx, to_name(lemma_name), to_bool(simp), force_to_unsigned(prio, 0));
hinst_lemma h = mk_hinst_lemma(ctx, to_name(lemma_name), to_bool(simp));
hinst_lemmas new_lemmas = to_hinst_lemmas(lemmas);
new_lemmas.insert(h);
return mk_tactic_success(to_obj(new_lemmas), to_tactic_state(s));

20
src/library/tactic/smt/hinst_lemmas.cpp
View file

@ -244,7 +244,6 @@ struct mk_hinst_lemma_fn {
name_set m_no_inst_patterns;
expr m_H;
unsigned m_num_uvars;
unsigned m_priority;
unsigned m_max_steps;
/* If m_simp is true, the pattern inference procedure assumes the given lemma is a [simp] lemma.
That is, the conclusion is of the form (t ~ s), and it will try to use t as a pattern. */
@ -256,9 +255,9 @@ struct mk_hinst_lemma_fn {
unsigned m_num_steps;
mk_hinst_lemma_fn(type_context & ctx, expr const & H,
unsigned num_uvars, unsigned prio, unsigned max_steps, bool simp):
unsigned num_uvars, unsigned max_steps, bool simp):
m_ctx(ctx), m_no_inst_patterns(get_no_inst_patterns(ctx.env())),
m_H(H), m_num_uvars(num_uvars), m_priority(prio), m_max_steps(max_steps),
m_H(H), m_num_uvars(num_uvars), m_max_steps(max_steps),
m_simp(simp) {}
struct candidate {
@ -574,7 +573,6 @@ struct mk_hinst_lemma_fn {
hinst_lemma r;
r.m_num_uvars = m_num_uvars;
r.m_num_mvars = m_mvars.size();
r.m_priority = m_priority;
r.m_multi_patterns = mps;
r.m_mvars = to_list(m_mvars);
r.m_is_inst_implicit = to_list(inst_implicit_flags);
@ -586,16 +584,16 @@ struct mk_hinst_lemma_fn {
};
hinst_lemma mk_hinst_lemma_core(type_context & ctx, expr const & H, unsigned num_uvars,
unsigned priority, unsigned max_steps, bool simp) {
unsigned max_steps, bool simp) {
try {
type_context::tmp_mode_scope tscope(ctx, num_uvars, 0);
bool erase_hints = false;
return mk_hinst_lemma_fn(ctx, H, num_uvars, priority, max_steps, simp)(erase_hints);
return mk_hinst_lemma_fn(ctx, H, num_uvars, max_steps, simp)(erase_hints);
} catch (mk_hinst_lemma_fn::try_again_without_hints &) {
type_context::tmp_mode_scope tscope(ctx, num_uvars, 0);
try {
bool erase_hints = true;
return mk_hinst_lemma_fn(ctx, H, num_uvars, priority, max_steps, simp)(erase_hints);
return mk_hinst_lemma_fn(ctx, H, num_uvars, max_steps, simp)(erase_hints);
} catch (mk_hinst_lemma_fn::try_again_without_hints &) {
lean_unreachable();
}
@ -608,15 +606,15 @@ unsigned get_hinst_lemma_max_steps(options const & o) {
return o.get_unsigned(*g_hinst_lemma_max_steps, LEAN_DEFAULT_HINST_LEMMA_PATTERN_MAX_STEPS);
}
hinst_lemma mk_hinst_lemma(type_context & ctx, expr const & H, bool simp, unsigned prio) {
hinst_lemma mk_hinst_lemma(type_context & ctx, expr const & H, bool simp) {
unsigned max_steps = get_hinst_lemma_max_steps(ctx.get_options());
hinst_lemma r = mk_hinst_lemma_core(ctx, H, 0, prio, max_steps, simp);
hinst_lemma r = mk_hinst_lemma_core(ctx, H, 0, max_steps, simp);
if (is_local(H))
r.m_id = local_pp_name(H);
return r;
}
hinst_lemma mk_hinst_lemma(type_context & ctx, name const & c, bool simp, unsigned priority) {
hinst_lemma mk_hinst_lemma(type_context & ctx, name const & c, bool simp) {
unsigned max_steps = get_hinst_lemma_max_steps(ctx.get_options());
declaration const & d = ctx.env().get(c);
buffer<level> us;
@ -624,7 +622,7 @@ hinst_lemma mk_hinst_lemma(type_context & ctx, name const & c, bool simp, unsign
for (unsigned i = 0; i < num_us; i++)
us.push_back(mk_idx_metauniv(i));
expr H = mk_constant(c, to_list(us));
hinst_lemma r = mk_hinst_lemma_core(ctx, H, num_us, priority, max_steps, simp);
hinst_lemma r = mk_hinst_lemma_core(ctx, H, num_us, max_steps, simp);
r.m_id = c;
return r;
}

14
src/library/tactic/smt/hinst_lemmas.h
View file

@ -35,7 +35,6 @@ struct hinst_lemma {
name m_id;
unsigned m_num_uvars;
unsigned m_num_mvars;
unsigned m_priority;
list<multi_pattern> m_multi_patterns;
list<bool> m_is_inst_implicit;
list<expr> m_mvars;
@ -45,16 +44,9 @@ struct hinst_lemma {
expr m_expr;
};
struct hinst_lemma_prio_fn { unsigned operator()(hinst_lemma const & s) const { return s.m_priority; } };
inline bool operator==(hinst_lemma const & l1, hinst_lemma const & l2) { return l1.m_prop == l2.m_prop; }
inline bool operator!=(hinst_lemma const & l1, hinst_lemma const & l2) { return l1.m_prop != l2.m_prop; }
struct hinst_lemma_cmp {
int operator()(hinst_lemma const & l1, hinst_lemma const & l2) const {
if (l1.m_priority != l2.m_priority)
return unsigned_cmp()(l1.m_priority, l2.m_priority);
else
return expr_quick_cmp()(l1.m_prop, l2.m_prop);
return expr_quick_cmp()(l1.m_prop, l2.m_prop);
}
};
typedef rb_tree<hinst_lemma, hinst_lemma_cmp> hinst_lemmas;
@ -64,8 +56,8 @@ list<multi_pattern> mk_multipatterns(environment const & env, io_state const & i
/** \brief Create a (local) heuristic instantiation lemma for \c H.
The maximum number of steps is extracted from the blast config object. */
hinst_lemma mk_hinst_lemma(type_context & ctx, expr const & H, bool simp = false, unsigned prio = LEAN_DEFAULT_PRIORITY);
hinst_lemma mk_hinst_lemma(type_context & ctx, name const & n, bool simp = false, unsigned prio = LEAN_DEFAULT_PRIORITY);
hinst_lemma mk_hinst_lemma(type_context & ctx, expr const & H, bool simp = false);
hinst_lemma mk_hinst_lemma(type_context & ctx, name const & n, bool simp = false);
format pp_hinst_lemma(formatter const & fmt, hinst_lemma const & h);