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

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

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-11 17:28:58 -08:00
parent 97552a8cfe
commit 287a444481
4 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -271,7 +271,8 @@ void pretty_fn::set_options_core(options const & o) {
m_purify_metavars = get_pp_purify_metavars(o);
m_purify_locals = get_pp_purify_locals(o);
m_beta = get_pp_beta(o);
m_num_nat_coe = !m_coercion && has_coercion_num_nat(m_env);
m_numerals = get_pp_numerals(o);
m_num_nat_coe = m_numerals && !m_coercion && has_coercion_num_nat(m_env);
}
void pretty_fn::set_options(options const & o) {
@ -1041,7 +1042,8 @@ auto pretty_fn::pp(expr const & e) -> result {
if (is_let(e)) return pp_let(e);
if (is_typed_expr(e)) return pp(get_typed_expr_expr(e));
if (is_let_value(e)) return pp(get_let_value_expr(e));
if (auto n = to_num(e)) return pp_num(*n);
if (m_numerals)
if (auto n = to_num(e)) return pp_num(*n);
if (m_num_nat_coe)
if (auto k = to_unsigned(e))
return format(*k);

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

@ -65,6 +65,7 @@ private:
bool m_purify_metavars;
bool m_purify_locals;
bool m_beta;
bool m_numerals;
name mk_metavar_name(name const & m);
name mk_local_name(name const & n, name const & suggested);

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

@ -55,6 +55,10 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_BETA false
#endif
#ifndef LEAN_DEFAULT_PP_NUMERALS
#define LEAN_DEFAULT_PP_NUMERALS true
#endif
namespace lean {
static name * g_pp_max_depth = nullptr;
static name * g_pp_max_steps = nullptr;
@ -68,6 +72,7 @@ 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 name * g_pp_numerals = nullptr;
static list<options> * g_distinguishing_pp_options = nullptr;
void initialize_pp_options() {
@ -83,6 +88,7 @@ void initialize_pp_options() {
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"};
g_pp_numerals = new name{"pp", "numerals"};
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,
@ -109,6 +115,8 @@ void initialize_pp_options() {
"before pretty printing");
register_bool_option(*g_pp_beta, LEAN_DEFAULT_PP_BETA,
"(pretty printer) apply beta-reduction when pretty printing");
register_bool_option(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS,
"(pretty printer) display nat/num numerals in decimal notation");
options universes_true(*g_pp_universes, true);
options full_names_true(*g_pp_full_names, true);
@ -158,5 +166,6 @@ bool get_pp_metavar_args(options const & opts) { return opts.get_bool(*g_
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); }
bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS); }
list<options> const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; }
}

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

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