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

feat(library/tactic/congruence/congruence_tactics): add missing functions

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-22 17:42:53 -08:00
parent 66c781cce6
commit eefd4cd6ab
6 changed files with 135 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

27
src/library/tactic/congruence/congruence_closure.cpp
View file

@ -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<expr> & 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<congruence_closure *> 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<expr> 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) {

1
src/library/tactic/congruence/congruence_closure.h
View file

@ -109,6 +109,7 @@ public:
friend class congruence_closure;
bool check_eqc(expr const & e) const;
public:
void get_roots(buffer<expr> & roots) const;
expr get_root(expr const & e) const;
expr get_next(expr const & e) const;
unsigned get_mt(expr const & e) const;

103
src/library/tactic/congruence/congruence_tactics.cpp
View file

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

6
src/library/tactic/tactic_state.cpp
View file

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

2
src/library/tactic/tactic_state.h
View file

@ -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); \