michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/pp): add pretty printing functions for debugging purposes

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-06 07:50:56 -07:00
parent 7d52fc0b51
commit 4cdfc9ee84
1 changed files with 31 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/frontends/lean/pp.cpp
View file

@ -1223,4 +1223,35 @@ formatter_factory mk_pretty_formatter_factory() {
});
};
}
static options mk_options(bool detail) {
options opts;
if (detail) {
opts = opts.update(name{"pp", "implicit"}, true);
opts = opts.update(name{"pp", "notation"}, false);
}
return opts;
}
static void pp_core(environment const & env, expr const & e, bool detail) {
io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
regular(env, ios) << e << "\n";
}
static void pp_core(environment const & env, goal const & g, bool detail) {
io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
regular(env, ios) << g << "\n";
}
static void pp_core(environment const & env, proof_state const & s, bool detail) {
io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
regular(env, ios) << s.pp(env, ios) << "\n";
}
}
// for debugging purposes
void pp(lean::environment const & env, lean::expr const & e) { lean::pp_core(env, e, false); }
void pp(lean::environment const & env, lean::goal const & g) { lean::pp_core(env, g, false); }
void pp(lean::environment const & env, lean::proof_state const & s) { lean::pp_core(env, s, false); }
void pp_detail(lean::environment const & env, lean::expr const & e) { lean::pp_core(env, e, true); }
void pp_detail(lean::environment const & env, lean::goal const & g) { lean::pp_core(env, g, true); }
void pp_detail(lean::environment const & env, lean::proof_state const & s) { lean::pp_core(env, s, true); }