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

feat(frontends/lean/pp): add option for displaying fully qualified names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-10 15:55:19 +01:00
parent 06beff327f
commit c13c75b93e
5 changed files with 38 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -91,14 +91,15 @@ expr pretty_fn::purify(expr const & e) {
}
void pretty_fn::set_options(options const & o) {
m_indent = get_pp_indent(o);
m_max_depth = get_pp_max_depth(o);
m_max_steps = get_pp_max_steps(o);
m_implict = get_pp_implicit(o);
m_unicode = get_pp_unicode(o);
m_coercion = get_pp_coercion(o);
m_notation = get_pp_notation(o);
m_universes = get_pp_universes(o);
m_indent = get_pp_indent(o);
m_max_depth = get_pp_max_depth(o);
m_max_steps = get_pp_max_steps(o);
m_implict = get_pp_implicit(o);
m_unicode = get_pp_unicode(o);
m_coercion = get_pp_coercion(o);
m_notation = get_pp_notation(o);
m_universes = get_pp_universes(o);
m_full_names = get_pp_full_names(o);
}
format pretty_fn::pp_level(level const & l) {
@ -156,14 +157,16 @@ auto pretty_fn::pp_sort(expr const & e) -> result {
auto pretty_fn::pp_const(expr const & e) -> result {
name n = const_name(e);
if (auto it = is_aliased(m_env, mk_constant(n))) { // TODO(Leo): fix is_aliased should get a name as argument
n = *it;
} else {
for (name const & ns : get_namespaces(m_env)) {
name new_n = n.replace_prefix(ns, name());
if (new_n != n) {
n = new_n;
break;
if (!m_full_names) {
if (auto it = is_aliased(m_env, mk_constant(n))) { // TODO(Leo): fix is_aliased should get a name as argument
n = *it;
} else {
for (name const & ns : get_namespaces(m_env)) {
name new_n = n.replace_prefix(ns, name());
if (new_n != n) {
n = new_n;
break;
}
}
}
}

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

@ -37,6 +37,7 @@ private:
bool m_coercion; //!< if true show coercions
bool m_notation;
bool m_universes;
bool m_full_names;
void set_options(options const & o);

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

@ -30,6 +30,10 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_UNIVERSES false
#endif
#ifndef LEAN_DEFAULT_PP_FULL_NAMES
#define LEAN_DEFAULT_PP_FULL_NAMES false
#endif
namespace lean {
static name g_pp_max_depth {"pp", "max_depth"};
static name g_pp_max_steps {"pp", "max_steps"};
@ -37,6 +41,7 @@ static name g_pp_notation {"pp", "notation"};
static name g_pp_implicit {"pp", "implicit"};
static name g_pp_coercion {"pp", "coercion"};
static name g_pp_universes {"pp", "universes"};
static name g_pp_full_names {"pp", "full_names"};
RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
"(pretty printer) maximum expression depth, after that it will use ellipsis");
@ -50,6 +55,8 @@ RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_COERCION,
"(pretty printer) display coercions");
RegisterBoolOption(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES,
"(pretty printer) display universes");
RegisterBoolOption(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES,
"(pretty printer) display fully qualified names");
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); }
@ -57,4 +64,5 @@ bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_not
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_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); }
}

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

@ -13,4 +13,5 @@ bool get_pp_notation(options const & opts);
bool get_pp_implicit(options const & opts);
bool get_pp_coercion(options const & opts);
bool get_pp_universes(options const & opts);
bool get_pp_full_names(options const & opts);
}

9
tests/lean/run/full.lean Normal file
View file

@ -0,0 +1,9 @@
import standard
namespace foo
variable x : num.num
check x
using num
check x
set_option pp.full_names true
check x
end