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

feat(frontends/lean): add option pp.purify_metavars

Browse source 
It is true by default. If the user sets it to false, then
the internal metavariable names are used in the pretty printer
This commit is contained in:
Leonardo de Moura 2014-11-09 11:04:22 -08:00
parent aef1dd9a04
commit 0b8c44a94a
4 changed files with 65 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -162,7 +162,7 @@ name pretty_fn::mk_local_name(name const & n, name const & suggested) {
}
level pretty_fn::purify(level const & l) {
if (!m_universes || !has_meta(l))
if (!m_universes || !m_purify_metavars || !has_meta(l))
return l;
return replace(l, [&](level const & l) {
if (!has_meta(l))
@ -185,7 +185,7 @@ expr pretty_fn::purify(expr const & e) {
return replace(e, [&](expr const & e, unsigned) {
if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e)))
return some_expr(e);
else if (is_metavar(e))
else if (is_metavar(e) && m_purify_metavars)
return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), mlocal_type(e)));
else if (is_local(e))
return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), local_pp_name(e)), mlocal_type(e), local_info(e)));
@ -199,19 +199,20 @@ expr pretty_fn::purify(expr const & e) {
}
void pretty_fn::set_options_core(options const & o) {
m_options = 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_coercions(o);
m_notation = get_pp_notation(o);
m_universes = get_pp_universes(o);
m_full_names = get_pp_full_names(o);
m_private_names = get_pp_private_names(o);
m_metavar_args = get_pp_metavar_args(o);
m_beta = get_pp_beta(o);
m_options = 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_coercions(o);
m_notation = get_pp_notation(o);
m_universes = get_pp_universes(o);
m_full_names = get_pp_full_names(o);
m_private_names = get_pp_private_names(o);
m_metavar_args = get_pp_metavar_args(o);
m_purify_metavars = get_pp_purify_metavars(o);
m_beta = get_pp_beta(o);
}
void pretty_fn::set_options(options const & o) {
@ -373,7 +374,10 @@ auto pretty_fn::pp_const(expr const & e) -> result {
}
auto pretty_fn::pp_meta(expr const & e) -> result {
return result(compose(format("?"), format(mlocal_name(e))));
if (m_purify_metavars)
return result(compose(format("?"), format(mlocal_name(e))));
else
return result(compose(format("?M."), format(mlocal_name(e))));
}
auto pretty_fn::pp_local(expr const & e) -> result {

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

@ -61,6 +61,7 @@ private:
bool m_full_names;
bool m_private_names;
bool m_metavar_args;
bool m_purify_metavars;
bool m_beta;
name mk_metavar_name(name const & m);

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

@ -43,34 +43,40 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_METAVAR_ARGS false
#endif
#ifndef LEAN_DEFAULT_PP_PURIFY_METAVARS
#define LEAN_DEFAULT_PP_PURIFY_METAVARS true
#endif
#ifndef LEAN_DEFAULT_PP_BETA
#define LEAN_DEFAULT_PP_BETA false
#endif
namespace lean {
static name * g_pp_max_depth = nullptr;
static name * g_pp_max_steps = nullptr;
static name * g_pp_notation = nullptr;
static name * g_pp_implicit = nullptr;
static name * g_pp_coercions = nullptr;
static name * g_pp_universes = nullptr;
static name * g_pp_full_names = nullptr;
static name * g_pp_private_names = nullptr;
static name * g_pp_metavar_args = nullptr;
static name * g_pp_beta = nullptr;
static name * g_pp_max_depth = nullptr;
static name * g_pp_max_steps = nullptr;
static name * g_pp_notation = nullptr;
static name * g_pp_implicit = nullptr;
static name * g_pp_coercions = nullptr;
static name * g_pp_universes = nullptr;
static name * g_pp_full_names = nullptr;
static name * g_pp_private_names = nullptr;
static name * g_pp_metavar_args = nullptr;
static name * g_pp_purify_metavars = nullptr;
static name * g_pp_beta = nullptr;
static list<options> * g_distinguishing_pp_options = nullptr;
void initialize_pp_options() {
g_pp_max_depth = new name{"pp", "max_depth"};
g_pp_max_steps = new name{"pp", "max_steps"};
g_pp_notation = new name{"pp", "notation"};
g_pp_implicit = new name{"pp", "implicit"};
g_pp_coercions = new name{"pp", "coercions"};
g_pp_universes = new name{"pp", "universes"};
g_pp_full_names = new name{"pp", "full_names"};
g_pp_private_names = new name{"pp", "private_names"};
g_pp_metavar_args = new name{"pp", "metavar_args"};
g_pp_beta = new name{"pp", "beta"};
g_pp_max_depth = new name{"pp", "max_depth"};
g_pp_max_steps = new name{"pp", "max_steps"};
g_pp_notation = new name{"pp", "notation"};
g_pp_implicit = new name{"pp", "implicit"};
g_pp_coercions = new name{"pp", "coercions"};
g_pp_universes = new name{"pp", "universes"};
g_pp_full_names = new name{"pp", "full_names"};
g_pp_private_names = new name{"pp", "private_names"};
g_pp_metavar_args = new name{"pp", "metavar_args"};
g_pp_purify_metavars = new name{"pp", "purify_metavars"};
g_pp_beta = new name{"pp", "beta"};
register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
"(pretty printer) maximum expression depth, after that it will use ellipsis");
register_unsigned_option(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS,
@ -89,6 +95,9 @@ void initialize_pp_options() {
"(pretty printer) display internal names assigned to private declarations");
register_bool_option(*g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS,
"(pretty printer) display metavariable arguments");
register_bool_option(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS,
"(pretty printer) rename internal metavariable names (with \"user-friendly\" ones) "
"before pretty printing");
register_bool_option(*g_pp_beta, LEAN_DEFAULT_PP_BETA,
"(pretty printer) apply beta-reduction when pretty printing");
@ -114,6 +123,7 @@ void finalize_pp_options() {
delete g_pp_full_names;
delete g_pp_private_names;
delete g_pp_metavar_args;
delete g_pp_purify_metavars;
delete g_pp_beta;
delete g_distinguishing_pp_options;
}
@ -123,16 +133,18 @@ name const & get_pp_full_names_option_name() { return *g_pp_full_names; }
name const & get_pp_universes_option_name() { return *g_pp_universes; }
name const & get_pp_notation_option_name() { return *g_pp_notation; }
name const & get_pp_metavar_args_name() { return *g_pp_metavar_args; }
name const & get_pp_purify_metavars_name() { return *g_pp_purify_metavars; }
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); }
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_coercions(options const & opts) { return opts.get_bool(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); }
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_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); }
bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); }
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); }
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_coercions(options const & opts) { return opts.get_bool(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); }
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_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); }
bool get_pp_purify_metavars(options const & opts) { return opts.get_bool(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS); }
bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); }
list<options> const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; }
}

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

@ -12,6 +12,7 @@ name const & get_pp_full_names_option_name();
name const & get_pp_universes_option_name();
name const & get_pp_notation_option_name();
name const & get_pp_metavar_args_name();
name const & get_pp_purify_metavars_name();
unsigned get_pp_max_depth(options const & opts);
unsigned get_pp_max_steps(options const & opts);
@ -23,6 +24,7 @@ bool get_pp_full_names(options const & opts);
bool get_pp_private_names(options const & opts);
bool get_pp_metavar_args(options const & opts);
bool get_pp_beta(options const & opts);
bool get_pp_purify_metavars(options const & opts);
list<options> const & get_distinguishing_pp_options();
void initialize_pp_options();