diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index dac7939c35..9abc37036e 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -283,6 +283,7 @@ void pretty_fn::set_options_core(options const & _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_proofs_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); @@ -298,6 +299,7 @@ void pretty_fn::set_options_core(options const & _o) { m_max_depth = get_pp_max_depth(o); m_max_steps = get_pp_max_steps(o); m_implict = get_pp_implicit(o); + m_proofs = get_pp_proofs(o); m_unicode = get_pp_unicode(o); m_coercion = get_pp_coercions(o); m_notation = get_pp_notation(o); @@ -329,6 +331,25 @@ format pretty_fn::pp_level(level const & l) { return ::lean::pp(l, m_unicode, m_indent); } +// Returns the theorem type if `f` has a Pi type with binding domain a Prop, +// and `m_proofs` is set to false. +optional pretty_fn::arg_is_proof(expr const & f) { + if (m_proofs) + return none_expr(); // showing proof terms + if (!closed(f)) + // the Lean type checker assumes expressions are closed. + return none_expr(); + try { + expr t = m_ctx.relaxed_whnf(m_ctx.infer(f)); + if (is_pi(t) && is_prop(binding_domain(t))) + return some_expr(binding_domain(t)); + else + return none_expr(); + } catch (exception &) { + return none_expr(); + } +} + bool pretty_fn::is_implicit(expr const & f) { // Remark: we assume preterms do not have implicit arguments, // since they have not been elaborated yet. @@ -533,6 +554,8 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul return pp_abbreviation(e, *it, true, bp, ignore_hide); } else if (is_implicit(f)) { return pp_child(f, bp, ignore_hide); + } else if (auto thm = arg_is_proof(f)) { + return pp_child_core(mk_app(f, mk_inaccessible(*thm)), bp, ignore_hide); } else if (!m_coercion && is_coercion(m_env, f)) { return pp_coercion(e, bp, ignore_hide); } diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index b988220aea..4e9c868b03 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -55,6 +55,7 @@ private: unsigned m_max_depth; unsigned m_max_steps; bool m_implict; //!< if true show implicit arguments + bool m_proofs; //!< if true show proof terms bool m_unicode; //!< if true use unicode chars bool m_coercion; //!< if true show coercions bool m_num_nat_coe; //!< truen when !m_coercion && env has coercion from num -> nat @@ -80,6 +81,7 @@ private: level purify(level const & l); expr purify(expr const & e); bool is_implicit(expr const & f); + optional arg_is_proof(expr const & f); bool is_prop(expr const & e); bool has_implicit_args(expr const & f); optional is_aliased(name const & n) const; diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 606aa3b733..4fb2d90b30 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -23,6 +23,10 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_IMPLICIT false #endif +#ifndef LEAN_DEFAULT_PP_PROOFS +#define LEAN_DEFAULT_PP_PROOFS true +#endif + #ifndef LEAN_DEFAULT_PP_COERCIONS #define LEAN_DEFAULT_PP_COERCIONS false #endif @@ -101,6 +105,7 @@ static name * g_pp_max_depth = nullptr; static name * g_pp_max_steps = nullptr; static name * g_pp_notation = nullptr; static name * g_pp_implicit = nullptr; +static name * g_pp_proofs = nullptr; static name * g_pp_coercions = nullptr; static name * g_pp_universes = nullptr; static name * g_pp_full_names = nullptr; @@ -126,6 +131,7 @@ void initialize_pp_options() { g_pp_max_steps = new name{"pp", "max_steps"}; g_pp_notation = new name{"pp", "notation"}; g_pp_implicit = new name{"pp", "implicit"}; + g_pp_proofs = new name{"pp", "proofs"}; g_pp_coercions = new name{"pp", "coercions"}; g_pp_universes = new name{"pp", "universes"}; g_pp_full_names = new name{"pp", "full_names"}; @@ -153,6 +159,8 @@ void initialize_pp_options() { "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"); register_bool_option(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, "(pretty printer) display implicit parameters"); + register_bool_option(*g_pp_proofs, LEAN_DEFAULT_PP_PROOFS, + "(pretty printer) display proof terms"); register_bool_option(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS, "(pretty printer) display coercionss"); register_bool_option(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES, @@ -190,17 +198,18 @@ void initialize_pp_options() { register_bool_option(*g_pp_lazy_abstraction, LEAN_DEFAULT_PP_LAZY_ABSTRACTION, "(pretty printer) display lazy-abstraction macros (for debugging purposes)"); register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL, - "(pretty printer) display coercions, implicit parameters, fully qualified names, universes, " + "(pretty printer) display coercions, implicit parameters, proof terms, 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); + options proofs_true(*g_pp_proofs, true); options coercions_true(*g_pp_coercions, true); options notation_false(*g_pp_notation, false); options binder_types_true(*g_pp_binder_types, true); options implicit_coercions = join(coercions_true, implicit_true); options implicit_notation = join(notation_false, implicit_true); - options all = universes_true + implicit_true + coercions_true + notation_false + full_names_true + binder_types_true; + options all = universes_true + implicit_true + proofs_true + coercions_true + notation_false + full_names_true + binder_types_true; g_distinguishing_pp_options = new list({implicit_true, full_names_true, coercions_true, implicit_coercions, implicit_notation, universes_true, all}); } @@ -214,6 +223,7 @@ void finalize_pp_options() { delete g_pp_max_steps; delete g_pp_notation; delete g_pp_implicit; + delete g_pp_proofs; delete g_pp_coercions; delete g_pp_universes; delete g_pp_full_names; @@ -232,6 +242,7 @@ void finalize_pp_options() { } name const & get_pp_implicit_name() { return *g_pp_implicit; } +name const & get_pp_proofs_name() { return *g_pp_proofs; } 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; } @@ -250,6 +261,7 @@ unsigned get_pp_max_depth(options const & opts) { return opts.get_unsign unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } bool get_pp_notation(options const & opts) { return opts.get_bool(*g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } bool get_pp_implicit(options const & opts) { return opts.get_bool(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } +bool get_pp_proofs(options const & opts) { return opts.get_bool(*g_pp_proofs, LEAN_DEFAULT_PP_PROOFS); } bool get_pp_coercions(options const & opts) { return opts.get_bool(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); } bool get_pp_universes(options const & opts) { return opts.get_bool(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); } bool get_pp_full_names(options const & opts) { return opts.get_bool(*g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index ffd81096f0..7247e3cb74 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/sexpr/options.h" namespace lean { name const & get_pp_implicit_name(); +name const & get_pp_proofs_name(); name const & get_pp_coercions_name(); name const & get_pp_full_names_name(); name const & get_pp_universes_name(); @@ -26,6 +27,7 @@ unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_steps(options const & opts); bool get_pp_notation(options const & opts); bool get_pp_implicit(options const & opts); +bool get_pp_proofs(options const & opts); bool get_pp_coercions(options const & opts); bool get_pp_universes(options const & opts); bool get_pp_full_names(options const & opts); diff --git a/tests/lean/pp_no_proofs.lean b/tests/lean/pp_no_proofs.lean new file mode 100644 index 0000000000..2953a64096 --- /dev/null +++ b/tests/lean/pp_no_proofs.lean @@ -0,0 +1,16 @@ +import data.nat +open nat + +constants (P : ∀ {t:true}, ℕ → Prop) (P0 : @P trivial 0) + (Ps : ∀ {n}, @P trivial n → @P trivial (succ n)) + (f : Π {n}, @P trivial n → ℕ) + +definition messy := f (Ps (Ps (Ps (Ps (Ps (Ps P0)))))) + +eval messy +set_option pp.proofs false +eval messy +set_option pp.implicit true +eval messy +set_option pp.proofs true +eval messy diff --git a/tests/lean/pp_no_proofs.lean.expected.out b/tests/lean/pp_no_proofs.lean.expected.out new file mode 100644 index 0000000000..cd36b3d787 --- /dev/null +++ b/tests/lean/pp_no_proofs.lean.expected.out @@ -0,0 +1,6 @@ +f (Ps (Ps (Ps (Ps (Ps (Ps P0)))))) +f ⌞P 6⌟ +@f 6 ⌞@P ⌞true⌟ 6⌟ +@f 6 + (@Ps (succ (succ (succ (succ (succ 0))))) + (@Ps (succ (succ (succ (succ 0)))) (@Ps (succ (succ (succ 0))) (@Ps (succ (succ 0)) (@Ps (succ 0) (@Ps 0 P0))))))