From 647078bd40e5eeb2e1760013190045b54518cb37 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 24 May 2016 11:42:06 -0400 Subject: [PATCH] feat(frontends/lean/pp): add option to hide binder types Replace old pp.hide_binder_types option Conflicts: src/frontends/lean/pp.cpp src/library/pp_options.cpp src/library/pp_options.h --- src/frontends/lean/pp.cpp | 81 +++++++++----------- src/frontends/lean/pp.h | 2 +- src/frontends/lean/print_cmd.cpp | 2 +- src/library/pp_options.cpp | 20 ++--- src/library/pp_options.h | 2 +- tests/lean/pp_binder_types.lean | 7 ++ tests/lean/pp_binder_types.lean.expected.out | 4 + 7 files changed, 61 insertions(+), 57 deletions(-) create mode 100644 tests/lean/pp_binder_types.lean create mode 100644 tests/lean/pp_binder_types.lean.expected.out diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 9b70fd614c..c149c7de96 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -297,7 +297,7 @@ void pretty_fn::set_options_core(options const & _o) { m_strings = get_pp_strings(o); m_abbreviations = get_pp_abbreviations(o); m_preterm = get_pp_preterm(o); - m_hide_binder_types = get_pp_hide_binder_types(o); + m_binder_types = get_pp_binder_types(o); m_hide_comp_irrel = get_pp_hide_comp_irrel(o); m_hide_full_terms = get_formatter_hide_full_terms(o); m_num_nat_coe = m_numerals && !m_coercion; @@ -679,65 +679,58 @@ auto pretty_fn::pp_app(expr const & e) -> result { } format pretty_fn::pp_binder(expr const & local) { - if (m_hide_binder_types) { - return format(local_pp_name(local)); - } else { - format r; - auto bi = local_info(local); - if (bi != binder_info()) - r += format(open_binder_string(bi, m_unicode)); - r += format(local_pp_name(local)); + format r; + auto bi = local_info(local); + if (bi != binder_info()) + r += format(open_binder_string(bi, m_unicode)); + r += format(local_pp_name(local)); + if (m_binder_types) { r += space(); r += compose(colon(), nest(m_indent, compose(line(), pp_child(mlocal_type(local), 0).fmt()))); - if (bi != binder_info()) - r += format(close_binder_string(bi, m_unicode)); - return r; } + if (bi != binder_info()) + r += format(close_binder_string(bi, m_unicode)); + return r; } format pretty_fn::pp_binder_block(buffer const & names, expr const & type, binder_info const & bi) { format r; - r += format(open_binder_string(bi, m_unicode)); + if (m_binder_types || bi != binder_info()) + r += format(open_binder_string(bi, m_unicode)); for (name const & n : names) { r += format(n); - r += space(); } - r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt()))); - r += format(close_binder_string(bi, m_unicode)); + if (m_binder_types) { + r += space(); + r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt()))); + } + if (m_binder_types || bi != binder_info()) + r += format(close_binder_string(bi, m_unicode)); return group(r); } format pretty_fn::pp_binders(buffer const & locals) { - if (m_hide_binder_types) { - format r; - for (auto l : locals) { - r += space(); - r += format(local_pp_name(l)); + unsigned num = locals.size(); + buffer names; + expr local = locals[0]; + expr type = mlocal_type(local); + binder_info bi = local_info(local); + names.push_back(local_pp_name(local)); + format r; + for (unsigned i = 1; i < num; i++) { + expr local = locals[i]; + if (!bi.is_inst_implicit() && mlocal_type(local) == type && local_info(local) == bi) { + names.push_back(local_pp_name(local)); + } else { + r += group(compose(line(), pp_binder_block(names, type, bi))); + names.clear(); + type = mlocal_type(local); + bi = local_info(local); + names.push_back(local_pp_name(local)); } - return r; - } else { - unsigned num = locals.size(); - buffer names; - expr local = locals[0]; - expr type = mlocal_type(local); - binder_info bi = local_info(local); - names.push_back(local_pp_name(local)); - format r; - for (unsigned i = 1; i < num; i++) { - expr local = locals[i]; - if (!bi.is_inst_implicit() && mlocal_type(local) == type && local_info(local) == bi) { - names.push_back(local_pp_name(local)); - } else { - r += group(compose(line(), pp_binder_block(names, type, bi))); - names.clear(); - type = mlocal_type(local); - bi = local_info(local); - names.push_back(local_pp_name(local)); - } - } - r += group(compose(line(), pp_binder_block(names, type, bi))); - return r; } + r += group(compose(line(), pp_binder_block(names, type, bi))); + return r; } auto pretty_fn::pp_lambda(expr const & e) -> result { diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index ec397bf450..26569ebb5e 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -65,7 +65,6 @@ private: bool m_metavar_args; bool m_purify_metavars; bool m_purify_locals; - bool m_hide_binder_types; bool m_beta; bool m_numerals; bool m_strings; @@ -73,6 +72,7 @@ private: bool m_hide_full_terms; bool m_hide_comp_irrel; bool m_preterm; + bool m_binder_types; name mk_metavar_name(name const & m); name mk_local_name(name const & n, name const & suggested); diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index d0a2d91ab3..4f979b1119 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -385,7 +385,7 @@ static bool print_constant(parser const & p, char const * kind, declaration cons out << "protected "; out << kind << " " << to_user_name(p.env(), d.get_name()); print_attributes(p, d.get_name()); - out << " : " << d.get_type(); + out.update_options(out.get_options().update((name {"pp", "binder_types"}), true)) << " : " << d.get_type(); if (is_def) out << " :="; out << "\n"; diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index be99e80caa..08ed3ffc6f 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -83,12 +83,12 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT true #endif -#ifndef LEAN_DEFAULT_PP_ALL -#define LEAN_DEFAULT_PP_ALL false +#ifndef LEAN_DEFAULT_PP_BINDER_TYPES +#define LEAN_DEFAULT_PP_BINDER_TYPES false #endif -#ifndef LEAN_DEFAULT_PP_HIDE_BINDER_TYPES -#define LEAN_DEFAULT_PP_HIDE_BINDER_TYPES false +#ifndef LEAN_DEFAULT_PP_ALL +#define LEAN_DEFAULT_PP_ALL false #endif @@ -111,7 +111,7 @@ static name * g_pp_abbreviations = nullptr; static name * g_pp_preterm = nullptr; static name * g_pp_goal_compact = nullptr; static name * g_pp_goal_max_hyps = nullptr; -static name * g_pp_hide_binder_types = nullptr; +static name * g_pp_binder_types = nullptr; static name * g_pp_hide_comp_irrel = nullptr; static name * g_pp_all = nullptr; static list * g_distinguishing_pp_options = nullptr; @@ -133,7 +133,7 @@ void initialize_pp_options() { g_pp_strings = new name{"pp", "strings"}; g_pp_abbreviations = new name{"pp", "abbreviations"}; g_pp_preterm = new name{"pp", "preterm"}; - g_pp_hide_binder_types = new name{"pp", "hide_binder_types"}; + g_pp_binder_types = new name{"pp", "binder_types"}; g_pp_hide_comp_irrel = new name{"pp", "hide_comp_irrelevant"}; g_pp_all = new name{"pp", "all"}; g_pp_goal_compact = new name{"pp", "goal", "compact"}; @@ -177,10 +177,10 @@ void initialize_pp_options() { "(pretty printer) try to display goal in a single line when possible"); register_unsigned_option(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS, "(pretty printer) maximum number of hypotheses to be displayed"); - register_bool_option(*g_pp_hide_binder_types, LEAN_DEFAULT_PP_HIDE_BINDER_TYPES, - "(pretty printer) hide types in binders"); register_bool_option(*g_pp_hide_comp_irrel, LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT, "(pretty printer) hide terms marked as computationally irrelevant, these marks are introduced by the code generator"); + register_bool_option(*g_pp_binder_types, LEAN_DEFAULT_PP_BINDER_TYPES, + "(pretty printer) display types of lambda and Pi parameters"); 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"); @@ -215,7 +215,7 @@ void finalize_pp_options() { delete g_pp_beta; delete g_pp_goal_compact; delete g_pp_goal_max_hyps; - delete g_pp_hide_binder_types; + delete g_pp_binder_types; delete g_pp_hide_comp_irrel; delete g_pp_all; delete g_distinguishing_pp_options; @@ -253,7 +253,7 @@ bool get_pp_abbreviations(options const & opts) { return opts.get_bool(* bool get_pp_preterm(options const & opts) { return opts.get_bool(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM); } bool get_pp_goal_compact(options const & opts) { return opts.get_bool(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT); } unsigned get_pp_goal_max_hyps(options const & opts) { return opts.get_unsigned(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS); } -bool get_pp_hide_binder_types(options const & opts) { return opts.get_bool(*g_pp_hide_binder_types, LEAN_DEFAULT_PP_HIDE_BINDER_TYPES); } +bool get_pp_binder_types(options const & opts) { return opts.get_bool(*g_pp_binder_types, LEAN_DEFAULT_PP_BINDER_TYPES); } bool get_pp_hide_comp_irrel(options const & opts) { return opts.get_bool(*g_pp_hide_comp_irrel, LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT); } bool get_pp_all(options const & opts) { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index 0999ff24ef..2238aae695 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -39,7 +39,7 @@ bool get_pp_abbreviations(options const & opts); bool get_pp_preterm(options const & opts); bool get_pp_goal_compact(options const & opts); unsigned get_pp_goal_max_hyps(options const & opts); -bool get_pp_hide_binder_types(options const & opts); +bool get_pp_binder_types(options const & opts); bool get_pp_hide_comp_irrel(options const & opts); bool get_pp_all(options const & opts); list const & get_distinguishing_pp_options(); diff --git a/tests/lean/pp_binder_types.lean b/tests/lean/pp_binder_types.lean new file mode 100644 index 0000000000..e2c158acc0 --- /dev/null +++ b/tests/lean/pp_binder_types.lean @@ -0,0 +1,7 @@ +open nat + +definition f (n : nat) (H : n = n) := λm, id (n + m) +print f + +set_option pp.binder_types true +print f diff --git a/tests/lean/pp_binder_types.lean.expected.out b/tests/lean/pp_binder_types.lean.expected.out new file mode 100644 index 0000000000..4a816761f9 --- /dev/null +++ b/tests/lean/pp_binder_types.lean.expected.out @@ -0,0 +1,4 @@ +definition f : Π (n : ℕ), n = n → ℕ → ℕ := +λ n H m, id (n + m) +definition f : Π (n : ℕ), n = n → ℕ → ℕ := +λ (n : ℕ) (H : n = n) (m : ℕ), id (n + m)