diff --git a/library/init/meta/congruence_tactics.lean b/library/init/meta/congruence_tactics.lean index 624ab49ac7..7255fe6896 100644 --- a/library/init/meta/congruence_tactics.lean +++ b/library/init/meta/congruence_tactics.lean @@ -13,12 +13,14 @@ 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.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.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_uneqv : 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 diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp index fe3a9e11c0..e5480fa603 100644 --- a/src/library/tactic/congruence/congruence_closure.cpp +++ b/src/library/tactic/congruence/congruence_closure.cpp @@ -22,6 +22,7 @@ struct congr_lemma_key { expr m_fn; unsigned m_nargs; unsigned m_hash; + congr_lemma_key():m_nargs(0), m_hash(0) {} congr_lemma_key(expr const & fn, unsigned nargs): m_fn(fn), m_nargs(nargs), m_hash(hash(fn.hash(), nargs)) {} @@ -155,6 +156,13 @@ expr congruence_closure::state::get_root(expr const & e) const { } } +void congruence_closure::state::get_roots(buffer & roots) const { + m_entries.for_each([&](expr const & k, entry const & n) { + if (k == n.m_root) + roots.push_back(k); + }); +} + expr congruence_closure::state::get_next(expr const & e) const { if (auto n = m_entries.find(e)) { return n->m_next; @@ -1210,6 +1218,20 @@ bool congruence_closure::proved(expr const & e) const { return is_eqv(e, mk_true()); } +void congruence_closure::internalize(expr const & e, bool toplevel) { + flet set_cc(g_cc, this); + bool to_propagate = false; // We don't need to mark units for propagation + internalize_core(e, toplevel, to_propagate); + process_todo(none_expr()); +} + +void congruence_closure::internalize(expr const & e) { + if (m_ctx.is_prop(e)) + internalize(e, true); + else + internalize(e, false); +} + bool congruence_closure::state::check_eqc(expr const & e) const { expr root = get_root(e); unsigned size = 0; @@ -1258,10 +1280,7 @@ format congruence_closure::state::pp_eqc(formatter const & fmt, expr const & e) format congruence_closure::state::pp_eqcs(formatter const & fmt) const { buffer roots; - m_entries.for_each([&](expr const & k, entry const & n) { - if (k == n.m_root) - roots.push_back(k); - }); + get_roots(roots); 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 6442b1fd9e..397732354b 100644 --- a/src/library/tactic/congruence/congruence_closure.h +++ b/src/library/tactic/congruence/congruence_closure.h @@ -109,6 +109,7 @@ public: friend class congruence_closure; bool check_eqc(expr const & e) const; public: + void get_roots(buffer & roots) const; expr get_root(expr const & e) const; expr get_next(expr const & e) const; unsigned get_mt(expr const & e) const; diff --git a/src/library/tactic/congruence/congruence_tactics.cpp b/src/library/tactic/congruence/congruence_tactics.cpp index d0652effbb..a11a22ac40 100644 --- a/src/library/tactic/congruence/congruence_tactics.cpp +++ b/src/library/tactic/congruence/congruence_tactics.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "library/vm/vm.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_format.h" +#include "library/vm/vm_list.h" #include "library/tactic/tactic_state.h" #include "library/tactic/congruence/congruence_closure.h" @@ -61,17 +62,113 @@ vm_obj cc_state_mk_using_hs(vm_obj const & _s) { vm_obj cc_state_pp(vm_obj const & ccs, 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); + formatter fmt = mk_formatter_for(s); format r = to_cc_state(ccs).pp_eqcs(fmt); return mk_tactic_success(to_obj(r), s); } +vm_obj cc_state_pp_eqc(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) { + tactic_state const & s = to_tactic_state(_s); + formatter fmt = mk_formatter_for(s); + format r = to_cc_state(ccs).pp_eqc(fmt, to_expr(e)); + return mk_tactic_success(to_obj(r), s); +} + +vm_obj cc_state_next(vm_obj const & ccs, vm_obj const & e) { + return to_obj(to_cc_state(ccs).get_next(to_expr(e))); +} + +vm_obj cc_state_root(vm_obj const & ccs, vm_obj const & e) { + return to_obj(to_cc_state(ccs).get_root(to_expr(e))); +} + +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) { + buffer roots; + to_cc_state(ccs).get_roots(roots); + return to_obj(roots); +} + +vm_obj cc_state_inconsistent(vm_obj const & ccs) { + return mk_vm_bool(to_cc_state(ccs).inconsistent()); +} + +vm_obj cc_state_mt(vm_obj const & ccs, vm_obj const & e) { + return mk_vm_nat(to_cc_state(ccs).get_mt(to_expr(e))); +} + +#define cc_state_proc(CODE) \ + tactic_state const & s = to_tactic_state(_s); \ + try { \ + type_context ctx = mk_type_context_for(s); \ + congruence_closure::state S = to_cc_state(ccs); \ + congruence_closure cc(ctx, S); \ + CODE \ + } catch (exception & ex) { \ + return mk_tactic_exception(ex, s); \ + } + +#define cc_state_updt_proc(CODE) cc_state_proc({ CODE; return mk_tactic_success(to_obj(S), s); }) + + +vm_obj cc_state_add(vm_obj const & ccs, vm_obj const & H, vm_obj const & _s) { + cc_state_updt_proc({ + expr type = ctx.infer(to_expr(H)); + 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) { + cc_state_updt_proc({ + cc.internalize(to_expr(e), to_bool(top_level)); + }); +} + +vm_obj cc_state_is_eqv(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) { + cc_state_proc({ + bool r = cc.is_eqv(to_expr(e1), to_expr(e2)); + return mk_tactic_success(mk_vm_bool(r), s); + }); +} + +vm_obj cc_state_is_not_eqv(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) { + cc_state_proc({ + bool r = cc.is_not_eqv(to_expr(e1), to_expr(e2)); + return mk_tactic_success(mk_vm_bool(r), s); + }); +} + +vm_obj cc_state_eqv_proof(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) { + cc_state_proc({ + if (optional r = cc.get_proof(to_expr(e1), to_expr(e2))) { + return mk_tactic_success(to_obj(*r), s); + } else { + return mk_tactic_exception("cc_state.eqv_proof failed to build proof", s); + } + }); +} + 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_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", "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); + DECLARE_VM_BUILTIN(name({"cc_state", "is_not_eqv"}), cc_state_is_not_eqv); + DECLARE_VM_BUILTIN(name({"cc_state", "eqv_proof"}), cc_state_eqv_proof); } void finalize_congruence_tactics() { diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 23ad9ea2c7..3d0f194bb5 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -360,6 +360,12 @@ type_context mk_type_context_for(vm_obj const & s, vm_obj const & m) { return mk_type_context_for(to_tactic_state(s), to_transparency_mode(m)); } +formatter mk_formatter_for(tactic_state const & s) { + type_context ctx = mk_type_context_for(s); + formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); + return fmtf(s.env(), s.get_options(), ctx); +} + vm_obj tactic_infer_type(vm_obj const & e, vm_obj const & s0) { tactic_state const & s = to_tactic_state(s0); type_context ctx = mk_type_context_for(s); diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 665d990d72..4f4c1f0ddb 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -136,6 +136,8 @@ type_context mk_type_context_for(environment const & env, options const & o, type_context mk_type_context_for(vm_obj const & s); type_context mk_type_context_for(vm_obj const & s, vm_obj const & m); +formatter mk_formatter_for(tactic_state const & s); + #define lean_tactic_trace(N, S, Code) lean_trace(N, { \ type_context _ctx = mk_type_context_for(S); \ scope_trace_env _scope((S).env(), _ctx); \