1961 lines
70 KiB
C++
Executable file
1961 lines
70 KiB
C++
Executable file
/*
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include <utility>
|
|
#include <algorithm>
|
|
#include <limits>
|
|
#include <string>
|
|
#include <util/utf8.h>
|
|
#include "library/sorry.h"
|
|
#include "util/flet.h"
|
|
#include "util/fresh_name.h"
|
|
#include "kernel/replace_fn.h"
|
|
#include "kernel/free_vars.h"
|
|
#include "kernel/abstract.h"
|
|
#include "kernel/instantiate.h"
|
|
#include "library/annotation.h"
|
|
#include "library/aliases.h"
|
|
#include "library/class.h"
|
|
#include "library/scoped_ext.h"
|
|
#include "library/expr_pair.h"
|
|
#include "library/placeholder.h"
|
|
#include "library/private.h"
|
|
#include "library/protected.h"
|
|
#include "library/quote.h"
|
|
#include "library/explicit.h"
|
|
#include "library/typed_expr.h"
|
|
#include "library/num.h"
|
|
#include "library/util.h"
|
|
#include "library/print.h"
|
|
#include "library/pp_options.h"
|
|
#include "library/delayed_abstraction.h"
|
|
#include "library/constants.h"
|
|
#include "library/replace_visitor.h"
|
|
#include "library/string.h"
|
|
#include "library/type_context.h"
|
|
#include "library/idx_metavar.h"
|
|
#include "library/equations_compiler/equations.h"
|
|
#include "library/tactic/tactic_state.h"
|
|
#include "library/tactic/smt/hinst_lemmas.h"
|
|
#include "library/compiler/comp_irrelevant.h"
|
|
#include "library/compiler/erase_irrelevant.h"
|
|
#include "library/compiler/rec_fn_macro.h"
|
|
#include "frontends/lean/pp.h"
|
|
#include "frontends/lean/util.h"
|
|
#include "frontends/lean/prenum.h"
|
|
#include "frontends/lean/token_table.h"
|
|
#include "frontends/lean/builtin_exprs.h"
|
|
#include "frontends/lean/structure_cmd.h"
|
|
#include "frontends/lean/parser_config.h"
|
|
#include "frontends/lean/scanner.h"
|
|
#include "frontends/lean/tokens.h"
|
|
|
|
#include "library/trace.h"
|
|
|
|
namespace lean {
|
|
static format * g_ellipsis_n_fmt = nullptr;
|
|
static format * g_ellipsis_fmt = nullptr;
|
|
static format * g_placeholder_fmt = nullptr;
|
|
static format * g_lambda_n_fmt = nullptr;
|
|
static format * g_lambda_fmt = nullptr;
|
|
static format * g_forall_n_fmt = nullptr;
|
|
static format * g_forall_fmt = nullptr;
|
|
static format * g_pi_n_fmt = nullptr;
|
|
static format * g_pi_fmt = nullptr;
|
|
static format * g_arrow_n_fmt = nullptr;
|
|
static format * g_arrow_fmt = nullptr;
|
|
static format * g_let_fmt = nullptr;
|
|
static format * g_in_fmt = nullptr;
|
|
static format * g_assign_fmt = nullptr;
|
|
static format * g_have_fmt = nullptr;
|
|
static format * g_from_fmt = nullptr;
|
|
static format * g_visible_fmt = nullptr;
|
|
static format * g_show_fmt = nullptr;
|
|
static format * g_explicit_fmt = nullptr;
|
|
static format * g_partial_explicit_fmt = nullptr;
|
|
static name * g_tmp_prefix = nullptr;
|
|
|
|
class nat_numeral_pp {
|
|
name m_nat;
|
|
expr m_nat_zero;
|
|
expr m_nat_succ;
|
|
public:
|
|
nat_numeral_pp():
|
|
m_nat(get_nat_name()),
|
|
m_nat_zero(mk_constant(get_nat_zero_name())),
|
|
m_nat_succ(mk_constant(get_nat_succ_name())) {
|
|
}
|
|
|
|
// Return an unsigned if \c e if of the form (succ^k zero), and k
|
|
// fits in a machine unsigned integer.
|
|
optional<unsigned> to_unsigned(expr const & e) const {
|
|
unsigned r = 0;
|
|
expr const * it = &e;
|
|
while (true) {
|
|
if (*it == m_nat_zero) {
|
|
return optional<unsigned>(r);
|
|
} else if (is_app(*it) && app_fn(*it) == m_nat_succ) {
|
|
if (r == std::numeric_limits<unsigned>::max())
|
|
return optional<unsigned>(); // just in case, it does not really happen in practice
|
|
r++;
|
|
it = &app_arg(*it);
|
|
} else if (is_zero(get_app_fn(*it))) {
|
|
return optional<unsigned>(r);
|
|
} else {
|
|
return optional<unsigned>();
|
|
}
|
|
}
|
|
}
|
|
};
|
|
|
|
static nat_numeral_pp * g_nat_numeral_pp = nullptr;
|
|
|
|
static optional<unsigned> to_unsigned(expr const & e) {
|
|
return g_nat_numeral_pp->to_unsigned(e);
|
|
}
|
|
|
|
static name * g_pp_using_anonymous_constructor = nullptr;
|
|
|
|
bool pp_using_anonymous_constructor(environment const & env, name const & n) {
|
|
return has_attribute(env, *g_pp_using_anonymous_constructor, n);
|
|
}
|
|
|
|
void initialize_pp() {
|
|
g_ellipsis_n_fmt = new format(highlight(format("\u2026")));
|
|
g_ellipsis_fmt = new format(highlight(format("...")));
|
|
g_placeholder_fmt = new format(highlight(format("_")));
|
|
g_lambda_n_fmt = new format(highlight_keyword(format("\xCE\xBB"))); //\u03BB
|
|
g_lambda_fmt = new format(highlight_keyword(format("fun")));
|
|
g_forall_n_fmt = new format(highlight_keyword(format("\xE2\x88\x80"))); //\u2200
|
|
g_forall_fmt = new format(highlight_keyword(format("forall")));
|
|
g_pi_n_fmt = new format(highlight_keyword(format("Π")));
|
|
g_pi_fmt = new format(highlight_keyword(format("Pi")));
|
|
g_arrow_n_fmt = new format(highlight_keyword(format("\xE2\x86\x92"))); //\u2192
|
|
g_arrow_fmt = new format(highlight_keyword(format("->")));
|
|
g_let_fmt = new format(highlight_keyword(format("let")));
|
|
g_in_fmt = new format(highlight_keyword(format("in")));
|
|
g_assign_fmt = new format(highlight_keyword(format(":=")));
|
|
g_have_fmt = new format(highlight_keyword(format("have")));
|
|
g_from_fmt = new format(highlight_keyword(format("from")));
|
|
g_visible_fmt = new format(highlight_keyword(format("[visible]")));
|
|
g_show_fmt = new format(highlight_keyword(format("show")));
|
|
g_explicit_fmt = new format(highlight_keyword(format("@")));
|
|
g_partial_explicit_fmt = new format(highlight_keyword(format("@@")));
|
|
g_tmp_prefix = new name(name::mk_internal_unique_name());
|
|
g_nat_numeral_pp = new nat_numeral_pp();
|
|
|
|
g_pp_using_anonymous_constructor = new name("pp_using_anonymous_constructor");
|
|
|
|
register_system_attribute(basic_attribute::with_check(
|
|
*g_pp_using_anonymous_constructor,
|
|
"if a structure S is marked with this attribute, then its constructor applications"
|
|
"are pretty printed using the anonymous constructor",
|
|
[](environment const & env, name const & d, bool) -> void {
|
|
if (!is_structure(env, d))
|
|
throw exception(
|
|
"invalid 'pp_using_anonymous_constructor' use, "
|
|
"only structures can be marked with this attribute");
|
|
}));
|
|
}
|
|
|
|
void finalize_pp() {
|
|
delete g_pp_using_anonymous_constructor;
|
|
delete g_nat_numeral_pp;
|
|
delete g_ellipsis_n_fmt;
|
|
delete g_ellipsis_fmt;
|
|
delete g_placeholder_fmt;
|
|
delete g_lambda_n_fmt;
|
|
delete g_lambda_fmt;
|
|
delete g_forall_n_fmt;
|
|
delete g_forall_fmt;
|
|
delete g_pi_n_fmt;
|
|
delete g_pi_fmt;
|
|
delete g_arrow_n_fmt;
|
|
delete g_arrow_fmt;
|
|
delete g_let_fmt;
|
|
delete g_in_fmt;
|
|
delete g_assign_fmt;
|
|
delete g_have_fmt;
|
|
delete g_from_fmt;
|
|
delete g_visible_fmt;
|
|
delete g_show_fmt;
|
|
delete g_partial_explicit_fmt;
|
|
delete g_explicit_fmt;
|
|
delete g_tmp_prefix;
|
|
}
|
|
|
|
/** \brief We assume a metavariable name has a suggestion embedded in it WHEN its
|
|
last component is a string. */
|
|
static bool has_embedded_suggestion(name const & m) {
|
|
return m.is_string();
|
|
}
|
|
|
|
/** \see extract_suggestion */
|
|
static name extract_suggestion_core(name const & m) {
|
|
if (m.is_string()) {
|
|
if (m.is_atomic())
|
|
return m;
|
|
else
|
|
return name(extract_suggestion_core(m.get_prefix()), m.get_string());
|
|
} else {
|
|
return name();
|
|
}
|
|
}
|
|
|
|
/** \brief Extract "suggested name" embedded in a metavariable name
|
|
|
|
\pre has_embedded_suggestion(m)
|
|
*/
|
|
static name extract_suggestion(name const & m) {
|
|
lean_assert(has_embedded_suggestion(m));
|
|
name r = extract_suggestion_core(m);
|
|
lean_assert(!r.is_anonymous());
|
|
return r;
|
|
}
|
|
|
|
name pretty_fn::mk_metavar_name(name const & m, optional<name> const & prefix) {
|
|
if (auto it = m_purify_meta_table.find(m))
|
|
return *it;
|
|
if (has_embedded_suggestion(m)) {
|
|
name suggested = extract_suggestion(m);
|
|
name r = suggested;
|
|
unsigned i = 1;
|
|
while (m_purify_used_metas.contains(r)) {
|
|
r = suggested.append_after(i);
|
|
i++;
|
|
}
|
|
m_purify_used_metas.insert(r);
|
|
m_purify_meta_table.insert(m, r);
|
|
return r;
|
|
} else {
|
|
name new_m;
|
|
if (prefix)
|
|
new_m = prefix->append_after(m_next_meta_idx);
|
|
else
|
|
new_m = m_meta_prefix.append_after(m_next_meta_idx);
|
|
m_next_meta_idx++;
|
|
m_purify_meta_table.insert(m, new_m);
|
|
return new_m;
|
|
}
|
|
}
|
|
|
|
name pretty_fn::mk_local_name(name const & n, name const & suggested) {
|
|
if (!m_purify_locals)
|
|
return suggested;
|
|
if (auto it = m_purify_local_table.find(n))
|
|
return *it;
|
|
unsigned i = 1;
|
|
name r = suggested;
|
|
while (m_purify_used_locals.contains(r)) {
|
|
r = suggested.append_after(i);
|
|
i++;
|
|
}
|
|
m_purify_used_locals.insert(r);
|
|
m_purify_local_table.insert(n, r);
|
|
return r;
|
|
}
|
|
|
|
level pretty_fn::purify(level const & l) {
|
|
if (!m_universes || !m_purify_metavars || !has_meta(l))
|
|
return l;
|
|
return replace(l, [&](level const & l) {
|
|
if (!has_meta(l))
|
|
return some_level(l);
|
|
if (is_metavar_decl_ref(l))
|
|
return some_level(mk_meta_univ(mk_metavar_name(meta_id(l), "l")));
|
|
if (is_meta(l) && !is_idx_metauniv(l))
|
|
return some_level(mk_meta_univ(mk_metavar_name(meta_id(l))));
|
|
return none_level();
|
|
});
|
|
}
|
|
|
|
expr pretty_fn::infer_type(expr const & e) {
|
|
try {
|
|
return m_ctx.infer(e);
|
|
} catch (exception &) {
|
|
expr dummy = mk_Prop();
|
|
return dummy;
|
|
}
|
|
}
|
|
|
|
/** \brief Make sure that all metavariables have reasonable names,
|
|
and for all local constants l1 l2, mlocal_pp_name(l1) != mlocal_pp_name(l2).
|
|
|
|
\remark pretty_fn will create new local constants when pretty printing,
|
|
but it will make sure that the new constants will not produce collisions.
|
|
|
|
\remark We do not purify metavariable names IF the user provided them.
|
|
We use the test (mlocal_name(e) == mlocal_pp_name(e)) to decide whether
|
|
the user provided the name or not.
|
|
*/
|
|
expr pretty_fn::purify(expr const & e) {
|
|
if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e)))
|
|
return 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 (m_purify_metavars && is_metavar_decl_ref(e) && mlocal_name(e) == mlocal_pp_name(e)) {
|
|
return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e), "m"), infer_type(e)));
|
|
} else if (m_purify_metavars && is_metavar(e) && mlocal_name(e) == mlocal_pp_name(e) && !is_idx_metavar(e)) {
|
|
return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), infer_type(e)));
|
|
} else if (is_local(e)) {
|
|
return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), mlocal_pp_name(e)),
|
|
infer_type(e), local_info(e)));
|
|
} else if (is_constant(e)) {
|
|
return some_expr(update_constant(e, map(const_levels(e), [&](level const & l) { return purify(l); })));
|
|
} else if (is_sort(e)) {
|
|
return some_expr(update_sort(e, purify(sort_level(e))));
|
|
} else {
|
|
return none_expr();
|
|
}
|
|
});
|
|
}
|
|
|
|
void pretty_fn::set_options_core(options const & _o) {
|
|
options o = _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);
|
|
o = o.update_if_undef(get_pp_full_names_name(), true);
|
|
o = o.update_if_undef(get_pp_beta_name(), false);
|
|
o = o.update_if_undef(get_pp_numerals_name(), false);
|
|
o = o.update_if_undef(get_pp_strings_name(), false);
|
|
o = o.update_if_undef(get_pp_binder_types_name(), true);
|
|
}
|
|
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_proofs = get_pp_proofs(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_purify_metavars = get_pp_purify_metavars(o);
|
|
m_purify_locals = get_pp_purify_locals(o);
|
|
m_locals_full_names = get_pp_locals_full_names(o);
|
|
m_beta = get_pp_beta(o);
|
|
m_numerals = get_pp_numerals(o);
|
|
m_strings = get_pp_strings(o);
|
|
m_preterm = get_pp_preterm(o);
|
|
m_binder_types = get_pp_binder_types(o);
|
|
m_hide_comp_irrel = get_pp_hide_comp_irrel(o);
|
|
m_delayed_abstraction = get_pp_delayed_abstraction(o);
|
|
m_use_holes = get_pp_use_holes(o);
|
|
m_annotations = get_pp_annotations(o);
|
|
m_hide_full_terms = get_formatter_hide_full_terms(o);
|
|
m_num_nat_coe = m_numerals;
|
|
m_structure_instances = get_pp_structure_instances(o);
|
|
m_structure_instances_qualifier = get_pp_structure_instances_qualifier(o);
|
|
m_structure_projections = get_pp_structure_projections(o);
|
|
}
|
|
|
|
void pretty_fn::set_options(options const & o) {
|
|
if (is_eqp(o, m_options))
|
|
return;
|
|
set_options_core(o);
|
|
}
|
|
|
|
format pretty_fn::pp_child(level const & l) {
|
|
if (is_explicit(l) || is_param(l) || is_meta(l)) {
|
|
return pp_level(l);
|
|
} else {
|
|
return paren(pp_level(l));
|
|
}
|
|
}
|
|
|
|
format pretty_fn::pp_max(level l) {
|
|
lean_assert(is_max(l) || is_imax(l));
|
|
format r = format(is_max(l) ? "max" : "imax");
|
|
level lhs = is_max(l) ? max_lhs(l) : imax_lhs(l);
|
|
level rhs = is_max(l) ? max_rhs(l) : imax_rhs(l);
|
|
r += nest(m_indent, compose(line(), pp_child(lhs)));
|
|
while (kind(rhs) == kind(l)) {
|
|
l = rhs;
|
|
lhs = is_max(l) ? max_lhs(l) : imax_lhs(l);
|
|
rhs = is_max(l) ? max_rhs(l) : imax_rhs(l);
|
|
r += nest(m_indent, compose(line(), pp_child(lhs)));
|
|
}
|
|
r += nest(m_indent, compose(line(), pp_child(rhs)));
|
|
return group(r);
|
|
}
|
|
|
|
format pretty_fn::pp_meta(level const & l) {
|
|
if (m_universes) {
|
|
if (is_idx_metauniv(l)) {
|
|
return format((sstream() << "?u_" << to_meta_idx(l)).str());
|
|
} else if (is_metavar_decl_ref(l)) {
|
|
return format((sstream() << "?l_" << get_metavar_decl_ref_suffix(l)).str());
|
|
} else {
|
|
return compose(format("?"), format(meta_id(l)));
|
|
}
|
|
} else {
|
|
return format("?");
|
|
}
|
|
}
|
|
|
|
format pretty_fn::pp_level(level const & l) {
|
|
if (is_explicit(l)) {
|
|
lean_assert(get_depth(l) > 0);
|
|
return format(get_depth(l) - 1);
|
|
} else {
|
|
switch (kind(l)) {
|
|
case level_kind::Zero:
|
|
lean_unreachable(); // LCOV_EXCL_LINE
|
|
case level_kind::Param:
|
|
return format(param_id(l));
|
|
case level_kind::Meta:
|
|
return pp_meta(l);
|
|
case level_kind::Succ: {
|
|
auto p = to_offset(l);
|
|
return pp_child(p.first) + format("+") + format(p.second);
|
|
}
|
|
case level_kind::Max: case level_kind::IMax:
|
|
return pp_max(l);
|
|
}
|
|
lean_unreachable(); // LCOV_EXCL_LINE
|
|
}
|
|
}
|
|
|
|
bool pretty_fn::is_implicit(expr const & f) {
|
|
// 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.
|
|
return false;
|
|
}
|
|
try {
|
|
expr t = m_ctx.relaxed_whnf(m_ctx.infer(f));
|
|
if (is_pi(t)) {
|
|
binder_info bi = binding_info(t);
|
|
return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit();
|
|
} else {
|
|
return false;
|
|
}
|
|
} catch (exception &) {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
bool pretty_fn::is_default_arg_app(expr const & e) {
|
|
if (m_implict || m_preterm)
|
|
return false; // showing default arguments
|
|
if (!closed(app_fn(e))) {
|
|
// the Lean type checker assumes expressions are closed.
|
|
return false;
|
|
}
|
|
try {
|
|
expr t = m_ctx.relaxed_whnf(m_ctx.infer(app_fn(e)));
|
|
if (is_pi(t)) {
|
|
expr arg_type = binding_domain(t);
|
|
t = binding_body(t);
|
|
if (!is_pi(t) && !is_var(t) && is_app_of(arg_type, get_opt_param_name(), 2)) {
|
|
expr defval = app_arg(arg_type);
|
|
return closed(defval) && defval == app_arg(e);
|
|
}
|
|
}
|
|
} catch (exception &) { }
|
|
return false;
|
|
}
|
|
|
|
bool pretty_fn::is_prop(expr const & e) {
|
|
try {
|
|
expr t = m_ctx.relaxed_whnf(m_ctx.infer(e));
|
|
return t == mk_Prop();
|
|
} catch (exception &) {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::add_paren_if_needed(result const & r, unsigned bp) -> result {
|
|
if (r.rbp() < bp) {
|
|
return result(paren(r.fmt()));
|
|
} else {
|
|
return r;
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) -> result {
|
|
return add_paren_if_needed(pp(e, ignore_hide), bp);
|
|
}
|
|
|
|
static expr consume_ref_annotations(expr const & e) {
|
|
if (is_explicit(e))
|
|
return consume_ref_annotations(get_explicit_arg(e));
|
|
else
|
|
return e;
|
|
}
|
|
|
|
enum local_ref_kind { LocalRef, OverridenLocalRef, NotLocalRef };
|
|
|
|
static local_ref_kind check_local_ref(environment const & env, expr const & e, unsigned & num_ref_univ_params) {
|
|
expr const & rfn = get_app_fn(e);
|
|
if (!is_constant(rfn))
|
|
return NotLocalRef;
|
|
auto ref = get_local_ref(env, const_name(rfn));
|
|
if (!ref)
|
|
return NotLocalRef;
|
|
if (is_as_atomic(*ref))
|
|
ref = get_as_atomic_arg(*ref);
|
|
buffer<expr> ref_args, e_args;
|
|
expr ref_fn = consume_ref_annotations(get_app_args(*ref, ref_args));
|
|
get_app_args(e, e_args);
|
|
if (!is_constant(ref_fn) || e_args.size() != ref_args.size()) {
|
|
return NotLocalRef;
|
|
}
|
|
for (unsigned i = 0; i < e_args.size(); i++) {
|
|
expr e_arg = e_args[i];
|
|
expr ref_arg = consume_ref_annotations(ref_args[i]);
|
|
if (!is_local(e_arg) || !is_local(ref_arg) || mlocal_pp_name(e_arg) != mlocal_pp_name(ref_arg))
|
|
return OverridenLocalRef;
|
|
}
|
|
num_ref_univ_params = length(const_levels(ref_fn));
|
|
buffer<level> lvls;
|
|
to_buffer(const_levels(rfn), lvls);
|
|
if (lvls.size() < num_ref_univ_params) {
|
|
return NotLocalRef;
|
|
}
|
|
for (unsigned i = 0; i < num_ref_univ_params; i++) {
|
|
level const & l = lvls[i];
|
|
if (!is_param(l)) {
|
|
return OverridenLocalRef;
|
|
}
|
|
for (unsigned j = 0; j < i; j++)
|
|
if (lvls[i] == lvls[j]) {
|
|
return OverridenLocalRef;
|
|
}
|
|
}
|
|
return LocalRef;
|
|
}
|
|
|
|
static bool is_local_ref(environment const & env, expr const & e) {
|
|
unsigned num_ref_univ_params;
|
|
return check_local_ref(env, e, num_ref_univ_params) == LocalRef;
|
|
}
|
|
|
|
auto pretty_fn::pp_overriden_local_ref(expr const & e) -> result {
|
|
buffer<expr> args;
|
|
expr const & fn = get_app_args(e, args);
|
|
result res_fn;
|
|
{
|
|
flet<bool> set1(m_full_names, true);
|
|
res_fn = pp_const(fn, some(0u));
|
|
}
|
|
format fn_fmt = res_fn.fmt();
|
|
if (const_name(fn).is_atomic())
|
|
fn_fmt = compose(format("_root_."), fn_fmt);
|
|
if (m_implict && has_implicit_args(fn))
|
|
fn_fmt = compose(*g_explicit_fmt, fn_fmt);
|
|
format r_fmt = fn_fmt;
|
|
expr curr_fn = fn;
|
|
for (unsigned i = 0; i < args.size(); i++) {
|
|
expr const & arg = args[i];
|
|
if (m_implict || !is_implicit(curr_fn)) {
|
|
result res_arg = pp_child(arg, max_bp());
|
|
r_fmt = group(compose(r_fmt, nest(m_indent, compose(line(), res_arg.fmt()))));
|
|
}
|
|
curr_fn = mk_app(curr_fn, arg);
|
|
}
|
|
return result(max_bp()-1, r_fmt);
|
|
}
|
|
|
|
// Return some result if \c e is of the form (c p_1 ... p_n) where
|
|
// c is a constant, and p_i's are parameters fixed in a section.
|
|
auto pretty_fn::pp_local_ref(expr const & e) -> optional<result> {
|
|
unsigned num_ref_univ_params;
|
|
switch (check_local_ref(m_env, e, num_ref_univ_params)) {
|
|
case NotLocalRef:
|
|
return optional<result>();
|
|
case LocalRef:
|
|
return some(pp_const(get_app_fn(e), optional<unsigned>(num_ref_univ_params)));
|
|
case OverridenLocalRef:
|
|
return some(pp_overriden_local_ref(e));
|
|
}
|
|
lean_unreachable();
|
|
}
|
|
|
|
static bool is_coercion(expr const & e) {
|
|
return is_app_of(e, get_coe_name()) && get_app_num_args(e) >= 4;
|
|
}
|
|
|
|
static bool is_coercion_fn(expr const & e) {
|
|
return is_app_of(e, get_coe_fn_name()) && get_app_num_args(e) >= 3;
|
|
}
|
|
|
|
auto pretty_fn::pp_hide_coercion(expr const & e, unsigned bp, bool ignore_hide) -> result {
|
|
lean_assert(is_coercion(e));
|
|
buffer<expr> args;
|
|
get_app_args(e, args);
|
|
if (args.size() == 4) {
|
|
return pp_child(args[3], bp, ignore_hide);
|
|
} else {
|
|
expr new_e = mk_app(args.size() - 3, args.data() + 3);
|
|
return pp_child(new_e, bp, ignore_hide);
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_hide) -> result {
|
|
lean_assert(is_coercion_fn(e));
|
|
buffer<expr> args;
|
|
get_app_args(e, args);
|
|
if (args.size() == 3) {
|
|
return pp_child(args[2], bp, ignore_hide);
|
|
} else {
|
|
expr new_e = mk_app(args.size() - 2, args.data() + 2);
|
|
return pp_child(new_e, bp, ignore_hide);
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result {
|
|
if (is_app(e)) {
|
|
if (auto r = pp_local_ref(e))
|
|
return add_paren_if_needed(*r, bp);
|
|
if (m_numerals) {
|
|
if (auto n = to_num(e)) return pp_num(*n, bp);
|
|
}
|
|
if (m_strings) {
|
|
if (auto r = to_string(e)) return pp_string_literal(*r);
|
|
if (auto r = to_char(m_ctx, e)) return pp_char_literal(*r);
|
|
}
|
|
expr const & f = app_fn(e);
|
|
if (is_implicit(f)) {
|
|
return pp_child(f, bp, ignore_hide);
|
|
} else if (!m_coercion && is_coercion(e)) {
|
|
return pp_hide_coercion(e, bp, ignore_hide);
|
|
} else if (!m_coercion && is_coercion_fn(e)) {
|
|
return pp_hide_coercion_fn(e, bp, ignore_hide);
|
|
}
|
|
}
|
|
return pp_child_core(e, bp, ignore_hide);
|
|
}
|
|
|
|
auto pretty_fn::pp_var(expr const & e) -> result {
|
|
unsigned vidx = var_idx(e);
|
|
return result(compose(format("#"), format(vidx)));
|
|
}
|
|
|
|
auto pretty_fn::pp_sort(expr const & e) -> result {
|
|
level u = sort_level(e);
|
|
if (u == mk_level_zero()) {
|
|
return result(format("Prop"));
|
|
} else if (u == mk_level_one()) {
|
|
return result(format("Type"));
|
|
} else if (optional<level> u1 = dec_level(u)) {
|
|
return result(max_bp()-1, group(format("Type") + space() + nest(5, pp_child(*u1))));
|
|
} else {
|
|
return result(max_bp()-1, group(format("Sort") + space() + nest(5, pp_child(u))));
|
|
}
|
|
}
|
|
|
|
optional<name> pretty_fn::is_aliased(name const & n) const {
|
|
if (auto it = is_expr_aliased(m_env, n)) {
|
|
// must check if we are not shadow by current namespace
|
|
for (name const & ns : get_namespaces(m_env)) {
|
|
if (!ns.is_anonymous() && m_env.find(ns + *it))
|
|
return optional<name>();
|
|
}
|
|
return it;
|
|
} else {
|
|
return optional<name>();
|
|
}
|
|
}
|
|
|
|
format pretty_fn::escape(name const & n) {
|
|
// also escape keyword-like names
|
|
if (n.is_atomic() && n.is_string() && find(m_token_table, n.get_string())) {
|
|
sstream ss;
|
|
ss << "«" << n.get_string() << "»";
|
|
return format(ss.str());
|
|
}
|
|
return format(n.escape());
|
|
}
|
|
|
|
auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ_params) -> result {
|
|
if (is_neutral_expr(e) && m_unicode)
|
|
return format("◾");
|
|
if (is_unreachable_expr(e) && m_unicode)
|
|
return format("⊥");
|
|
name n = const_name(e);
|
|
if (m_notation && n == get_unit_star_name())
|
|
return format("()");
|
|
if (!num_ref_univ_params) {
|
|
if (auto r = pp_local_ref(e))
|
|
return *r;
|
|
}
|
|
// Remark: if num_ref_univ_params is "some", then it contains the number of
|
|
// universe levels that are fixed in a section. That is, \c e corresponds to
|
|
// a constant in a section which has fixed levels.
|
|
auto short_n = n;
|
|
if (!m_full_names) {
|
|
if (auto it = is_aliased(n)) {
|
|
if (!m_private_names || !hidden_to_user_name(m_env, n))
|
|
short_n = *it;
|
|
} else {
|
|
for (name const & ns : get_namespaces(m_env)) {
|
|
if (!ns.is_anonymous()) {
|
|
name new_n = n.replace_prefix(ns, name());
|
|
if (new_n != n &&
|
|
!new_n.is_anonymous() &&
|
|
(!new_n.is_atomic() || !is_protected(m_env, n))) {
|
|
short_n = new_n;
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
if (!m_private_names) {
|
|
if (auto n1 = hidden_to_user_name(m_env, short_n))
|
|
short_n = *n1;
|
|
}
|
|
if (m_ctx.has_local_pp_name(short_n.get_root())) {
|
|
if (m_ctx.has_local_pp_name(n.get_root())) {
|
|
n = get_root_tk() + n;
|
|
}
|
|
} else {
|
|
n = short_n;
|
|
}
|
|
if (m_universes && !empty(const_levels(e))) {
|
|
unsigned first_idx = 0;
|
|
buffer<level> ls;
|
|
to_buffer(const_levels(e), ls);
|
|
if (num_ref_univ_params) {
|
|
if (ls.size() <= *num_ref_univ_params)
|
|
return result(escape(n));
|
|
else
|
|
first_idx = *num_ref_univ_params;
|
|
}
|
|
format r = compose(escape(n), format(".{"));
|
|
bool first = true;
|
|
for (unsigned i = first_idx; i < ls.size(); i++) {
|
|
level const & l = ls[i];
|
|
format l_fmt = pp_level(l);
|
|
if (is_max(l) || is_imax(l))
|
|
l_fmt = paren(l_fmt);
|
|
if (first)
|
|
r += nest(m_indent, l_fmt);
|
|
else
|
|
r += nest(m_indent, compose(line(), l_fmt));
|
|
first = false;
|
|
}
|
|
r += format("}");
|
|
return result(group(r));
|
|
} else {
|
|
return result(escape(n));
|
|
}
|
|
}
|
|
|
|
static format pp_hole() { return format("{! !}"); }
|
|
|
|
auto pretty_fn::pp_meta(expr const & e) -> result {
|
|
if (m_use_holes) {
|
|
return pp_hole();
|
|
} else if (mlocal_name(e) != mlocal_pp_name(e)) {
|
|
return result(format(mlocal_pp_name(e)));
|
|
} else if (is_idx_metavar(e)) {
|
|
return result(format((sstream() << "?x_" << to_meta_idx(e)).str()));
|
|
} else if (is_metavar_decl_ref(e) && !m_purify_metavars) {
|
|
return result(format((sstream() << "?m_" << get_metavar_decl_ref_suffix(e)).str()));
|
|
} else 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 {
|
|
name n = sanitize_if_fresh(mlocal_pp_name(e));
|
|
if (m_locals_full_names)
|
|
return result(format("<") + format(n + mlocal_name(e)) + format(">"));
|
|
else
|
|
return format(escape(n));
|
|
}
|
|
|
|
bool pretty_fn::has_implicit_args(expr const & f) {
|
|
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;
|
|
}
|
|
try {
|
|
expr type = m_ctx.relaxed_whnf(m_ctx.infer(f));
|
|
push_local_fn push_local(m_ctx);
|
|
while (is_pi(type)) {
|
|
binder_info bi = binding_info(type);
|
|
if (bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit())
|
|
return true;
|
|
expr local = push_local(binding_name(type), binding_domain(type), binding_info(type));
|
|
type = m_ctx.relaxed_whnf(instantiate(binding_body(type), local));
|
|
}
|
|
return false;
|
|
} catch (exception &) {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
static bool is_structure_instance(environment const & env, expr const & e, bool implicit) {
|
|
expr const & fn = get_app_fn(e);
|
|
if (!is_constant(fn)) return false;
|
|
name const & mk_name = const_name(fn);
|
|
if (!inductive::is_intro_rule(env, mk_name)) return false;
|
|
name const & S = mk_name.get_prefix();
|
|
if (!is_structure(env, S)) return false;
|
|
/* If implicit arguments is true, and the structure has parameters, we should not
|
|
pretty print using { ... }, because we will not be able to see the parameters. */
|
|
if (implicit && *inductive::get_num_params(env, S) > 0) return false;
|
|
/* check whether it is a partially applied constructor application */
|
|
if (get_app_num_args(e) != get_arity(env.get(mk_name).get_type())) return false;
|
|
return true;
|
|
}
|
|
|
|
auto pretty_fn::pp_structure_instance(expr const & e) -> result {
|
|
lean_assert(is_structure_instance(m_env, e, m_implict));
|
|
buffer<expr> args;
|
|
expr const & mk = get_app_args(e, args);
|
|
name const & S = const_name(mk).get_prefix();
|
|
unsigned num_params = *inductive::get_num_params(m_env, S);
|
|
if (pp_using_anonymous_constructor(m_env, S)) {
|
|
format r;
|
|
for (unsigned i = num_params; i < args.size(); i++) {
|
|
if (i > num_params) r += line();
|
|
format fval_fmt = pp(args[i]).fmt();
|
|
if (i < args.size() - 1) fval_fmt += comma();
|
|
r += fval_fmt;
|
|
}
|
|
r = group(nest(1, format("⟨") + r + format("⟩")));
|
|
return result(r);
|
|
} else {
|
|
auto fields = get_structure_fields(m_env, S);
|
|
lean_assert(args.size() == num_params + fields.size());
|
|
format r;
|
|
if (m_structure_instances_qualifier)
|
|
r += format(S) + space() + format(".");
|
|
for (unsigned i = 0; i < fields.size(); i++) {
|
|
if (i > 0 || m_structure_instances_qualifier) r += line();
|
|
name fname = fields[i];
|
|
unsigned field_size = fname.utf8_size();
|
|
format fval_fmt = pp(args[i + num_params]).fmt();
|
|
if (i < fields.size() - 1) fval_fmt += comma();
|
|
r += format(fname) + space() + *g_assign_fmt + space() + nest(field_size + 4, fval_fmt);
|
|
}
|
|
r = group(nest(1, format("{") + r + format("}")));
|
|
return result(r);
|
|
}
|
|
}
|
|
|
|
static bool is_field_notation_candidate(environment const & env, expr const & e, bool implicit) {
|
|
expr const & f = get_app_fn(e);
|
|
if (!is_constant(f)) return false;
|
|
projection_info const * info = get_projection_info(env, const_name(f));
|
|
if (!info) return false; /* it is not a projection */
|
|
if (get_app_num_args(e) != info->m_nparams + 1) return false;
|
|
/* If implicit arguments is true, and the structure has parameters, we should not
|
|
pretty print using field notation because we will not be able to see the parameters. */
|
|
if (implicit && info->m_nparams) return false;
|
|
name const & S = const_name(f).get_prefix();
|
|
/* We should not use field notation with type classes since the structure is implicit. */
|
|
if (is_class(env, S)) return false;
|
|
return true;
|
|
}
|
|
|
|
auto pretty_fn::pp_field_notation(expr const & e) -> result {
|
|
lean_assert(is_field_notation_candidate(m_env, e, m_implict));
|
|
buffer<expr> args;
|
|
expr const & f = get_app_args(e, args);
|
|
bool ignore_hide = true;
|
|
format s_fmt = pp_child(args.back(), max_bp(), ignore_hide).fmt();
|
|
return result(max_bp()-1, s_fmt + format(".") + format(const_name(f).get_string()));
|
|
}
|
|
|
|
auto pretty_fn::pp_app(expr const & e) -> result {
|
|
if (auto r = pp_local_ref(e))
|
|
return *r;
|
|
if (is_default_arg_app(e))
|
|
return pp_child(app_fn(e), max_bp());
|
|
expr const & fn = app_fn(e);
|
|
if (m_structure_instances && is_structure_instance(m_env, e, m_implict))
|
|
return pp_structure_instance(e);
|
|
if (m_structure_projections && is_field_notation_candidate(m_env, e, m_implict))
|
|
return pp_field_notation(e);
|
|
// If the application contains a metavariable, then we want to
|
|
// show the function, otherwise it would be hard to understand the
|
|
// context where the metavariable occurs. This is hack to implement
|
|
// formatter.hide_full_terms
|
|
bool ignore_hide = true;
|
|
result res_fn = pp_child(fn, max_bp()-1, ignore_hide);
|
|
format fn_fmt = res_fn.fmt();
|
|
if (m_implict && (!is_app(fn) || (is_local_ref(m_env, fn))) && has_implicit_args(fn))
|
|
fn_fmt = compose(*g_explicit_fmt, fn_fmt);
|
|
result res_arg = pp_child(app_arg(e), max_bp());
|
|
return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
|
|
}
|
|
|
|
format pretty_fn::pp_binder(expr const & local) {
|
|
format r;
|
|
auto bi = local_info(local);
|
|
if (bi != binder_info())
|
|
r += format(open_binder_string(bi, m_unicode));
|
|
r += escape(mlocal_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;
|
|
}
|
|
|
|
format pretty_fn::pp_binder_block(buffer<name> const & names, expr const & type, binder_info const & bi) {
|
|
format r;
|
|
if (m_binder_types || bi != binder_info())
|
|
r += format(open_binder_string(bi, m_unicode));
|
|
for (name const & n : names) {
|
|
r += escape(n);
|
|
}
|
|
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<expr> const & locals) {
|
|
unsigned num = locals.size();
|
|
buffer<name> names;
|
|
expr local = locals[0];
|
|
expr type = mlocal_type(local);
|
|
binder_info bi = local_info(local);
|
|
names.push_back(mlocal_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(mlocal_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(mlocal_pp_name(local));
|
|
}
|
|
}
|
|
r += group(compose(line(), pp_binder_block(names, type, bi)));
|
|
return r;
|
|
}
|
|
|
|
auto pretty_fn::pp_lambda(expr const & e) -> result {
|
|
expr b = e;
|
|
buffer<expr> locals;
|
|
while (is_lambda(b)) {
|
|
auto p = binding_body_fresh(b, true);
|
|
locals.push_back(p.second);
|
|
b = p.first;
|
|
}
|
|
format r = m_unicode ? *g_lambda_n_fmt : *g_lambda_fmt;
|
|
r += pp_binders(locals);
|
|
r += group(compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).fmt()))));
|
|
return result(0, r);
|
|
}
|
|
|
|
/** \brief Similar to #is_arrow, but only returns true if binder_info is the default one.
|
|
That is, we don't want to lose binder info when pretty printing.
|
|
*/
|
|
static bool is_default_arrow(expr const & e) {
|
|
return is_arrow(e) && binding_info(e) == binder_info();
|
|
}
|
|
|
|
auto pretty_fn::pp_pi(expr const & e) -> result {
|
|
if (is_default_arrow(e)) {
|
|
result lhs = pp_child(binding_domain(e), get_arrow_prec());
|
|
expr b = lift_free_vars(binding_body(e), 1);
|
|
result rhs = is_pi(b) ? pp(b) : pp_child(b, get_arrow_prec()-1);
|
|
format r = group(lhs.fmt() + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt());
|
|
return result(get_arrow_prec(), get_arrow_prec()-1, r);
|
|
} else {
|
|
expr b = e;
|
|
buffer<expr> locals;
|
|
while (is_pi(b) && !is_default_arrow(b)) {
|
|
auto p = binding_body_fresh(b, true);
|
|
locals.push_back(p.second);
|
|
b = p.first;
|
|
}
|
|
format r;
|
|
if (is_prop(b))
|
|
r = m_unicode ? *g_forall_n_fmt : *g_forall_fmt;
|
|
else
|
|
r = m_unicode ? *g_pi_n_fmt : *g_pi_fmt;
|
|
r += pp_binders(locals);
|
|
r += group(compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).fmt()))));
|
|
return result(0, r);
|
|
}
|
|
}
|
|
|
|
static bool is_have(expr const & e) {
|
|
return is_app(e) && is_have_annotation(app_fn(e)) && is_binding(get_annotation_arg(app_fn(e)));
|
|
}
|
|
static bool is_show(expr const & e) {
|
|
return is_show_annotation(e) && is_app(get_annotation_arg(e)) &&
|
|
is_lambda(app_fn(get_annotation_arg(e)));
|
|
}
|
|
|
|
auto pretty_fn::pp_have(expr const & e) -> result {
|
|
expr proof = app_arg(e);
|
|
expr binding = get_annotation_arg(app_fn(e));
|
|
auto p = binding_body_fresh(binding, true);
|
|
expr local = p.second;
|
|
expr body = p.first;
|
|
name const & n = mlocal_pp_name(local);
|
|
format type_fmt = pp_child(mlocal_type(local), 0).fmt();
|
|
format proof_fmt = pp_child(proof, 0).fmt();
|
|
format body_fmt = pp_child(body, 0).fmt();
|
|
format head_fmt = *g_have_fmt;
|
|
format r = head_fmt + space() + escape(n) + space();
|
|
r += colon() + nest(m_indent, line() + type_fmt + comma() + space() + *g_from_fmt);
|
|
r = group(r);
|
|
r += nest(m_indent, line() + proof_fmt + comma());
|
|
r = group(r);
|
|
r += line() + body_fmt;
|
|
return result(0, r);
|
|
}
|
|
|
|
auto pretty_fn::pp_show(expr const & e) -> result {
|
|
lean_assert(is_show(e));
|
|
expr s = get_annotation_arg(e);
|
|
expr proof = app_arg(s);
|
|
expr type = binding_domain(app_fn(s));
|
|
format type_fmt = pp_child(type, 0).fmt();
|
|
format proof_fmt = pp_child(proof, 0).fmt();
|
|
format r = *g_show_fmt + space() + nest(5, type_fmt) + comma() + space() + *g_from_fmt;
|
|
r = group(r);
|
|
r += nest(m_indent, compose(line(), proof_fmt));
|
|
return result(0, group(r));
|
|
}
|
|
|
|
auto pretty_fn::pp_explicit(expr const & e) -> result {
|
|
result res_arg = pp_child(get_explicit_arg(e), max_bp());
|
|
return result(max_bp(), compose(*g_explicit_fmt, res_arg.fmt()));
|
|
}
|
|
|
|
auto pretty_fn::pp_delayed_abstraction(expr const & e) -> result {
|
|
if (m_use_holes) {
|
|
return pp_hole();
|
|
} else if (m_delayed_abstraction) {
|
|
format r;
|
|
r += format("[");
|
|
buffer<name> ns; buffer<expr> es;
|
|
get_delayed_abstraction_info(e, ns, es);
|
|
for (unsigned i = 0; i < ns.size(); i++) {
|
|
format r2;
|
|
if (i) r2 += format(",") + line();
|
|
r2 += pp(es[i]).fmt();
|
|
r += group(r2);
|
|
}
|
|
r += format("]");
|
|
return result(pp(get_delayed_abstraction_expr(e)).fmt() + nest(m_indent, r));
|
|
} else {
|
|
return pp(get_delayed_abstraction_expr(e));
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::pp_equation(expr const & e) -> format {
|
|
lean_assert(is_equation(e));
|
|
format r = format("|");
|
|
buffer<expr> args;
|
|
get_app_args(equation_lhs(e), args);
|
|
for (expr const & arg : args) {
|
|
r += space() + pp_child(arg, max_bp()).fmt();
|
|
}
|
|
r += space() + *g_assign_fmt + space() + pp_child(equation_rhs(e), 0).fmt();
|
|
return r;
|
|
}
|
|
|
|
auto pretty_fn::pp_equations(expr const & e) -> optional<result> {
|
|
buffer<expr> eqns;
|
|
unsigned num_fns = equations_num_fns(e);
|
|
to_equations(e, eqns);
|
|
buffer<expr> fns;
|
|
expr eqn = eqns[0];
|
|
for (unsigned i = 0; i < num_fns; i++) {
|
|
if (!is_lambda(eqn)) return optional<result>();
|
|
if (!closed(binding_domain(eqn))) return optional<result>();
|
|
auto p = binding_body_fresh(eqn, true);
|
|
fns.push_back(p.second);
|
|
eqn = p.first;
|
|
}
|
|
format r;
|
|
if (num_fns > 1) {
|
|
r = format("mutual_def") + space();
|
|
for (unsigned i = 0; i < num_fns; i++) {
|
|
if (i > 0) r += format(", ");
|
|
r += pp(fns[i]).fmt();
|
|
}
|
|
r += line();
|
|
} else {
|
|
r = format("def") + space() + pp(fns[0]).fmt() + space() + colon() + space() + pp(mlocal_type(fns[0])).fmt();
|
|
}
|
|
unsigned eqnidx = 0;
|
|
for (unsigned fidx = 0; fidx < num_fns; fidx++) {
|
|
if (num_fns > 1) {
|
|
if (fidx > 0) r += line();
|
|
r += format("with") + space() + pp(fns[fidx]).fmt() + space() + colon() +
|
|
space() + pp(mlocal_type(fns[fidx])).fmt();
|
|
}
|
|
if (eqnidx >= eqns.size()) return optional<result>();
|
|
expr eqn = eqns[eqnidx];
|
|
while (is_lambda(eqn)) {
|
|
eqn = binding_body_fresh(eqn, true).first;
|
|
}
|
|
eqnidx++;
|
|
if (is_equation(eqn)) {
|
|
r += line() + pp_equation(eqn);
|
|
while (eqnidx < eqns.size()) {
|
|
expr eqn = eqns[eqnidx];
|
|
while (is_lambda(eqn)) {
|
|
eqn = binding_body_fresh(eqn, true).first;
|
|
}
|
|
if (is_equation(eqn) &&
|
|
get_app_fn(equation_lhs(eqn)) == fns[fidx]) {
|
|
r += line() + pp_equation(eqn);
|
|
eqnidx++;
|
|
} else {
|
|
break;
|
|
}
|
|
}
|
|
} else {
|
|
/* noequation */
|
|
r += line() + format("[none]");
|
|
}
|
|
}
|
|
if (eqns.size() != eqnidx) return optional<result>();
|
|
return optional<result>(r);
|
|
}
|
|
|
|
auto pretty_fn::pp_macro_default(expr const & e) -> result {
|
|
// TODO(Leo): have macro annotations
|
|
// fix macro<->pp interface
|
|
if (is_prenum(e)) {
|
|
return format(prenum_value(e).to_string());
|
|
}
|
|
format r = compose(format("["), format(macro_def(e).get_name()));
|
|
for (unsigned i = 0; i < macro_num_args(e); i++)
|
|
r += nest(m_indent, compose(line(), pp_child(macro_arg(e, i), max_bp()).fmt()));
|
|
r += format("]");
|
|
return result(group(r));
|
|
}
|
|
|
|
auto pretty_fn::pp_macro(expr const & e) -> result {
|
|
if (is_explicit(e)) {
|
|
return pp_explicit(e);
|
|
} else if (is_expr_quote(e)) {
|
|
return result(format("`(") + nest(4, pp(get_expr_quote_value(e)).fmt()) + format(")"));
|
|
} else if (is_pexpr_quote(e)) {
|
|
return result(format("``(") + nest(2, pp(get_pexpr_quote_value(e)).fmt()) + format(")"));
|
|
} else if (is_delayed_abstraction(e)) {
|
|
return pp_delayed_abstraction(e);
|
|
} else if (is_inaccessible(e)) {
|
|
format r = format(".") + pp_child(get_annotation_arg(e), max_bp()).fmt();
|
|
return result(r);
|
|
} else if (is_as_pattern(e)) {
|
|
auto lhs_fmt = pp_child(get_as_pattern_lhs(e), max_bp()).fmt();
|
|
auto rhs_fmt = pp_child(get_as_pattern_rhs(e), max_bp()).fmt();
|
|
return result(lhs_fmt + format("@") + rhs_fmt);
|
|
} else if (is_pattern_hint(e)) {
|
|
return result(group(nest(2, format("(:") + pp(get_pattern_hint_arg(e)).fmt() + format(":)"))));
|
|
} else if (is_marked_as_comp_irrelevant(e)) {
|
|
if (m_hide_comp_irrel)
|
|
return m_unicode ? format("◾") : format("irrel");
|
|
else
|
|
return pp(get_annotation_arg(e));
|
|
} else if (!m_strings && to_string(e)) {
|
|
expr n = *macro_def(e).expand(e, m_ctx);
|
|
return pp(n);
|
|
} else if (is_equations(e)) {
|
|
if (auto r = pp_equations(e))
|
|
return *r;
|
|
else
|
|
return pp_macro_default(e);
|
|
} else if (is_annotation(e)) {
|
|
if (m_annotations)
|
|
return format("[") + format(get_annotation_kind(e)) + space() + pp(get_annotation_arg(e)).fmt() + format("]");
|
|
else
|
|
return pp(get_annotation_arg(e));
|
|
} else if (is_rec_fn_macro(e)) {
|
|
return format("[") + format(get_rec_fn_name(e)) + format("]");
|
|
} else if (is_synthetic_sorry(e)) {
|
|
if (m_use_holes)
|
|
return pp_hole();
|
|
else
|
|
return m_unicode ? format("⁇") : format("??");
|
|
} else if (is_sorry(e)) {
|
|
if (m_use_holes)
|
|
return pp_hole();
|
|
else
|
|
return format("sorry");
|
|
} else {
|
|
return pp_macro_default(e);
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::pp_let(expr e) -> result {
|
|
buffer<std::tuple<expr, expr, expr>> decls;
|
|
while (true) {
|
|
expr t = let_type(e);
|
|
expr v = let_value(e);
|
|
expr b = let_body(e);
|
|
auto p = let_body_fresh(e, true);
|
|
decls.emplace_back(p.second, t, v);
|
|
e = p.first;
|
|
if (!is_let(e))
|
|
break;
|
|
}
|
|
lean_assert(!decls.empty());
|
|
format r = *g_let_fmt;
|
|
unsigned sz = decls.size();
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
expr l, t, v;
|
|
std::tie(l, t, v) = decls[i];
|
|
name const & n = mlocal_pp_name(l);
|
|
format beg = i == 0 ? space() : line();
|
|
format sep = i < sz - 1 ? comma() : format();
|
|
format entry = format(n);
|
|
format v_fmt = pp_child(v, 0).fmt();
|
|
if (is_neutral_expr(t)) {
|
|
entry += space() + *g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
|
|
} else {
|
|
format t_fmt = pp_child(t, 0).fmt();
|
|
entry += space() + colon() + space() + t_fmt + space() + *g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
|
|
}
|
|
r += nest(3 + 1, beg + group(entry));
|
|
}
|
|
format b = pp_child(e, 0).fmt();
|
|
r += line() + *g_in_fmt + space() + nest(2 + 1, b);
|
|
return result(0, r);
|
|
}
|
|
|
|
auto pretty_fn::pp_num(mpz const & n, unsigned bp) -> result {
|
|
if (n.is_neg()) {
|
|
auto prec = get_expr_precedence(m_token_table, "-");
|
|
if (!prec || bp > *prec) {
|
|
return result(paren(format(n.to_string())));
|
|
}
|
|
}
|
|
return result(format(n.to_string()));
|
|
}
|
|
|
|
// Return the number of parameters in a notation declaration.
|
|
static unsigned get_num_parameters(notation_entry const & entry) {
|
|
if (entry.is_numeral())
|
|
return 0;
|
|
unsigned r = 0;
|
|
if (!entry.is_nud())
|
|
r++;
|
|
for (auto const & t : entry.get_transitions()) {
|
|
switch (t.get_action().kind()) {
|
|
case notation::action_kind::Skip:
|
|
case notation::action_kind::Binder:
|
|
case notation::action_kind::Binders:
|
|
break;
|
|
case notation::action_kind::Expr:
|
|
case notation::action_kind::Exprs:
|
|
case notation::action_kind::ScopedExpr:
|
|
case notation::action_kind::Ext:
|
|
r++;
|
|
}
|
|
}
|
|
return r;
|
|
}
|
|
|
|
bool pretty_fn::match(level const & p, level const & l) {
|
|
if (p == l)
|
|
return true;
|
|
if (m_universes)
|
|
return false;
|
|
if (is_placeholder(p))
|
|
return true;
|
|
if (is_succ(p) && is_succ(l))
|
|
return match(succ_of(p), succ_of(l));
|
|
return false;
|
|
}
|
|
|
|
bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & args) {
|
|
if (is_explicit(p)) {
|
|
return match(get_explicit_arg(p), e, args);
|
|
} else if (is_as_atomic(p)) {
|
|
return match(get_app_fn(get_as_atomic_arg(p)), e, args);
|
|
} else if (is_var(p)) {
|
|
unsigned vidx = var_idx(p);
|
|
if (vidx >= args.size())
|
|
return false;
|
|
unsigned i = args.size() - vidx - 1;
|
|
if (args[i])
|
|
return *args[i] == e;
|
|
args[i] = e;
|
|
return true;
|
|
} else if (is_placeholder(p)) {
|
|
return true;
|
|
} else if (is_constant(p) && is_constant(e)) {
|
|
if (const_name(p) != const_name(e))
|
|
return false;
|
|
levels p_ls = const_levels(p);
|
|
levels e_ls = const_levels(p);
|
|
while (!is_nil(p_ls)) {
|
|
if (is_nil(e_ls))
|
|
return false; // e must have at least as many arguments as p
|
|
if (!match(head(p_ls), head(e_ls)))
|
|
return false;
|
|
p_ls = tail(p_ls);
|
|
e_ls = tail(e_ls);
|
|
}
|
|
return true;
|
|
} else if (is_sort(p)) {
|
|
if (!is_sort(e))
|
|
return false;
|
|
return match(sort_level(p), sort_level(e));
|
|
} else if (is_app(e)) {
|
|
buffer<expr> p_args, e_args;
|
|
expr p_fn = get_app_args(p, p_args);
|
|
expr e_fn = get_app_args(e, e_args);
|
|
if (!match(p_fn, e_fn, args))
|
|
return false;
|
|
if (is_explicit(p)) {
|
|
if (p_args.size() != e_args.size())
|
|
return false;
|
|
for (unsigned i = 0; i < p_args.size(); i++) {
|
|
if (!match(p_args[i], e_args[i], args))
|
|
return false;
|
|
}
|
|
return true;
|
|
} else {
|
|
try {
|
|
expr fn_type = m_ctx.infer(e_fn);
|
|
unsigned j = 0;
|
|
for (unsigned i = 0; i < e_args.size(); i++) {
|
|
fn_type = m_ctx.relaxed_whnf(fn_type);
|
|
if (!is_pi(fn_type))
|
|
return false;
|
|
expr const & body = binding_body(fn_type);
|
|
binder_info const & info = binding_info(fn_type);
|
|
if (is_explicit(info)) {
|
|
if (j >= p_args.size())
|
|
return false;
|
|
if (!match(p_args[j], e_args[i], args))
|
|
return false;
|
|
j++;
|
|
}
|
|
fn_type = instantiate(body, e_args[i]);
|
|
}
|
|
return j == p_args.size();
|
|
} catch (exception &) {
|
|
return false;
|
|
}
|
|
}
|
|
} else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
static unsigned get_some_precedence(token_table const & t, name const & tk) {
|
|
if (tk.is_atomic() && tk.is_string()) {
|
|
if (auto p = get_expr_precedence(t, tk.get_string()))
|
|
return *p;
|
|
} else {
|
|
if (auto p = get_expr_precedence(t, tk.to_string().c_str()))
|
|
return *p;
|
|
}
|
|
return 0;
|
|
}
|
|
|
|
auto pretty_fn::pp_notation_child(expr const & e, unsigned rbp, unsigned lbp) -> result {
|
|
if (is_app(e)) {
|
|
if (m_numerals) {
|
|
if (auto n = to_num(e)) return pp_num(*n, lbp);
|
|
}
|
|
if (m_strings) {
|
|
if (auto r = to_string(e)) return pp_string_literal(*r);
|
|
if (auto r = to_char(m_ctx, e)) return pp_char_literal(*r);
|
|
}
|
|
expr const & f = app_fn(e);
|
|
if (is_implicit(f)) {
|
|
return pp_notation_child(f, rbp, lbp);
|
|
} else if (!m_coercion && is_coercion(e)) {
|
|
return pp_hide_coercion(e, rbp);
|
|
} else if (!m_coercion && is_coercion_fn(e)) {
|
|
return pp_hide_coercion_fn(e, rbp);
|
|
}
|
|
}
|
|
result r = pp(e);
|
|
/* see invariants of `pretty_fn::result`: Check that the surrounding notation would parse at least r
|
|
* by the first invariant, and at most r (instead of the following token with binding power lbp) by the
|
|
* second invariant. */
|
|
if (rbp < r.lbp() && r.rbp() >= lbp) {
|
|
return r;
|
|
} else {
|
|
return result(paren(r.fmt()));
|
|
}
|
|
}
|
|
|
|
static bool is_atomic_notation(notation_entry const & entry) {
|
|
if (!entry.is_nud())
|
|
return false;
|
|
list<notation::transition> const & ts = entry.get_transitions();
|
|
if (!is_nil(tail(ts)))
|
|
return false;
|
|
return head(ts).get_action().kind() == notation::action_kind::Skip;
|
|
}
|
|
|
|
static format mk_tk_fmt(name const & tkn) {
|
|
auto tk = tkn.to_string();
|
|
if (!tk.empty() && tk.back() == ' ') {
|
|
tk.pop_back();
|
|
return format(tk) + line();
|
|
} else {
|
|
return format(tk);
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>> & args) -> optional<result> {
|
|
if (entry.is_numeral()) {
|
|
return some(result(format(entry.get_num().to_string())));
|
|
} else if (is_atomic_notation(entry)) {
|
|
format fmt = format(head(entry.get_transitions()).get_token());
|
|
return some(result(fmt));
|
|
} else {
|
|
using notation::transition;
|
|
buffer<transition> ts;
|
|
buffer<expr> locals; // from scoped_expr
|
|
to_buffer(entry.get_transitions(), ts);
|
|
format fmt;
|
|
unsigned i = ts.size();
|
|
// bp of the last action
|
|
unsigned last_rbp = inf_bp()-1;
|
|
// bp of the token immediately to the right of the action
|
|
unsigned token_lbp = 0;
|
|
bool last = true;
|
|
while (i > 0) {
|
|
--i;
|
|
format curr;
|
|
notation::action const & a = ts[i].get_action();
|
|
name const & tk = ts[i].get_token();
|
|
format tk_fmt = mk_tk_fmt(ts[i].get_pp_token());
|
|
switch (a.kind()) {
|
|
case notation::action_kind::Skip:
|
|
curr = tk_fmt;
|
|
if (last)
|
|
// invariant fulfilled: Skip action will never parse a trailing token
|
|
last_rbp = inf_bp();
|
|
break;
|
|
case notation::action_kind::Expr:
|
|
if (args.empty() || !args.back()) {
|
|
return optional<result>();
|
|
} else {
|
|
expr e = *args.back();
|
|
args.pop_back();
|
|
result e_r = pp_notation_child(e, a.rbp(), token_lbp);
|
|
curr = tk_fmt + e_r.fmt();
|
|
if (last)
|
|
/* last_rbp can be no more than `a.rbp()`, since this is the bp used during parsing.
|
|
* However, `e_r.rbp()` may actually be smaller since it may be missing parentheses
|
|
* compared to the original input. For example, when re-printing `x >>= (fun y, z) = ...`,
|
|
* `e_r.fmt()` will be `fun y, z`. If we used the rbp of the `>>=` instead of
|
|
* `e_r.rbp()` (0), we would get the wrong output `x >>= fun y, z = ...`. */
|
|
last_rbp = std::min(a.rbp(), e_r.rbp());
|
|
break;
|
|
}
|
|
case notation::action_kind::Exprs:
|
|
if (args.empty() || !args.back()) {
|
|
return optional<result>();
|
|
} else {
|
|
expr e = *args.back();
|
|
args.pop_back();
|
|
expr const & rec = a.get_rec();
|
|
optional<expr> const & ini = a.get_initial();
|
|
buffer<expr> rec_args;
|
|
bool matched_once = false;
|
|
while (true) {
|
|
args.resize(args.size() + 2);
|
|
if (!match(rec, e, args)) {
|
|
args.pop_back();
|
|
args.pop_back();
|
|
break;
|
|
}
|
|
optional<expr> new_e = args.back();
|
|
args.pop_back();
|
|
optional<expr> rec_arg = args.back();
|
|
args.pop_back();
|
|
if (!new_e || !rec_arg)
|
|
return optional<result>();
|
|
rec_args.push_back(*rec_arg);
|
|
e = *new_e;
|
|
matched_once = true;
|
|
}
|
|
if (!matched_once && ini)
|
|
return optional<result>();
|
|
if (ini) {
|
|
if (!match(*ini, e, args))
|
|
return optional<result>();
|
|
} else {
|
|
rec_args.push_back(e);
|
|
}
|
|
if (!a.is_fold_right())
|
|
std::reverse(rec_args.begin(), rec_args.end());
|
|
unsigned curr_lbp = token_lbp;
|
|
if (auto t = a.get_terminator()) {
|
|
curr = format(*t);
|
|
curr_lbp = get_some_precedence(m_token_table, *t);
|
|
}
|
|
unsigned j = rec_args.size();
|
|
format sep_fmt = format(a.get_sep());
|
|
unsigned sep_lbp = get_some_precedence(m_token_table, a.get_sep());
|
|
while (j > 0) {
|
|
--j;
|
|
result arg_res = pp_notation_child(rec_args[j], a.rbp(), curr_lbp);
|
|
if (j == 0) {
|
|
curr = tk_fmt + arg_res.fmt() + curr;
|
|
} else {
|
|
curr = sep_fmt + arg_res.fmt() + curr;
|
|
}
|
|
curr_lbp = sep_lbp;
|
|
}
|
|
break;
|
|
}
|
|
case notation::action_kind::Binder:
|
|
if (locals.size() != 1)
|
|
return optional<result>();
|
|
curr = tk_fmt + pp_binder(locals[0]);
|
|
break;
|
|
case notation::action_kind::Binders:
|
|
curr = tk_fmt + pp_binders(locals);
|
|
break;
|
|
case notation::action_kind::ScopedExpr:
|
|
if (args.empty() || !args.back()) {
|
|
return optional<result>();
|
|
} else {
|
|
expr e = *args.back();
|
|
bool first_scoped = locals.empty();
|
|
unsigned i = 0;
|
|
args.pop_back();
|
|
expr const & rec = a.get_rec();
|
|
while (true) {
|
|
args.resize(args.size() + 1);
|
|
if (!match(rec, e, args) || !args.back()) {
|
|
args.pop_back();
|
|
break;
|
|
}
|
|
expr b = *args.back();
|
|
args.pop_back();
|
|
if (!((is_lambda(b) && a.use_lambda_abstraction()) ||
|
|
(is_pi(b) && !a.use_lambda_abstraction()))) {
|
|
break;
|
|
}
|
|
auto p = binding_body_fresh(b, true);
|
|
if (first_scoped) {
|
|
locals.push_back(p.second);
|
|
} else {
|
|
if (i >= locals.size() || locals[i] != p.second)
|
|
return optional<result>();
|
|
}
|
|
e = p.first;
|
|
i++;
|
|
}
|
|
if (locals.empty())
|
|
return optional<result>();
|
|
result e_r = pp_notation_child(e, a.rbp(), token_lbp);
|
|
curr = tk_fmt + e_r.fmt();
|
|
if (last)
|
|
// see Expr action
|
|
last_rbp = std::min(a.rbp(), e_r.rbp());
|
|
break;
|
|
}
|
|
case notation::action_kind::Ext:
|
|
return optional<result>();
|
|
}
|
|
token_lbp = get_some_precedence(m_token_table, tk);
|
|
if (last) {
|
|
fmt = curr;
|
|
last = false;
|
|
} else {
|
|
fmt = curr + fmt;
|
|
}
|
|
}
|
|
unsigned first_lbp = inf_bp();
|
|
if (!entry.is_nud()) {
|
|
first_lbp = token_lbp;
|
|
lean_assert(!last);
|
|
if (args.size() != 1 || !args.back())
|
|
return optional<result>();
|
|
expr e = *args.back();
|
|
args.pop_back();
|
|
format e_fmt = pp_notation_child(e, 0, token_lbp).fmt();
|
|
fmt = e_fmt + fmt;
|
|
}
|
|
return optional<result>(result(first_lbp, last_rbp, group(nest(m_indent, fmt))));
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::pp_notation(expr const & e) -> optional<result> {
|
|
if (!m_notation || is_var(e))
|
|
return optional<result>();
|
|
for (notation_entry const & entry : get_notation_entries(m_env, head_index(e))) {
|
|
if (entry.group() == notation_entry_group::Reserve)
|
|
continue;
|
|
if (!m_unicode && !entry.is_safe_ascii())
|
|
continue; // ignore this notation declaration since unicode support is not enabled
|
|
unsigned num_params = get_num_parameters(entry);
|
|
buffer<optional<expr>> args;
|
|
args.resize(num_params);
|
|
if (match(entry.get_expr(), e, args)) {
|
|
if (auto r = pp_notation(entry, args))
|
|
return r;
|
|
}
|
|
}
|
|
return optional<result>();
|
|
}
|
|
|
|
static bool is_pp_atomic(expr const & e) {
|
|
switch (e.kind()) {
|
|
case expr_kind::App:
|
|
case expr_kind::Lambda:
|
|
case expr_kind::Pi:
|
|
case expr_kind::Macro:
|
|
return false;
|
|
default:
|
|
return true;
|
|
}
|
|
}
|
|
|
|
static bool is_subtype(expr const & e) {
|
|
return
|
|
is_constant(get_app_fn(e), get_subtype_name()) &&
|
|
get_app_num_args(e) == 2 &&
|
|
is_lambda(app_arg(e));
|
|
}
|
|
|
|
auto pretty_fn::pp_subtype(expr const & e) -> result {
|
|
lean_assert(is_subtype(e));
|
|
expr pred = app_arg(e);
|
|
lean_assert(is_lambda(pred));
|
|
auto p = binding_body_fresh(pred, true);
|
|
expr body = p.first;
|
|
expr local = p.second;
|
|
format r = bracket("{", format(mlocal_pp_name(local)) + space() + format("//") + space() + pp_child(body, 0).fmt(), "}");
|
|
return result(r);
|
|
}
|
|
|
|
static bool is_emptyc(expr const & e) {
|
|
return
|
|
is_constant(get_app_fn(e), get_has_emptyc_emptyc_name()) &&
|
|
get_app_num_args(e) == 2;
|
|
}
|
|
|
|
static bool is_singleton(expr const & e) {
|
|
return
|
|
is_constant(get_app_fn(e), get_singleton_name()) &&
|
|
get_app_num_args(e) == 5;
|
|
}
|
|
|
|
static bool is_insert(expr const & e) {
|
|
return
|
|
is_constant(get_app_fn(e), get_has_insert_insert_name()) &&
|
|
get_app_num_args(e) == 5;
|
|
}
|
|
|
|
/* Return true iff 'e' encodes a nonempty finite collection,
|
|
and stores its elements at elems. */
|
|
static bool is_explicit_collection(expr const & e, buffer<expr> & elems) {
|
|
if (is_emptyc(e)) {
|
|
return true;
|
|
} else if (is_singleton(e)) {
|
|
elems.push_back(app_arg(e));
|
|
return true;
|
|
} else if (is_insert(e) && is_explicit_collection(app_arg(e), elems)) {
|
|
elems.push_back(app_arg(app_fn(e)));
|
|
return true;
|
|
} else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
auto pretty_fn::pp_explicit_collection(buffer<expr> const & elems) -> result {
|
|
if (elems.empty()) {
|
|
return result(format(m_unicode ? "∅" : "{}"));
|
|
} else {
|
|
format r = pp_child(elems[0], 0).fmt();
|
|
for (unsigned i = 1; i < elems.size(); i++) {
|
|
r += nest(m_indent, comma() + line() + pp_child(elems[i], 0).fmt());
|
|
}
|
|
r = group(bracket("{", r, "}"));
|
|
return result(r);
|
|
}
|
|
}
|
|
|
|
bool is_set_of(expr const & e) {
|
|
return
|
|
is_constant(get_app_fn(e), get_set_of_name()) &&
|
|
get_app_num_args(e) == 2 &&
|
|
is_lambda(app_arg(e));
|
|
}
|
|
|
|
auto pretty_fn::pp_set_of(expr const & e) -> result {
|
|
lean_assert(is_set_of(e));
|
|
expr pred = app_arg(e);
|
|
lean_assert(is_lambda(pred));
|
|
auto p = binding_body_fresh(pred, true);
|
|
expr body = p.first;
|
|
expr local = p.second;
|
|
format r = bracket("{",
|
|
pp_binder(local) + space() + format("|") + space() +
|
|
pp_child(body, 0).fmt(), "}");
|
|
return result(r);
|
|
}
|
|
|
|
static bool is_sep(expr const & e) {
|
|
return
|
|
is_constant(get_app_fn(e), get_has_sep_sep_name()) &&
|
|
get_app_num_args(e) == 5 &&
|
|
is_lambda(app_arg(app_fn(e)));
|
|
}
|
|
|
|
auto pretty_fn::pp_sep(expr const & e) -> result {
|
|
lean_assert(is_sep(e));
|
|
expr s = app_arg(e);
|
|
expr pred = app_arg(app_fn(e));
|
|
lean_assert(is_lambda(pred));
|
|
auto p = binding_body_fresh(pred, true);
|
|
expr body = p.first;
|
|
expr local = p.second;
|
|
format in = format(m_unicode ? "∈" : "in");
|
|
format r = bracket("{",
|
|
format(mlocal_pp_name(local)) + space() + in + space() +
|
|
pp_child(s, 0).fmt() + space() + format("|") + space() +
|
|
pp_child(body, 0).fmt(), "}");
|
|
return result(r);
|
|
}
|
|
|
|
auto pretty_fn::pp_prod(expr const & e) -> result {
|
|
format r = pp(app_arg(app_fn(e))).fmt();
|
|
auto it = app_arg(e);
|
|
while (is_app_of(it, get_prod_mk_name(), 4)) {
|
|
r += comma() + line();
|
|
r += pp(app_arg(app_fn(it))).fmt();
|
|
it = app_arg(it);
|
|
}
|
|
r += comma() + line();
|
|
r += pp(it).fmt();
|
|
return result(paren(group(r)));
|
|
}
|
|
|
|
auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
|
|
check_system("pretty printer");
|
|
if ((m_depth >= m_max_depth ||
|
|
m_num_steps > m_max_steps ||
|
|
(m_hide_full_terms && !ignore_hide && !has_expr_metavar(e))) &&
|
|
!is_pp_atomic(e)) {
|
|
return result(m_unicode ? *g_ellipsis_n_fmt : *g_ellipsis_fmt);
|
|
}
|
|
flet<unsigned> let_d(m_depth, m_depth+1);
|
|
m_num_steps++;
|
|
|
|
if (m_numerals) {
|
|
if (auto n = to_num(e)) return pp_num(*n, 0);
|
|
}
|
|
if (m_strings) {
|
|
if (auto r = to_string(e)) return pp_string_literal(*r);
|
|
if (auto r = to_char(m_ctx, e)) return pp_char_literal(*r);
|
|
}
|
|
try {
|
|
if (!m_proofs && !is_constant(e) && !is_mlocal(e) && closed(e) && is_prop(m_ctx.infer(e))) {
|
|
return result(format("_"));
|
|
}
|
|
} catch (exception) {}
|
|
|
|
if (auto r = pp_notation(e))
|
|
return *r;
|
|
|
|
if (m_notation) {
|
|
if (is_subtype(e))
|
|
return pp_subtype(e);
|
|
if (is_sep(e))
|
|
return pp_sep(e);
|
|
if (is_set_of(e))
|
|
return pp_set_of(e);
|
|
buffer<expr> elems;
|
|
if (is_explicit_collection(e, elems))
|
|
return pp_explicit_collection(elems);
|
|
if (is_app_of(e, get_prod_mk_name(), 4))
|
|
return pp_prod(e);
|
|
}
|
|
|
|
if (is_placeholder(e)) return result(*g_placeholder_fmt);
|
|
if (is_show(e)) return pp_show(e);
|
|
if (is_have(e)) return pp_have(e);
|
|
if (is_typed_expr(e)) return pp(get_typed_expr_expr(e));
|
|
if (m_num_nat_coe)
|
|
if (auto k = to_unsigned(e))
|
|
return format(*k);
|
|
switch (e.kind()) {
|
|
case expr_kind::Var: return pp_var(e);
|
|
case expr_kind::Sort: return pp_sort(e);
|
|
case expr_kind::Constant: return pp_const(e);
|
|
case expr_kind::Meta: return pp_meta(e);
|
|
case expr_kind::Local: return pp_local(e);
|
|
case expr_kind::App: return pp_app(e);
|
|
case expr_kind::Lambda: return pp_lambda(e);
|
|
case expr_kind::Pi: return pp_pi(e);
|
|
case expr_kind::Macro: return pp_macro(e);
|
|
case expr_kind::Let: return pp_let(e);
|
|
}
|
|
lean_unreachable(); // LCOV_EXCL_LINE
|
|
}
|
|
|
|
pretty_fn::pretty_fn(environment const & env, options const & o, abstract_type_context & ctx):
|
|
m_env(env), m_ctx(ctx), m_token_table(get_token_table(env)) {
|
|
set_options_core(o);
|
|
m_meta_prefix = "M";
|
|
m_next_meta_idx = 1;
|
|
}
|
|
|
|
// Custom beta reduction procedure for the pretty printer.
|
|
// We don't want to reduce application in show annotations.
|
|
class pp_beta_reduce_fn : public replace_visitor {
|
|
virtual expr visit_meta(expr const & e) override { return e; }
|
|
virtual expr visit_local(expr const & e) override { return e; }
|
|
|
|
virtual expr visit_macro(expr const & e) override {
|
|
if (is_show_annotation(e) && is_app(get_annotation_arg(e))) {
|
|
expr const & n = get_annotation_arg(e);
|
|
expr new_fn = visit(app_fn(n));
|
|
expr new_arg = visit(app_arg(n));
|
|
return mk_show_annotation(mk_app(new_fn, new_arg));
|
|
} else {
|
|
return replace_visitor::visit_macro(e);
|
|
}
|
|
}
|
|
|
|
virtual expr visit_app(expr const & e) override {
|
|
expr new_e = replace_visitor::visit_app(e);
|
|
if (is_head_beta(new_e))
|
|
return visit(head_beta_reduce(new_e));
|
|
else
|
|
return new_e;
|
|
}
|
|
};
|
|
|
|
std::string sexpr_to_string(sexpr const & s) {
|
|
if (is_string(s))
|
|
return to_string(s);
|
|
std::stringstream ss;
|
|
ss << s;
|
|
return ss.str();
|
|
}
|
|
|
|
// check whether a space must be inserted between the strings so that lexing them would
|
|
// produce separate tokens
|
|
std::pair<bool, token_table const *> pretty_fn::needs_space_sep(token_table const * last, std::string const & s1, std::string const & s2) const {
|
|
if (s1.empty() || (is_id_rest(get_utf8_last_char(s1.data()), s1.data() + s1.size()) && is_id_rest(s2.data(), s2.data() + s2.size())))
|
|
return mk_pair(true, nullptr); // would be lexed as a single identifier without space
|
|
|
|
if (last) {
|
|
// complete deferred two-token lookahead
|
|
for (char c : s2) {
|
|
last = last->find(c);
|
|
if (!last)
|
|
break;
|
|
if (last->value())
|
|
return mk_pair(true, nullptr);
|
|
}
|
|
if (last) {
|
|
// would need an even larger lookahead, give up
|
|
return mk_pair(true, nullptr);
|
|
}
|
|
}
|
|
|
|
// check whether s1 + s2 has a longer prefix in the token table than s1
|
|
token_table const * t = &m_token_table;
|
|
for (char c : s1) {
|
|
t = t->find(c);
|
|
if (!t)
|
|
return mk_pair(false, nullptr); // s1 must be an identifier, and we know s2 does not start with is_id_rest
|
|
}
|
|
for (char c : s2) {
|
|
t = t->find(c);
|
|
if (!t)
|
|
return mk_pair(false, nullptr);
|
|
if (t->value())
|
|
return mk_pair(true, nullptr);
|
|
}
|
|
|
|
// the next identifier may expand s1 + s2 to a token, defer decision
|
|
return mk_pair(false, t);
|
|
}
|
|
|
|
format pretty_fn::operator()(expr const & e) {
|
|
auto purified = purify(m_beta ? pp_beta_reduce_fn()(e) : e);
|
|
|
|
if (!m_options.contains(get_pp_proofs_name()) && !get_pp_all(m_options)) {
|
|
try {
|
|
m_proofs = !closed(purified) || is_prop(m_ctx.infer(purified));
|
|
} catch (exception) {
|
|
m_proofs = true;
|
|
}
|
|
}
|
|
|
|
m_depth = 0; m_num_steps = 0;
|
|
result r = pp_child(purified, 0);
|
|
|
|
// insert spaces so that lexing the result round-trips
|
|
std::function<bool(sexpr const &, sexpr const &)> sep; // NOLINT
|
|
token_table const * last = nullptr;
|
|
sep = [&](sexpr const & s1, sexpr const & s2) {
|
|
bool b;
|
|
std::tie(b, last) = needs_space_sep(last, sexpr_to_string(s1), sexpr_to_string(s2));
|
|
return b;
|
|
};
|
|
return r.fmt().separate_tokens(sep);
|
|
}
|
|
|
|
formatter_factory mk_pretty_formatter_factory() {
|
|
return [](environment const & env, options const & o, abstract_type_context & ctx) { // NOLINT
|
|
auto fn_ptr = std::make_shared<pretty_fn>(env, o, ctx);
|
|
return formatter(o, [=](expr const & e, options const & new_o) {
|
|
fn_ptr->set_options(new_o);
|
|
return (*fn_ptr)(e);
|
|
});
|
|
};
|
|
}
|
|
|
|
static options mk_options(bool detail) {
|
|
options opts;
|
|
if (detail) {
|
|
opts = opts.update(name{"pp", "implicit"}, true);
|
|
opts = opts.update(name{"pp", "notation"}, false);
|
|
}
|
|
return opts;
|
|
}
|
|
|
|
static void pp_core(environment const & env, expr const & e, bool detail) {
|
|
type_checker tc(env);
|
|
io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
|
|
regular(env, ios, tc) << e << "\n";
|
|
}
|
|
|
|
}
|
|
// for debugging purposes
|
|
void pp(lean::environment const & env, lean::expr const & e) { lean::pp_core(env, e, false); }
|
|
void pp_detail(lean::environment const & env, lean::expr const & e) { lean::pp_core(env, e, true); }
|