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

chore(library/tactic/tactic_state): add helper methods

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-20 10:47:48 -07:00
parent 851bc30f3a
commit d03dc18096
2 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -114,6 +114,16 @@ format tactic_state::pp(formatter_factory const & fmtf) const {
return r;
}
format tactic_state::pp() const {
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
return pp(fmtf);
}
format tactic_state::pp_expr(expr const & e) const {
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
return pp_expr(fmtf, e);
}
struct vm_tactic_state : public vm_external {
tactic_state m_val;
vm_tactic_state(tactic_state const & v):m_val(v) {}
@ -146,13 +156,11 @@ vm_obj tactic_state_env(vm_obj const & s) {
}
vm_obj tactic_state_to_format(vm_obj const & s) {
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
return to_obj(to_tactic_state(s).pp(fmtf));
return to_obj(to_tactic_state(s).pp());
}
format pp_expr(tactic_state const & s, expr const & e) {
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
return s.pp_expr(fmtf, e);
return s.pp_expr(e);
}
format pp_indented_expr(tactic_state const & s, expr const & e) {

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

@ -60,6 +60,8 @@ public:
format pp(formatter_factory const & fmtf) const;
format pp_expr(formatter_factory const & fmtf, expr const & e) const;
format pp() const;
format pp_expr(expr const & e) const;
};
inline bool operator==(tactic_state const & s1, tactic_state const & s2) { return is_eqp(s1, s2); }