diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 8d37c060a..a8e9d39a6 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -162,7 +162,7 @@ name pretty_fn::mk_local_name(name const & n, name const & suggested) { } level pretty_fn::purify(level const & l) { - if (!m_universes || !has_meta(l)) + if (!m_universes || !m_purify_metavars || !has_meta(l)) return l; return replace(l, [&](level const & l) { if (!has_meta(l)) @@ -185,7 +185,7 @@ expr pretty_fn::purify(expr const & e) { return replace(e, [&](expr const & e, unsigned) { if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e))) return some_expr(e); - else if (is_metavar(e)) + else if (is_metavar(e) && m_purify_metavars) return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), mlocal_type(e))); else if (is_local(e)) return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), local_pp_name(e)), mlocal_type(e), local_info(e))); @@ -199,19 +199,20 @@ expr pretty_fn::purify(expr const & e) { } void pretty_fn::set_options_core(options const & o) { - m_options = 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_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_private_names = get_pp_private_names(o); - m_metavar_args = get_pp_metavar_args(o); - m_beta = get_pp_beta(o); + m_options = 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_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_private_names = get_pp_private_names(o); + m_metavar_args = get_pp_metavar_args(o); + m_purify_metavars = get_pp_purify_metavars(o); + m_beta = get_pp_beta(o); } void pretty_fn::set_options(options const & o) { @@ -373,7 +374,10 @@ auto pretty_fn::pp_const(expr const & e) -> result { } auto pretty_fn::pp_meta(expr const & e) -> result { - return result(compose(format("?"), format(mlocal_name(e)))); + if (m_purify_metavars) + return result(compose(format("?"), format(mlocal_name(e)))); + else + return result(compose(format("?M."), format(mlocal_name(e)))); } auto pretty_fn::pp_local(expr const & e) -> result { diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 2b0d57fad..0441cbe5a 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -61,6 +61,7 @@ private: bool m_full_names; bool m_private_names; bool m_metavar_args; + bool m_purify_metavars; bool m_beta; name mk_metavar_name(name const & m); diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index 856cdd9ea..94c9c92af 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -43,34 +43,40 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_METAVAR_ARGS false #endif +#ifndef LEAN_DEFAULT_PP_PURIFY_METAVARS +#define LEAN_DEFAULT_PP_PURIFY_METAVARS true +#endif + #ifndef LEAN_DEFAULT_PP_BETA #define LEAN_DEFAULT_PP_BETA false #endif namespace lean { -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_coercions = nullptr; -static name * g_pp_universes = nullptr; -static name * g_pp_full_names = nullptr; -static name * g_pp_private_names = nullptr; -static name * g_pp_metavar_args = nullptr; -static name * g_pp_beta = nullptr; +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_coercions = nullptr; +static name * g_pp_universes = nullptr; +static name * g_pp_full_names = nullptr; +static name * g_pp_private_names = nullptr; +static name * g_pp_metavar_args = nullptr; +static name * g_pp_purify_metavars = nullptr; +static name * g_pp_beta = nullptr; static list * g_distinguishing_pp_options = nullptr; void initialize_pp_options() { - g_pp_max_depth = new name{"pp", "max_depth"}; - 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_coercions = new name{"pp", "coercions"}; - g_pp_universes = new name{"pp", "universes"}; - g_pp_full_names = new name{"pp", "full_names"}; - g_pp_private_names = new name{"pp", "private_names"}; - g_pp_metavar_args = new name{"pp", "metavar_args"}; - g_pp_beta = new name{"pp", "beta"}; + g_pp_max_depth = new name{"pp", "max_depth"}; + 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_coercions = new name{"pp", "coercions"}; + g_pp_universes = new name{"pp", "universes"}; + g_pp_full_names = new name{"pp", "full_names"}; + g_pp_private_names = new name{"pp", "private_names"}; + g_pp_metavar_args = new name{"pp", "metavar_args"}; + g_pp_purify_metavars = new name{"pp", "purify_metavars"}; + g_pp_beta = new name{"pp", "beta"}; 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, @@ -89,6 +95,9 @@ void initialize_pp_options() { "(pretty printer) display internal names assigned to private declarations"); register_bool_option(*g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS, "(pretty printer) display metavariable arguments"); + register_bool_option(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS, + "(pretty printer) rename internal metavariable names (with \"user-friendly\" ones) " + "before pretty printing"); register_bool_option(*g_pp_beta, LEAN_DEFAULT_PP_BETA, "(pretty printer) apply beta-reduction when pretty printing"); @@ -114,6 +123,7 @@ void finalize_pp_options() { delete g_pp_full_names; delete g_pp_private_names; delete g_pp_metavar_args; + delete g_pp_purify_metavars; delete g_pp_beta; delete g_distinguishing_pp_options; } @@ -123,16 +133,18 @@ name const & get_pp_full_names_option_name() { return *g_pp_full_names; } name const & get_pp_universes_option_name() { return *g_pp_universes; } name const & get_pp_notation_option_name() { return *g_pp_notation; } name const & get_pp_metavar_args_name() { return *g_pp_metavar_args; } +name const & get_pp_purify_metavars_name() { return *g_pp_purify_metavars; } -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); } -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_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); } -bool get_pp_private_names(options const & opts) { return opts.get_bool(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); } -bool get_pp_metavar_args(options const & opts) { return opts.get_bool(*g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); } -bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); } +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); } +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_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); } +bool get_pp_private_names(options const & opts) { return opts.get_bool(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); } +bool get_pp_metavar_args(options const & opts) { return opts.get_bool(*g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); } +bool get_pp_purify_metavars(options const & opts) { return opts.get_bool(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS); } +bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); } list const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; } } diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h index 141f4cffe..ea353c534 100644 --- a/src/frontends/lean/pp_options.h +++ b/src/frontends/lean/pp_options.h @@ -12,6 +12,7 @@ name const & get_pp_full_names_option_name(); name const & get_pp_universes_option_name(); name const & get_pp_notation_option_name(); name const & get_pp_metavar_args_name(); +name const & get_pp_purify_metavars_name(); unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_steps(options const & opts); @@ -23,6 +24,7 @@ bool get_pp_full_names(options const & opts); bool get_pp_private_names(options const & opts); bool get_pp_metavar_args(options const & opts); bool get_pp_beta(options const & opts); +bool get_pp_purify_metavars(options const & opts); list const & get_distinguishing_pp_options(); void initialize_pp_options();