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

feat(frontends/lean/pp): allow user to override pp.all setting

Browse source 
see #922
This commit is contained in:
Leonardo de Moura 2015-12-11 10:40:48 -08:00
parent a35fd06a33
commit 7f1800962a
8 changed files with 51 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -71,7 +71,7 @@ namespace lean {
static void print_coercions(parser & p, optional<name> const & C) { static void print_coercions(parser & p, optional<name> const & C) {
environment const & env = p.env(); environment const & env = p.env();
options opts = p.regular_stream().get_options(); options opts = p.regular_stream().get_options();
opts = opts.update(get_pp_coercions_option_name(), true); opts = opts.update(get_pp_coercions_name(), true);
io_state_stream out = p.regular_stream().update_options(opts); io_state_stream out = p.regular_stream().update_options(opts);
char const * arrow = get_pp_unicode(opts) ? "↣" : ">->"; char const * arrow = get_pp_unicode(opts) ? "↣" : ">->";
for_each_coercion_user(env, [&](name const & C1, name const & c, name const & D) { for_each_coercion_user(env, [&](name const & C1, name const & c, name const & D) {
@ -194,8 +194,8 @@ static bool print_parse_table(parser const & p, parse_table const & t, bool nud,
bool found = false; bool found = false;
io_state ios = p.ios(); io_state ios = p.ios();
options os = ios.get_options(); options os = ios.get_options();
os = os.update_if_undef(get_pp_full_names_option_name(), true); os = os.update_if_undef(get_pp_full_names_name(), true);
os = os.update(get_pp_notation_option_name(), false); os = os.update(get_pp_notation_name(), false);
os = os.update(get_pp_preterm_name(), true); os = os.update(get_pp_preterm_name(), true);
ios.set_options(os); ios.set_options(os);
optional<token_table> tt(get_token_table(p.env())); optional<token_table> tt(get_token_table(p.env()));
@ -622,7 +622,7 @@ environment print_cmd(parser & p) {
expr e = p.parse_expr(); expr e = p.parse_expr();
io_state_stream out = p.regular_stream(); io_state_stream out = p.regular_stream();
options opts = out.get_options(); options opts = out.get_options();
opts = opts.update(get_pp_notation_option_name(), false); opts = opts.update(get_pp_notation_name(), false);
out.update_options(opts) << e << endl; out.update_options(opts) << e << endl;
} else if (p.curr_is_token_or_id(get_no_pattern_attr_tk())) { } else if (p.curr_is_token_or_id(get_no_pattern_attr_tk())) {
p.next(); p.next();

4
src/frontends/lean/elaborator.cpp
View file

@ -1155,7 +1155,7 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) {
lean_assert(r.first == Inaccessible); lean_assert(r.first == Inaccessible);
throw_elaborator_exception(eqns, [=](formatter const & fmt) { throw_elaborator_exception(eqns, [=](formatter const & fmt) {
options o = fmt.get_options().update_if_undef(get_pp_implicit_name(), true); options o = fmt.get_options().update_if_undef(get_pp_implicit_name(), true);
o = o.update_if_undef(get_pp_notation_option_name(), false); o = o.update_if_undef(get_pp_notation_name(), false);
formatter new_fmt = fmt.update_options(o); formatter new_fmt = fmt.update_options(o);
expr const & f = get_app_fn(lhs); expr const & f = get_app_fn(lhs);
format r; format r;
@ -2198,7 +2198,7 @@ void elaborator::check_sort_assignments(substitution const & s) {
substitution saved_s(s); substitution saved_s(s);
throw_kernel_exception(env(), pre, [=](formatter const & fmt) { throw_kernel_exception(env(), pre, [=](formatter const & fmt) {
options o = fmt.get_options(); options o = fmt.get_options();
o = o.update(get_pp_universes_option_name(), true); o = o.update(get_pp_universes_name(), true);
format r("solution computed by the elaborator forces a universe placeholder" format r("solution computed by the elaborator forces a universe placeholder"
" to be a fixed value, computed sort is"); " to be a fixed value, computed sort is");
r += pp_indent_expr(fmt.update_options(o), substitution(saved_s).instantiate(post)); r += pp_indent_expr(fmt.update_options(o), substitution(saved_s).instantiate(post));

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

@ -176,7 +176,7 @@ public:
virtual void display(io_state_stream const & ios, unsigned line) const { virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n"; ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n";
options os = ios.get_options(); options os = ios.get_options();
os = os.update_if_undef(get_pp_full_names_option_name(), true); os = os.update_if_undef(get_pp_full_names_name(), true);
auto new_ios = ios.update_options(os); auto new_ios = ios.update_options(os);
for (unsigned i = 0; i < get_num_choices(m_choices); i++) { for (unsigned i = 0; i < get_num_choices(m_choices); i++) {
if (i > 0) if (i > 0)
@ -197,8 +197,8 @@ public:
virtual void display(io_state_stream const & ios, unsigned line) const { virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n"; ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n";
options os = ios.get_options(); options os = ios.get_options();
os = os.update_if_undef(get_pp_full_names_option_name(), true); os = os.update_if_undef(get_pp_full_names_name(), true);
os = os.update_if_undef(get_pp_notation_option_name(), false); os = os.update_if_undef(get_pp_notation_name(), false);
auto new_ios = ios.update_options(os); auto new_ios = ios.update_options(os);
bool first = true; bool first = true;
for (expr const & e : m_alts) { for (expr const & e : m_alts) {
@ -221,7 +221,7 @@ public:
virtual void display(io_state_stream const & ios, unsigned line) const { virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- COERCION|" << line << "|" << get_column() << "\n"; ios << "-- COERCION|" << line << "|" << get_column() << "\n";
options os = ios.get_options(); options os = ios.get_options();
os = os.update_if_undef(get_pp_coercions_option_name(), true); os = os.update_if_undef(get_pp_coercions_name(), true);
ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl; ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl;
ios << "-- ACK" << endl; ios << "-- ACK" << endl;
} }

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

@ -263,25 +263,36 @@ expr pretty_fn::purify(expr const & e) {
}); });
} }
void pretty_fn::set_options_core(options const & o) { void pretty_fn::set_options_core(options const & _o) {
m_options = o; options o = _o;
bool all = get_pp_all(o); bool all = get_pp_all(o);
if (all) {
o = o.update_if_undef(get_pp_implicit_name(), true);
o = o.update_if_undef(get_pp_coercions_name(), true);
o = o.update_if_undef(get_pp_notation_name(), false);
o = o.update_if_undef(get_pp_universes_name(), true);
o = o.update_if_undef(get_pp_full_names_name(), true);
o = o.update_if_undef(get_pp_beta_name(), false);
o = o.update_if_undef(get_pp_numerals_name(), false);
o = o.update_if_undef(get_pp_abbreviations_name(), false);
}
m_options = 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 = all || get_pp_implicit(o); m_implict = get_pp_implicit(o);
m_unicode = get_pp_unicode(o); m_unicode = get_pp_unicode(o);
m_coercion = all || get_pp_coercions(o); m_coercion = get_pp_coercions(o);
m_notation = !all && get_pp_notation(o); m_notation = get_pp_notation(o);
m_universes = all || get_pp_universes(o); m_universes = get_pp_universes(o);
m_full_names = all || get_pp_full_names(o); m_full_names = get_pp_full_names(o);
m_private_names = get_pp_private_names(o); m_private_names = get_pp_private_names(o);
m_metavar_args = get_pp_metavar_args(o); m_metavar_args = get_pp_metavar_args(o);
m_purify_metavars = get_pp_purify_metavars(o); m_purify_metavars = get_pp_purify_metavars(o);
m_purify_locals = get_pp_purify_locals(o); m_purify_locals = get_pp_purify_locals(o);
m_beta = !all && get_pp_beta(o); m_beta = get_pp_beta(o);
m_numerals = !all && get_pp_numerals(o); m_numerals = get_pp_numerals(o);
m_abbreviations = !all && get_pp_abbreviations(o); m_abbreviations = get_pp_abbreviations(o);
m_preterm = get_pp_preterm(o); m_preterm = get_pp_preterm(o);
m_hide_full_terms = get_formatter_hide_full_terms(o); m_hide_full_terms = get_formatter_hide_full_terms(o);
m_num_nat_coe = m_numerals && !m_coercion; m_num_nat_coe = m_numerals && !m_coercion;

10
src/library/pp_options.cpp
View file

@ -184,15 +184,17 @@ void finalize_pp_options() {
} }
name const & get_pp_implicit_name() { return *g_pp_implicit; } name const & get_pp_implicit_name() { return *g_pp_implicit; }
name const & get_pp_coercions_option_name() { return *g_pp_coercions; } name const & get_pp_coercions_name() { return *g_pp_coercions; }
name const & get_pp_full_names_option_name() { return *g_pp_full_names; } name const & get_pp_full_names_name() { return *g_pp_full_names; }
name const & get_pp_universes_option_name() { return *g_pp_universes; } name const & get_pp_universes_name() { return *g_pp_universes; }
name const & get_pp_notation_option_name() { return *g_pp_notation; } name const & get_pp_notation_name() { return *g_pp_notation; }
name const & get_pp_metavar_args_name() { return *g_pp_metavar_args; } name const & get_pp_metavar_args_name() { return *g_pp_metavar_args; }
name const & get_pp_purify_metavars_name() { return *g_pp_purify_metavars; } name const & get_pp_purify_metavars_name() { return *g_pp_purify_metavars; }
name const & get_pp_purify_locals_name() { return *g_pp_purify_locals; } name const & get_pp_purify_locals_name() { return *g_pp_purify_locals; }
name const & get_pp_beta_name() { return *g_pp_beta; } name const & get_pp_beta_name() { return *g_pp_beta; }
name const & get_pp_preterm_name() { return *g_pp_preterm; } name const & get_pp_preterm_name() { return *g_pp_preterm; }
name const & get_pp_numerals_name() { return *g_pp_numerals; }
name const & get_pp_abbreviations_name() { return *g_pp_abbreviations; }
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); }

10
src/library/pp_options.h
View file

@ -8,15 +8,17 @@ Author: Leonardo de Moura
#include "util/sexpr/options.h" #include "util/sexpr/options.h"
namespace lean { namespace lean {
name const & get_pp_implicit_name(); name const & get_pp_implicit_name();
name const & get_pp_coercions_option_name(); name const & get_pp_coercions_name();
name const & get_pp_full_names_option_name(); name const & get_pp_full_names_name();
name const & get_pp_universes_option_name(); name const & get_pp_universes_name();
name const & get_pp_notation_option_name(); name const & get_pp_notation_name();
name const & get_pp_metavar_args_name(); name const & get_pp_metavar_args_name();
name const & get_pp_purify_metavars_name(); name const & get_pp_purify_metavars_name();
name const & get_pp_purify_locals_name(); name const & get_pp_purify_locals_name();
name const & get_pp_beta_name(); name const & get_pp_beta_name();
name const & get_pp_preterm_name(); name const & get_pp_preterm_name();
name const & get_pp_numerals_name();
name const & get_pp_abbreviations_name();
unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_depth(options const & opts);
unsigned get_pp_max_steps(options const & opts); unsigned get_pp_max_steps(options const & opts);

7
tests/lean/pp_all2.lean Normal file
View file

@ -0,0 +1,7 @@
import data.nat
set_option pp.all true
set_option pp.numerals true
set_option pp.universes false
check (10 : nat) + (3 : nat)

1
tests/lean/pp_all2.lean.expected.out Normal file
View file

@ -0,0 +1 @@
@add nat nat_has_add 10 3 : nat