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

feat(frontends/lean/pp): add option for displaying internal names associated with private declarations

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-25 11:03:54 -07:00
parent 0c668a31fe
commit 811f46e97b
4 changed files with 31 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -95,15 +95,16 @@ expr pretty_fn::purify(expr const & e) {
} }
void pretty_fn::set_options(options const & o) { void pretty_fn::set_options(options const & o) {
m_indent = get_pp_indent(o); m_indent = get_pp_indent(o);
m_max_depth = get_pp_max_depth(o); m_max_depth = get_pp_max_depth(o);
m_max_steps = get_pp_max_steps(o); m_max_steps = get_pp_max_steps(o);
m_implict = get_pp_implicit(o); m_implict = get_pp_implicit(o);
m_unicode = get_pp_unicode(o); m_unicode = get_pp_unicode(o);
m_coercion = get_pp_coercion(o); m_coercion = get_pp_coercion(o);
m_notation = get_pp_notation(o); m_notation = get_pp_notation(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);
} }
format pretty_fn::pp_level(level const & l) { format pretty_fn::pp_level(level const & l) {
@ -176,8 +177,10 @@ auto pretty_fn::pp_const(expr const & e) -> result {
} }
} }
} }
if (auto n1 = hidden_to_user_name(m_env, n)) if (!m_private_names) {
n = *n1; if (auto n1 = hidden_to_user_name(m_env, n))
n = *n1;
}
if (m_universes && !empty(const_levels(e))) { if (m_universes && !empty(const_levels(e))) {
format r = compose(format(n), format(".{")); format r = compose(format(n), format(".{"));
bool first = true; bool first = true;

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

@ -38,6 +38,7 @@ private:
bool m_notation; bool m_notation;
bool m_universes; bool m_universes;
bool m_full_names; bool m_full_names;
bool m_private_names;
void set_options(options const & o); void set_options(options const & o);

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

@ -34,6 +34,10 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_FULL_NAMES false #define LEAN_DEFAULT_PP_FULL_NAMES false
#endif #endif
#ifndef LEAN_DEFAULT_PP_PRIVATE_NAMES
#define LEAN_DEFAULT_PP_PRIVATE_NAMES 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"};
@ -42,6 +46,7 @@ static name g_pp_implicit {"pp", "implicit"};
static name g_pp_coercion {"pp", "coercion"}; 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"};
RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
"(pretty printer) maximum expression depth, after that it will use ellipsis"); "(pretty printer) maximum expression depth, after that it will use ellipsis");
@ -57,12 +62,15 @@ RegisterBoolOption(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES,
"(pretty printer) display universes"); "(pretty printer) display universes");
RegisterBoolOption(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES, 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,
"(pretty printer) display internal names assigned to private declarations");
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); }
bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); } bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); }
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); }
} }

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

@ -14,4 +14,5 @@ bool get_pp_implicit(options const & opts);
bool get_pp_coercion(options const & opts); 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);
} }