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

feat(library/init/meta/congruence_tactics): add cc_state.gmt and cc_state.inc_gmt

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-27 10:49:20 -08:00
parent daf839e0d5
commit 773389f9df
3 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -15,6 +15,8 @@ meta constant cc_state.next : cc_state → expr → 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.gmt : cc_state → nat
meta constant cc_state.inc_gmt : cc_state → cc_state
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_core : cc_state → bool → tactic format

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

@ -144,6 +144,7 @@ public:
format pp_parent_occs(formatter const & fmt, expr const & e) const;
format pp_parent_occs(formatter const & fmt) const;
unsigned get_gmt() const { return m_gmt; }
void inc_gmt() { m_gmt++; }
};
private:

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

@ -109,6 +109,16 @@ 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)));
}
vm_obj cc_state_gmt(vm_obj const & ccs) {
return mk_vm_nat(to_cc_state(ccs).get_gmt());
}
vm_obj cc_state_inc_gmt(vm_obj const & ccs) {
congruence_closure::state s = to_cc_state(ccs);
s.inc_gmt();
return to_obj(s);
}
#define cc_state_proc(CODE) \
tactic_state const & s = to_tactic_state(_s); \
try { \
@ -333,6 +343,8 @@ void initialize_congruence_tactics() {
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", "gmt"}), cc_state_gmt);
DECLARE_VM_BUILTIN(name({"cc_state", "inc_gmt"}), cc_state_inc_gmt);
DECLARE_VM_BUILTIN(name({"cc_state", "is_cg_root"}), cc_state_is_cg_root);
DECLARE_VM_BUILTIN(name({"cc_state", "roots_core"}), cc_state_roots_core);
DECLARE_VM_BUILTIN(name({"cc_state", "internalize"}), cc_state_internalize);