From 7f1800962a4491e46781fc539f419b6f0e111405 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Dec 2015 10:40:48 -0800 Subject: [PATCH] feat(frontends/lean/pp): allow user to override pp.all setting see #922 --- src/frontends/lean/builtin_cmds.cpp | 8 +++---- src/frontends/lean/elaborator.cpp | 4 ++-- src/frontends/lean/info_manager.cpp | 8 +++---- src/frontends/lean/pp.cpp | 31 +++++++++++++++++++--------- src/library/pp_options.cpp | 10 +++++---- src/library/pp_options.h | 10 +++++---- tests/lean/pp_all2.lean | 7 +++++++ tests/lean/pp_all2.lean.expected.out | 1 + 8 files changed, 51 insertions(+), 28 deletions(-) create mode 100644 tests/lean/pp_all2.lean create mode 100644 tests/lean/pp_all2.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 944b82d65..2d08a1fb2 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -71,7 +71,7 @@ namespace lean { static void print_coercions(parser & p, optional const & C) { environment const & env = p.env(); 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); char const * arrow = get_pp_unicode(opts) ? "↣" : ">->"; 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; io_state ios = p.ios(); options os = ios.get_options(); - os = os.update_if_undef(get_pp_full_names_option_name(), true); - os = os.update(get_pp_notation_option_name(), false); + os = os.update_if_undef(get_pp_full_names_name(), true); + os = os.update(get_pp_notation_name(), false); os = os.update(get_pp_preterm_name(), true); ios.set_options(os); optional tt(get_token_table(p.env())); @@ -622,7 +622,7 @@ environment print_cmd(parser & p) { expr e = p.parse_expr(); io_state_stream out = p.regular_stream(); 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; } else if (p.curr_is_token_or_id(get_no_pattern_attr_tk())) { p.next(); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c876949b4..3acd9db1c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1155,7 +1155,7 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) { lean_assert(r.first == Inaccessible); throw_elaborator_exception(eqns, [=](formatter const & fmt) { 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); expr const & f = get_app_fn(lhs); format r; @@ -2198,7 +2198,7 @@ void elaborator::check_sort_assignments(substitution const & s) { substitution saved_s(s); throw_kernel_exception(env(), pre, [=](formatter const & fmt) { 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" " to be a fixed value, computed sort is"); r += pp_indent_expr(fmt.update_options(o), substitution(saved_s).instantiate(post)); diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index dca7f41df..7aaffa05b 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -176,7 +176,7 @@ public: virtual void display(io_state_stream const & ios, unsigned line) const { ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n"; 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); for (unsigned i = 0; i < get_num_choices(m_choices); i++) { if (i > 0) @@ -197,8 +197,8 @@ public: virtual void display(io_state_stream const & ios, unsigned line) const { ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n"; options os = ios.get_options(); - os = os.update_if_undef(get_pp_full_names_option_name(), true); - os = os.update_if_undef(get_pp_notation_option_name(), false); + os = os.update_if_undef(get_pp_full_names_name(), true); + os = os.update_if_undef(get_pp_notation_name(), false); auto new_ios = ios.update_options(os); bool first = true; for (expr const & e : m_alts) { @@ -221,7 +221,7 @@ public: virtual void display(io_state_stream const & ios, unsigned line) const { ios << "-- COERCION|" << line << "|" << get_column() << "\n"; 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 << "-- ACK" << endl; } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 680b08df4..bd04f3835 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -263,25 +263,36 @@ expr pretty_fn::purify(expr const & e) { }); } -void pretty_fn::set_options_core(options const & o) { - m_options = o; +void pretty_fn::set_options_core(options const & _o) { + options o = _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_max_depth = get_pp_max_depth(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_coercion = all || get_pp_coercions(o); - m_notation = !all && get_pp_notation(o); - m_universes = all || get_pp_universes(o); - m_full_names = all || get_pp_full_names(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_purify_locals = get_pp_purify_locals(o); - m_beta = !all && get_pp_beta(o); - m_numerals = !all && get_pp_numerals(o); - m_abbreviations = !all && get_pp_abbreviations(o); + m_beta = get_pp_beta(o); + m_numerals = get_pp_numerals(o); + m_abbreviations = get_pp_abbreviations(o); m_preterm = get_pp_preterm(o); m_hide_full_terms = get_formatter_hide_full_terms(o); m_num_nat_coe = m_numerals && !m_coercion; diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 68e7914c8..edc485afe 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -184,15 +184,17 @@ void finalize_pp_options() { } 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_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_coercions_name() { return *g_pp_coercions; } +name const & get_pp_full_names_name() { return *g_pp_full_names; } +name const & get_pp_universes_name() { return *g_pp_universes; } +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_purify_metavars_name() { return *g_pp_purify_metavars; } 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_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_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index 341dc6971..beaa7946a 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -8,15 +8,17 @@ Author: Leonardo de Moura #include "util/sexpr/options.h" namespace lean { name const & get_pp_implicit_name(); -name const & get_pp_coercions_option_name(); -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_coercions_name(); +name const & get_pp_full_names_name(); +name const & get_pp_universes_name(); +name const & get_pp_notation_name(); name const & get_pp_metavar_args_name(); name const & get_pp_purify_metavars_name(); name const & get_pp_purify_locals_name(); name const & get_pp_beta_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_steps(options const & opts); diff --git a/tests/lean/pp_all2.lean b/tests/lean/pp_all2.lean new file mode 100644 index 000000000..e9922e721 --- /dev/null +++ b/tests/lean/pp_all2.lean @@ -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) diff --git a/tests/lean/pp_all2.lean.expected.out b/tests/lean/pp_all2.lean.expected.out new file mode 100644 index 000000000..f7ed80d31 --- /dev/null +++ b/tests/lean/pp_all2.lean.expected.out @@ -0,0 +1 @@ +@add nat nat_has_add 10 3 : nat