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

feat(frontends/lean): add option 'pp.purify_locals'

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-28 14:49:00 -08:00
parent 13405b2bb0
commit 4ec2101b06
4 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -148,6 +148,8 @@ name pretty_fn::mk_metavar_name(name const & m) {
}
name pretty_fn::mk_local_name(name const & n, name const & suggested) {
if (!m_purify_locals)
return suggested;
if (auto it = m_purify_local_table.find(n))
return *it;
unsigned i = 1;
@ -212,6 +214,7 @@ void pretty_fn::set_options_core(options const & 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_purify_locals = get_pp_purify_locals(o);
m_beta = get_pp_beta(o);
}

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

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

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

@ -47,6 +47,10 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_PURIFY_METAVARS true
#endif
#ifndef LEAN_DEFAULT_PP_PURIFY_LOCALS
#define LEAN_DEFAULT_PP_PURIFY_LOCALS true
#endif
#ifndef LEAN_DEFAULT_PP_BETA
#define LEAN_DEFAULT_PP_BETA false
#endif
@ -62,6 +66,7 @@ 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_purify_locals = nullptr;
static name * g_pp_beta = nullptr;
static list<options> * g_distinguishing_pp_options = nullptr;
@ -76,6 +81,7 @@ void initialize_pp_options() {
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_purify_locals = new name{"pp", "purify_locals"};
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");
@ -98,6 +104,9 @@ void initialize_pp_options() {
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_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS,
"(pretty printer) rename local names to avoid name capture, "
"before pretty printing");
register_bool_option(*g_pp_beta, LEAN_DEFAULT_PP_BETA,
"(pretty printer) apply beta-reduction when pretty printing");
@ -124,6 +133,7 @@ void finalize_pp_options() {
delete g_pp_private_names;
delete g_pp_metavar_args;
delete g_pp_purify_metavars;
delete g_pp_purify_locals;
delete g_pp_beta;
delete g_distinguishing_pp_options;
}
@ -146,6 +156,7 @@ bool get_pp_full_names(options const & opts) { return opts.get_bool(*g_
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_purify_locals(options const & opts) { return opts.get_bool(*g_pp_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS); }
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; }
}

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

@ -26,6 +26,7 @@ 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);
bool get_pp_purify_locals(options const & opts);
list<options> const & get_distinguishing_pp_options();
void initialize_pp_options();