diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index beb8947d9..da52bc4bb 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -133,6 +133,7 @@ static bool print_parse_table(parser & p, parse_table const & t, bool nud, buffe 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(get_pp_preterm_name(), true); ios.set_options(os); optional tt(get_token_table(p.env())); t.for_each([&](unsigned num, notation::transition const * ts, list const & overloads) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 8fdff1ea0..6ecd1bb50 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -286,6 +286,7 @@ void pretty_fn::set_options_core(options const & o) { m_numerals = get_pp_numerals(o); m_abbreviations = 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); m_num_nat_coe = m_numerals && !m_coercion && has_coercion_num_nat(m_env); } @@ -301,7 +302,11 @@ format pretty_fn::pp_level(level const & l) { } bool pretty_fn::is_implicit(expr const & f) { - if (m_implict) + // Remark: we assume preterms do not have implicit arguments, + // since they have not been elaborated yet. + // Moreover, the type checker will probably produce an error + // when trying to infer type information + if (m_implict || m_preterm) return false; // showing implicit arguments if (!closed(f)) { // the Lean type checker assumes expressions are closed. @@ -505,8 +510,10 @@ auto pretty_fn::pp_local(expr const & e) -> result { } bool pretty_fn::has_implicit_args(expr const & f) { - if (!closed(f)) { - // the Lean type checker assumes expressions are closed. + if (!closed(f) || m_preterm) { + // The Lean type checker assumes expressions are closed. + // If preterms are being processed, then we assume + // there are no implicit arguments. return false; } name_generator ngen(*g_tmp_prefix); diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 1da5b0f9f..8e8cac130 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -69,6 +69,7 @@ private: bool m_abbreviations; bool m_hide_full_terms; bool m_extra_spaces; + bool m_preterm; name mk_metavar_name(name const & m); name mk_local_name(name const & n, name const & suggested); diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 7921dc036..89966c1fd 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -67,6 +67,10 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_EXTRA_SPACES false #endif +#ifndef LEAN_DEFAULT_PP_PRETERM +#define LEAN_DEFAULT_PP_PRETERM false +#endif + namespace lean { static name * g_pp_max_depth = nullptr; static name * g_pp_max_steps = nullptr; @@ -83,6 +87,7 @@ static name * g_pp_beta = nullptr; static name * g_pp_numerals = nullptr; static name * g_pp_abbreviations = nullptr; static name * g_pp_extra_spaces = nullptr; +static name * g_pp_preterm = nullptr; static list * g_distinguishing_pp_options = nullptr; void initialize_pp_options() { @@ -101,6 +106,7 @@ void initialize_pp_options() { g_pp_numerals = new name{"pp", "numerals"}; g_pp_abbreviations = new name{"pp", "abbreviations"}; g_pp_extra_spaces = new name{"pp", "extra_spaces"}; + g_pp_preterm = new name{"pp", "preterm"}; 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, @@ -133,6 +139,8 @@ void initialize_pp_options() { "(pretty printer) display abbreviations (i.e., revert abbreviation expansion when pretty printing)"); register_bool_option(*g_pp_extra_spaces, LEAN_DEFAULT_PP_EXTRA_SPACES, "(pretty printer) add space after prefix operators and before postfix ones"); + register_bool_option(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM, + "(pretty printer) assume the term is a preterm (i.e., a term before elaboration)"); options universes_true(*g_pp_universes, true); options full_names_true(*g_pp_full_names, true); @@ -147,6 +155,7 @@ void initialize_pp_options() { } void finalize_pp_options() { + delete g_pp_preterm; delete g_pp_extra_spaces; delete g_pp_abbreviations; delete g_pp_numerals; @@ -174,6 +183,7 @@ 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; } 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); } @@ -190,5 +200,6 @@ bool get_pp_beta(options const & opts) { return opts.get_bool(*g_ bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS); } 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); } 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 567a9cb87..53bd083d9 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -16,6 +16,7 @@ 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(); unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_steps(options const & opts); @@ -32,6 +33,7 @@ bool get_pp_purify_locals(options const & opts); bool get_pp_numerals(options const & opts); bool get_pp_abbreviations(options const & opts); bool get_pp_extra_spaces(options const & opts); +bool get_pp_preterm(options const & opts); list const & get_distinguishing_pp_options(); void initialize_pp_options(); diff --git a/tests/lean/604.lean b/tests/lean/604.lean new file mode 100644 index 000000000..b5bf0006a --- /dev/null +++ b/tests/lean/604.lean @@ -0,0 +1 @@ +print notation dec_trivial diff --git a/tests/lean/604.lean.expected.out b/tests/lean/604.lean.expected.out new file mode 100644 index 000000000..f1d8cd500 --- /dev/null +++ b/tests/lean/604.lean.expected.out @@ -0,0 +1 @@ +`dec_trivial`:1024 := of_is_true trivial