diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 167e67adba..426b7aa437 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -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 diff --git a/library/init/meta/smt/congruence_tactics.lean b/library/init/meta/smt/congruence_closure.lean similarity index 73% rename from library/init/meta/smt/congruence_tactics.lean rename to library/init/meta/smt/congruence_closure.lean index 7603de95b3..92cce53419 100644 --- a/library/init/meta/smt/congruence_tactics.lean +++ b/library/init/meta/smt/congruence_closure.lean @@ -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 diff --git a/library/init/meta/smt/default.lean b/library/init/meta/smt/default.lean index 9247eb6434..8fd097dad7 100644 --- a/library/init/meta/smt/default.lean +++ b/library/init/meta/smt/default.lean @@ -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 diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean new file mode 100644 index 0000000000..329cf10f88 --- /dev/null +++ b/library/init/meta/smt/ematch.lean @@ -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 diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean index 889f90df02..69483eb315 100644 --- a/library/init/meta/smt/smt_tactic.lean +++ b/library/init/meta/smt/smt_tactic.lean @@ -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 diff --git a/src/library/tactic/smt/congruence_tactics.cpp b/src/library/tactic/smt/congruence_tactics.cpp index 69513fd1ee..7a8093f0f4 100644 --- a/src/library/tactic/smt/congruence_tactics.cpp +++ b/src/library/tactic/smt/congruence_tactics.cpp @@ -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)); diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp index b2c8fb5fb6..9673eae9b2 100644 --- a/src/library/tactic/smt/hinst_lemmas.cpp +++ b/src/library/tactic/smt/hinst_lemmas.cpp @@ -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 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; } diff --git a/src/library/tactic/smt/hinst_lemmas.h b/src/library/tactic/smt/hinst_lemmas.h index 4431a1d068..3bc3f0efb6 100644 --- a/src/library/tactic/smt/hinst_lemmas.h +++ b/src/library/tactic/smt/hinst_lemmas.h @@ -35,7 +35,6 @@ struct hinst_lemma { name m_id; unsigned m_num_uvars; unsigned m_num_mvars; - unsigned m_priority; list m_multi_patterns; list m_is_inst_implicit; list 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_lemmas; @@ -64,8 +56,8 @@ list 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);