From ca261b7fa8f1e1dd8c35ba5bbc7b1aaef1e5da43 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Dec 2016 18:35:44 -0800 Subject: [PATCH] feat(library/init/meta/congruence_tactics): add option for retrieving only non-singleton equivalence classes, add auxiliary functions --- library/init/meta/congruence_tactics.lean | 28 +++++++++++++++++-- .../tactic/congruence/congruence_closure.cpp | 14 +++++++--- .../tactic/congruence/congruence_closure.h | 5 ++-- .../tactic/congruence/congruence_tactics.cpp | 14 +++++----- tests/lean/run/cc1.lean | 7 +++++ 5 files changed, 53 insertions(+), 15 deletions(-) diff --git a/library/init/meta/congruence_tactics.lean b/library/init/meta/congruence_tactics.lean index 7255fe6896..4bbbc3a2d7 100644 --- a/library/init/meta/congruence_tactics.lean +++ b/library/init/meta/congruence_tactics.lean @@ -13,14 +13,38 @@ meta constant cc_state.mk : cc_state meta constant cc_state.mk_using_hs : tactic cc_state meta constant cc_state.next : cc_state → expr → expr meta constant cc_state.inconsistent : cc_state → bool -meta constant cc_state.roots : cc_state → list expr +meta constant cc_state.roots_core : cc_state → bool → list expr meta constant cc_state.root : cc_state → expr → expr meta constant cc_state.mt : cc_state → expr → nat meta constant cc_state.is_cg_root : cc_state → expr → bool meta constant cc_state.pp_eqc : cc_state → expr → tactic format -meta constant cc_state.pp : cc_state → tactic format +meta constant cc_state.pp_core : cc_state → bool → tactic format meta constant cc_state.internalize : cc_state → expr → bool → tactic cc_state meta constant cc_state.add : cc_state → expr → tactic cc_state meta constant cc_state.is_eqv : cc_state → expr → expr → tactic bool meta constant cc_state.is_not_eqv : cc_state → expr → expr → tactic bool meta constant cc_state.eqv_proof : cc_state → expr → expr → tactic expr + +namespace cc_state + +meta def roots (s : cc_state) : list expr := +cc_state.roots_core s tt + +meta def pp (s : cc_state) : tactic format := +cc_state.pp_core s tt + +meta def eqc_of_core (s : cc_state) : expr → expr → list expr → list expr +| e f r := + let n := s^.next e in + if n = f then e::r else eqc_of_core n f (e::r) + +meta def eqc_of (s : cc_state) (e : expr) : list expr := +s^.eqc_of_core e e [] + +meta def in_singlenton_eqc (s : cc_state) (e : expr) : bool := +to_bool (s^.next e = e) + +meta def eqc_size (s : cc_state) (e : expr) : nat := +(s^.eqc_of e)^.length + +end cc_state diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp index b06faaf5f5..291b08edc9 100644 --- a/src/library/tactic/congruence/congruence_closure.cpp +++ b/src/library/tactic/congruence/congruence_closure.cpp @@ -162,9 +162,9 @@ expr congruence_closure::state::get_root(expr const & e) const { } } -void congruence_closure::state::get_roots(buffer & roots) const { +void congruence_closure::state::get_roots(buffer & roots, bool nonsingleton_only) const { m_entries.for_each([&](expr const & k, entry const & n) { - if (k == n.m_root) + if (k == n.m_root && (!nonsingleton_only || !in_singleton_eqc(k))) roots.push_back(k); }); } @@ -1394,9 +1394,15 @@ format congruence_closure::state::pp_eqc(formatter const & fmt, expr const & e) return bracket("{", group(r), "}"); } -format congruence_closure::state::pp_eqcs(formatter const & fmt) const { +bool congruence_closure::state::in_singleton_eqc(expr const & e) const { + if (auto it = m_entries.find(e)) + return it->m_next == e; + return true; +} + +format congruence_closure::state::pp_eqcs(formatter const & fmt, bool nonsingleton_only) const { buffer roots; - get_roots(roots); + get_roots(roots, nonsingleton_only); format r; bool first = true; for (expr const & root : roots) { diff --git a/src/library/tactic/congruence/congruence_closure.h b/src/library/tactic/congruence/congruence_closure.h index febfb3f9ee..27fde3708a 100644 --- a/src/library/tactic/congruence/congruence_closure.h +++ b/src/library/tactic/congruence/congruence_closure.h @@ -130,15 +130,16 @@ public: void mk_entry_core(expr const & e, bool to_propagate, bool interpreted, bool constructor); public: state(name_set const & ho_fns = name_set(), config const & cfg = config()); - void get_roots(buffer & roots) const; + void get_roots(buffer & roots, bool nonsingleton_only = true) const; expr get_root(expr const & e) const; expr get_next(expr const & e) const; unsigned get_mt(expr const & e) const; bool is_congr_root(expr const & e) const; bool check_invariant() const; bool inconsistent() const { return m_inconsistent; } + bool in_singleton_eqc(expr const & e) const; format pp_eqc(formatter const & fmt, expr const & e) const; - format pp_eqcs(formatter const & fmt) const; + format pp_eqcs(formatter const & fmt, bool nonsingleton_only = true) const; }; private: diff --git a/src/library/tactic/congruence/congruence_tactics.cpp b/src/library/tactic/congruence/congruence_tactics.cpp index f5310ebd07..1ba2042ed3 100644 --- a/src/library/tactic/congruence/congruence_tactics.cpp +++ b/src/library/tactic/congruence/congruence_tactics.cpp @@ -60,12 +60,12 @@ vm_obj cc_state_mk_using_hs(vm_obj const & _s) { } } -vm_obj cc_state_pp(vm_obj const & ccs, vm_obj const & _s) { +vm_obj cc_state_pp_core(vm_obj const & ccs, vm_obj const & nonsingleton, vm_obj const & _s) { tactic_state const & s = to_tactic_state(_s); type_context ctx = mk_type_context_for(s); formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); formatter fmt = fmtf(s.env(), s.get_options(), ctx); - format r = to_cc_state(ccs).pp_eqcs(fmt); + format r = to_cc_state(ccs).pp_eqcs(fmt, to_bool(nonsingleton)); return mk_tactic_success(to_obj(r), s); } @@ -90,9 +90,9 @@ vm_obj cc_state_is_cg_root(vm_obj const & ccs, vm_obj const & e) { return mk_vm_bool(to_cc_state(ccs).is_congr_root(to_expr(e))); } -vm_obj cc_state_roots(vm_obj const & ccs) { +vm_obj cc_state_roots_core(vm_obj const & ccs, vm_obj const & nonsingleton) { buffer roots; - to_cc_state(ccs).get_roots(roots); + to_cc_state(ccs).get_roots(roots, to_bool(nonsingleton)); return to_obj(roots); } @@ -124,7 +124,7 @@ vm_obj cc_state_add(vm_obj const & ccs, vm_obj const & H, vm_obj const & _s) { if (ctx.is_prop(type)) return mk_tactic_exception("cc_state.add failed, given expression is not a proof term", s); cc.add(type, to_expr(H)); - }); + }); } vm_obj cc_state_internalize(vm_obj const & ccs, vm_obj const & e, vm_obj const & top_level, vm_obj const & _s) { @@ -161,13 +161,13 @@ void initialize_congruence_tactics() { DECLARE_VM_BUILTIN(name({"cc_state", "mk"}), cc_state_mk); DECLARE_VM_BUILTIN(name({"cc_state", "next"}), cc_state_next); DECLARE_VM_BUILTIN(name({"cc_state", "mk_using_hs"}), cc_state_mk_using_hs); - DECLARE_VM_BUILTIN(name({"cc_state", "pp"}), cc_state_pp); + DECLARE_VM_BUILTIN(name({"cc_state", "pp_core"}), cc_state_pp_core); DECLARE_VM_BUILTIN(name({"cc_state", "pp_eqc"}), cc_state_pp_eqc); DECLARE_VM_BUILTIN(name({"cc_state", "next"}), cc_state_next); DECLARE_VM_BUILTIN(name({"cc_state", "root"}), cc_state_root); DECLARE_VM_BUILTIN(name({"cc_state", "mt"}), cc_state_mt); DECLARE_VM_BUILTIN(name({"cc_state", "is_cg_root"}), cc_state_is_cg_root); - DECLARE_VM_BUILTIN(name({"cc_state", "roots"}), cc_state_roots); + DECLARE_VM_BUILTIN(name({"cc_state", "roots_core"}), cc_state_roots_core); DECLARE_VM_BUILTIN(name({"cc_state", "internalize"}), cc_state_internalize); DECLARE_VM_BUILTIN(name({"cc_state", "add"}), cc_state_add); DECLARE_VM_BUILTIN(name({"cc_state", "is_eqv"}), cc_state_is_eqv); diff --git a/tests/lean/run/cc1.lean b/tests/lean/run/cc1.lean index 3d60476355..b094672813 100644 --- a/tests/lean/run/cc1.lean +++ b/tests/lean/run/cc1.lean @@ -8,9 +8,16 @@ by do intros, s^.pp >>= trace, t₁ ← to_expr `(f (b + b) b), t₂ ← to_expr `(f (a + c) c), + b ← to_expr `(b), + d ← to_expr `(d), guard (s^.inconsistent), + guard (s^.eqc_size b = 3), + guard (not (s^.in_singlenton_eqc b)), + guard (s^.in_singlenton_eqc d), trace ">>> Equivalence roots", trace s^.roots, + trace ">>> b's equivalence class", + trace (s^.eqc_of b), pr ← s^.eqv_proof t₁ t₂, note `h pr, contradiction