From 4cdfc9ee84edb8b9cee7394eb6640900d3024172 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 May 2015 07:50:56 -0700 Subject: [PATCH] feat(frontends/lean/pp): add pretty printing functions for debugging purposes --- src/frontends/lean/pp.cpp | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 2663908101..8bda9e508e 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -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); }