From c76d92284fd274b149f3a948832eb850de2e221e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Jun 2015 08:41:46 -0700 Subject: [PATCH] feat(library/pp_options): add 'pp.all' option --- src/frontends/lean/pp.cpp | 15 ++++++++------- src/library/pp_options.cpp | 16 +++++++++++++--- src/library/pp_options.h | 1 + tests/lean/pp_all.lean | 9 +++++++++ tests/lean/pp_all.lean.expected.out | 2 ++ 5 files changed, 33 insertions(+), 10 deletions(-) create mode 100644 tests/lean/pp_all.lean create mode 100644 tests/lean/pp_all.lean.expected.out diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 1641e109c..9fa6ba52b 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -269,22 +269,23 @@ expr pretty_fn::purify(expr const & e) { void pretty_fn::set_options_core(options const & o) { m_options = o; + bool all = get_pp_all(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_implict = all || 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_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_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); + m_beta = !all && get_pp_beta(o); m_numerals = get_pp_numerals(o); - m_abbreviations = get_pp_abbreviations(o); + m_abbreviations = !all && get_pp_abbreviations(o); m_extra_spaces = get_pp_extra_spaces(o); m_preterm = get_pp_preterm(o); m_hide_full_terms = get_formatter_hide_full_terms(o); diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 5ebff3529..228caf98e 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -75,6 +75,10 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_COMPACT_GOALS false #endif +#ifndef LEAN_DEFAULT_PP_ALL +#define LEAN_DEFAULT_PP_ALL false +#endif + namespace lean { static name * g_pp_max_depth = nullptr; static name * g_pp_max_steps = nullptr; @@ -93,6 +97,7 @@ static name * g_pp_abbreviations = nullptr; static name * g_pp_extra_spaces = nullptr; static name * g_pp_preterm = nullptr; static name * g_pp_compact_goals = nullptr; +static name * g_pp_all = nullptr; static list * g_distinguishing_pp_options = nullptr; void initialize_pp_options() { @@ -112,7 +117,8 @@ void initialize_pp_options() { g_pp_abbreviations = new name{"pp", "abbreviations"}; g_pp_extra_spaces = new name{"pp", "extra_spaces"}; g_pp_preterm = new name{"pp", "preterm"}; - g_pp_compact_goals = new name({"pp", "compact_goals"}); + g_pp_all = new name{"pp", "all"}; + g_pp_compact_goals = new name{"pp", "compact_goals"}; 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, @@ -149,7 +155,9 @@ void initialize_pp_options() { "(pretty printer) assume the term is a preterm (i.e., a term before elaboration)"); register_bool_option(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS, "(pretty printer) try to display goal in a single line when possible"); - + register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL, + "(pretty printer) display coercions, implicit parameters, fully qualified names, universes, " + "and disable abbreviations, beta reduction and notation during pretty printing"); options universes_true(*g_pp_universes, true); options full_names_true(*g_pp_full_names, true); options implicit_true(*g_pp_implicit, true); @@ -180,6 +188,7 @@ void finalize_pp_options() { delete g_pp_purify_locals; delete g_pp_beta; delete g_pp_compact_goals; + delete g_pp_all; delete g_distinguishing_pp_options; } @@ -210,7 +219,8 @@ bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_ bool get_pp_abbreviations(options const & opts) { return opts.get_bool(*g_pp_abbreviations, LEAN_DEFAULT_PP_ABBREVIATIONS); } bool get_pp_extra_spaces(options const & opts) { return opts.get_bool(*g_pp_extra_spaces, LEAN_DEFAULT_PP_EXTRA_SPACES); } bool get_pp_preterm(options const & opts) { return opts.get_bool(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM); } -bool get_pp_compact_goals(options const & o) { return o.get_bool(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS); } +bool get_pp_compact_goals(options const & opts) { return opts.get_bool(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS); } +bool get_pp_all(options const & opts) { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); } list const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; } } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index 1783a3d55..1470f5648 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -35,6 +35,7 @@ bool get_pp_abbreviations(options const & opts); bool get_pp_extra_spaces(options const & opts); bool get_pp_preterm(options const & opts); bool get_pp_compact_goals(options const & opts); +bool get_pp_all(options const & opts); list const & get_distinguishing_pp_options(); void initialize_pp_options(); diff --git a/tests/lean/pp_all.lean b/tests/lean/pp_all.lean new file mode 100644 index 000000000..08a1d25c5 --- /dev/null +++ b/tests/lean/pp_all.lean @@ -0,0 +1,9 @@ +open nat + +variables {a : nat} + +abbreviation b := 2 + +check (λ x, x) a + b = 10 +set_option pp.all true +check (λ x, x) a + b = 10 diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out new file mode 100644 index 000000000..e01571659 --- /dev/null +++ b/tests/lean/pp_all.lean.expected.out @@ -0,0 +1,2 @@ +a + b = 10 : Prop +@eq.{1} nat (nat.add ((λ (x : nat), x) a) (nat.of_num 2)) (nat.of_num 10) : Prop