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

feat(frontends/lean/pp): do not display metavariable arguments by default, add option pp.metavar_args to control whether they are displayed or not

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-31 16:44:57 -07:00
parent de05c041c7
commit ba98634a7a
4 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -113,6 +113,7 @@ void pretty_fn::set_options_core(options const & o) {
m_universes = get_pp_universes(o); m_universes = get_pp_universes(o);
m_full_names = get_pp_full_names(o); m_full_names = get_pp_full_names(o);
m_private_names = get_pp_private_names(o); m_private_names = get_pp_private_names(o);
m_metavar_args = get_pp_metavar_args(o);
} }
void pretty_fn::set_options(options const & o) { void pretty_fn::set_options(options const & o) {
@ -412,6 +413,7 @@ auto pretty_fn::pp(expr const & e) -> result {
if (is_show(e)) return pp_show(e); if (is_show(e)) return pp_show(e);
if (is_let(e)) return pp_let(e); if (is_let(e)) return pp_let(e);
if (is_have(e)) return pp_have(e); if (is_have(e)) return pp_have(e);
if (!m_metavar_args && is_meta(e)) return pp_meta(get_app_fn(e));
switch (e.kind()) { switch (e.kind()) {
case expr_kind::Var: return pp_var(e); case expr_kind::Var: return pp_var(e);

1
src/frontends/lean/pp.h
View file

@ -40,6 +40,7 @@ private:
bool m_universes; bool m_universes;
bool m_full_names; bool m_full_names;
bool m_private_names; bool m_private_names;
bool m_metavar_args;
unsigned max_bp() const { return std::numeric_limits<unsigned>::max(); } unsigned max_bp() const { return std::numeric_limits<unsigned>::max(); }
name mk_metavar_name(name const & m); name mk_metavar_name(name const & m);

8
src/frontends/lean/pp_options.cpp
View file

@ -38,6 +38,10 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_PRIVATE_NAMES false #define LEAN_DEFAULT_PP_PRIVATE_NAMES false
#endif #endif
#ifndef LEAN_DEFAULT_PP_METAVAR_ARGS
#define LEAN_DEFAULT_PP_METAVAR_ARGS false
#endif
namespace lean { namespace lean {
static name g_pp_max_depth {"pp", "max_depth"}; static name g_pp_max_depth {"pp", "max_depth"};
static name g_pp_max_steps {"pp", "max_steps"}; static name g_pp_max_steps {"pp", "max_steps"};
@ -47,6 +51,7 @@ static name g_pp_coercion {"pp", "coercion"};
static name g_pp_universes {"pp", "universes"}; static name g_pp_universes {"pp", "universes"};
static name g_pp_full_names {"pp", "full_names"}; static name g_pp_full_names {"pp", "full_names"};
static name g_pp_private_names {"pp", "private_names"}; static name g_pp_private_names {"pp", "private_names"};
static name g_pp_metavar_args {"pp", "metavar_args"};
list<options> const & get_distinguishing_pp_options() { list<options> const & get_distinguishing_pp_options() {
static options g_universes_true(g_pp_universes, true); static options g_universes_true(g_pp_universes, true);
@ -76,6 +81,8 @@ RegisterBoolOption(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES,
"(pretty printer) display fully qualified names"); "(pretty printer) display fully qualified names");
RegisterBoolOption(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES, RegisterBoolOption(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES,
"(pretty printer) display internal names assigned to private declarations"); "(pretty printer) display internal names assigned to private declarations");
RegisterBoolOption(g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS,
"(pretty printer) display metavariable arguments");
unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
@ -85,4 +92,5 @@ bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_
bool get_pp_universes(options const & opts) { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); } bool get_pp_universes(options const & opts) { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
bool get_pp_full_names(options const & opts) { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); } bool get_pp_full_names(options const & opts) { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }
bool get_pp_private_names(options const & opts) { return opts.get_bool(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); } bool get_pp_private_names(options const & opts) { return opts.get_bool(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); }
bool get_pp_metavar_args(options const & opts) { return opts.get_bool(g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); }
} }

1
src/frontends/lean/pp_options.h
View file

@ -15,5 +15,6 @@ bool get_pp_coercion(options const & opts);
bool get_pp_universes(options const & opts); bool get_pp_universes(options const & opts);
bool get_pp_full_names(options const & opts); bool get_pp_full_names(options const & opts);
bool get_pp_private_names(options const & opts); bool get_pp_private_names(options const & opts);
bool get_pp_metavar_args(options const & opts);
list<options> const & get_distinguishing_pp_options(); list<options> const & get_distinguishing_pp_options();
} }