diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index d5b1383b5..d8f4c9250 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -292,6 +292,7 @@ void pretty_fn::set_options_core(options const & _o) { m_numerals = get_pp_numerals(o); m_abbreviations = get_pp_abbreviations(o); m_preterm = get_pp_preterm(o); + m_binder_types = get_pp_binder_types(o); m_hide_full_terms = get_formatter_hide_full_terms(o); m_num_nat_coe = m_numerals && !m_coercion; } @@ -669,8 +670,10 @@ format pretty_fn::pp_binder(expr const & local) { if (bi != binder_info()) r += format(open_binder_string(bi, m_unicode)); r += format(local_pp_name(local)); - r += space(); - r += compose(colon(), nest(m_indent, compose(line(), pp_child(mlocal_type(local), 0).fmt()))); + 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; @@ -678,13 +681,17 @@ format pretty_fn::pp_binder(expr const & local) { 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); } diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index e07b7cf92..5fb22f3b5 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -70,6 +70,7 @@ private: bool m_abbreviations; bool m_hide_full_terms; 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 d1773bb25..afb9714f9 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -387,7 +387,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 91f40b12a..ad99bcc7b 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_GOAL_MAX_HYPS 200 #endif +#ifndef LEAN_DEFAULT_PP_BINDER_TYPES +#define LEAN_DEFAULT_PP_BINDER_TYPES false +#endif + #ifndef LEAN_DEFAULT_PP_ALL #define LEAN_DEFAULT_PP_ALL false #endif @@ -97,6 +101,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_binder_types = nullptr; static name * g_pp_all = nullptr; static list * g_distinguishing_pp_options = nullptr; @@ -119,6 +124,7 @@ void initialize_pp_options() { g_pp_all = new name{"pp", "all"}; g_pp_goal_compact = new name{"pp", "goal", "compact"}; g_pp_goal_max_hyps = new name{"pp", "goal", "max_hypotheses"}; + g_pp_binder_types = new name{"pp", "binder_types"}; register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(pretty printer) maximum expression depth, after that it will use ellipsis"); @@ -156,6 +162,8 @@ 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_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"); @@ -223,6 +231,7 @@ bool get_pp_abbreviations(options const & opts) { return opts.get_bool(*g_ 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_binder_types(options const & opts) { return opts.get_bool(*g_pp_binder_types, LEAN_DEFAULT_PP_BINDER_TYPES); } 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 dd8fa6604..51ab22e82 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -37,6 +37,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_binder_types(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 000000000..e2c158acc --- /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 000000000..4a816761f --- /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)