<commit_before>/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <algorithm>
#include <limits>
#include "util/flet.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/scoped_ext.h"
#include "library/coercion.h"
#include "library/expr_pair.h"
#include "library/placeholder.h"
#include "library/private.h"
#include "library/protected.h"
#include "library/explicit.h"
#include "library/typed_expr.h"
#include "library/num.h"
#include "library/util.h"
#include "library/let.h"
#include "library/print.h"
#include "library/abbreviation.h"
#include "library/pp_options.h"
#include "library/constants.h"
#include "library/replace_visitor.h"
#include "library/definitional/equations.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/util.h"
#include "frontends/lean/token_table.h"
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/parser_config.h"
#include "frontends/lean/local_ref_info.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_assert_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 name   * g_tmp_prefix      = nullptr;

class nat_numeral_pp {
    expr m_num_type;
    name m_nat;
    expr m_nat_of_num;
    expr m_zero;
    expr m_succ;
public:
    nat_numeral_pp():
        m_num_type(mk_constant(get_num_name())),
        m_nat(get_nat_name()),
        m_nat_of_num(mk_constant(get_nat_of_num_name())),
        m_zero(mk_constant(get_nat_zero_name())),
        m_succ(mk_constant(get_nat_succ_name())) {
    }

    // Return ture if the environment has a coercion from num->nat
    bool has_coercion_num_nat(environment const & env) const {
        list<expr> coes = get_coercions(env, m_num_type, m_nat);
        if (length(coes) != 1)
            return false;
        return head(coes) == m_nat_of_num;
    }

    // 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_zero) {
                return optional<unsigned>(r);
            } else if (is_app(*it) && app_fn(*it) == m_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 {
                return optional<unsigned>();
            }
        }
    }
};

static nat_numeral_pp * g_nat_numeral_pp = nullptr;

static bool has_coercion_num_nat(environment const & env) {
    return g_nat_numeral_pp->has_coercion_num_nat(env);
}

static optional<unsigned> to_unsigned(expr const & e) {
    return g_nat_numeral_pp->to_unsigned(e);
}

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("\u03BB")));
    g_lambda_fmt      = new format(highlight_keyword(format("fun")));
    g_forall_n_fmt    = new format(highlight_keyword(format("\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("\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_assert_fmt      = new format(highlight_keyword(format("assert")));
    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_tmp_prefix      = new name(name::mk_internal_unique_name());
    g_nat_numeral_pp  = new nat_numeral_pp();
}

void finalize_pp() {
    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_assert_fmt;
    delete g_from_fmt;
    delete g_visible_fmt;
    delete g_show_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) {
    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 = 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_meta(l))
                return some_level(mk_meta_univ(mk_metavar_name(meta_id(l))));
            return none_level();
        });
}

/** \brief Make sure that all metavariables have reasonable names,
    and for all local constants l1 l2, local_pp_name(l1) != local_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.
*/
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 (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)));
            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) {
    m_options         = o;
    bool all          = get_pp_all(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         = all || get_pp_implicit(o);
    m_unicode         = get_pp_unicode(o);
    m_coercion        = all || get_pp_coercions(o);
    m_notation        = !all && get_pp_notation(o);
    m_universes       = all || get_pp_universes(o);
    m_full_names      = all || 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_purify_locals   = get_pp_purify_locals(o);
    m_beta            = !all && get_pp_beta(o);
    m_numerals        = get_pp_numerals(o);
    m_abbreviations   = !all && 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);
}

void pretty_fn::set_options(options const & o) {
    if (is_eqp(o, m_options))
        return;
    set_options_core(o);
}

format pretty_fn::pp_level(level const & l) {
    return ::lean::pp(l, m_unicode, m_indent);
}

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 {
        binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f).first).first);
        return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit();
    } catch (exception &) {
        return false;
    }
}

bool pretty_fn::is_prop(expr const & e) {
    try {
        return m_env.impredicative() && m_tc.is_prop(e).first;
    } catch (exception &) {
        return false;
    }
}

auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide) -> result {
    if (sz == 1) {
        return pp_child(app_arg(e), max_bp()-1, ignore_hide);
    } else if (is_app(e) && is_implicit(app_fn(e))) {
        return pp_coercion_fn(app_fn(e), sz-1, ignore_hide);
    } else {
        expr const & fn = app_fn(e);
        result res_fn   = pp_coercion_fn(fn, sz-1, ignore_hide);
        format fn_fmt   = res_fn.fmt();
        if (m_implict && sz == 2 && has_implicit_args(fn))
            fn_fmt = compose(*g_explicit_fmt, fn_fmt);
        result res_arg  = pp_child(app_arg(e), max_bp(), ignore_hide);
        return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
    }
}

auto pretty_fn::pp_coercion(expr const & e, unsigned bp, bool ignore_hide) -> result {
    buffer<expr> args;
    expr const & f = get_app_args(e, args);
    optional<pair<name, unsigned>> r = is_coercion(m_env, f);
    lean_assert(r);
    if (r->second >= args.size()) {
        return pp_child_core(e, bp, ignore_hide);
    } else if (r->second == args.size() - 1) {
        return pp_child(args.back(), bp, ignore_hide);
    } else {
        unsigned sz = args.size() - r->second;
        lean_assert(sz >= 2);
        auto r = pp_coercion_fn(e, sz, ignore_hide);
        if (r.rbp() < bp) {
            return result(paren(r.fmt()));
        } else {
            return r;
        }
    }
}

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_info(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) || local_pp_name(e_arg) != local_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);
}

bool pretty_fn::ignore_local_ref(expr const & e) {
    expr const & fn = get_app_fn(e);
    return m_full_names && (!is_constant(fn) || !const_name(fn).is_atomic());
}

// 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> {
    if (ignore_local_ref(e))
        return 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();
}

auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result {
    if (auto it = is_abbreviated(e))
        return pp_abbreviation(e, *it, false, bp, ignore_hide);
    if (is_app(e)) {
        if (auto r = pp_local_ref(e))
            return add_paren_if_needed(*r, bp);
        expr const & f = app_fn(e);
        if (auto it = is_abbreviated(f)) {
            return pp_abbreviation(e, *it, true, bp, ignore_hide);
        } else if (is_implicit(f)) {
            return pp_child(f, bp, ignore_hide);
        } else if (!m_coercion && is_coercion(m_env, f)) {
            return pp_coercion(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 {
    if (m_env.impredicative() && e == mk_Prop()) {
        return result(format("Prop"));
    } else if (m_universes) {
        return result(group(format("Type.{") + nest(6, pp_level(sort_level(e))) + format("}")));
    } else {
        return result(format("Type"));
    }
}

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>();
    }
}

optional<name> pretty_fn::is_abbreviated(expr const & e) const {
    if (m_abbreviations)
        return ::lean::is_abbreviated(m_env, e);
    return optional<name>();
}

auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ_params) -> result {
    if (auto it = is_abbreviated(e))
        return pp_abbreviation(e, *it, false);
    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.
    name n = const_name(e);
    if (!m_full_names) {
        if (auto it = is_aliased(n)) {
            if (!m_private_names || !hidden_to_user_name(m_env, n))
                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))) {
                        n = new_n;
                        break;
                    }
                }
            }
        }
    }
    if (!m_private_names) {
        if (auto n1 = hidden_to_user_name(m_env, n))
            n = *n1;
    }
    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(format(n));
            else
                first_idx = *num_ref_univ_params;
        }
        format r = compose(format(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(format(n));
    }
}

auto pretty_fn::pp_meta(expr const & e) -> result {
    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 {
    return result(format(local_pp_name(e)));
}

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;
    }
    name_generator ngen(*g_tmp_prefix);
    try {
        expr type = m_tc.whnf(m_tc.infer(f).first).first;
        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 = mk_local(ngen.next(), binding_name(type), binding_domain(type), binding_info(type));
            type = m_tc.whnf(instantiate(binding_body(type), local)).first;
        }
        return false;
    } catch (exception &) {
        return false;
    }
}

auto pretty_fn::pp_app(expr const & e) -> result {
    if (auto r = pp_local_ref(e))
        return *r;
    expr const & fn = app_fn(e);
    if (auto it = is_abbreviated(fn))
        return pp_abbreviation(e, *it, true);
    // 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) || (!ignore_local_ref(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_block(buffer<name> const & names, expr const & type, binder_info const & bi) {
    format r;
    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));
    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(local_pp_name(local));
    format r;
    for (unsigned i = 1; i < num; i++) {
        expr local = locals[i];
        if (mlocal_type(local) == type && local_info(local) == bi) {
            names.push_back(local_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(local_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 += 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());
        result rhs = pp_child(lift_free_vars(binding_body(e), 1), 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 += 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)); }
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 = local_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  = (binding_info(binding).is_contextual()) ? *g_assert_fmt : *g_have_fmt;
    format r = head_fmt + space() + format(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();<commit_msg>fix(frontends/lean/pp): make pp_have more robust<commit_after>/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <algorithm>
#include <limits>
#include "util/flet.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/scoped_ext.h"
#include "library/coercion.h"
#include "library/expr_pair.h"
#include "library/placeholder.h"
#include "library/private.h"
#include "library/protected.h"
#include "library/explicit.h"
#include "library/typed_expr.h"
#include "library/num.h"
#include "library/util.h"
#include "library/let.h"
#include "library/print.h"
#include "library/abbreviation.h"
#include "library/pp_options.h"
#include "library/constants.h"
#include "library/replace_visitor.h"
#include "library/definitional/equations.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/util.h"
#include "frontends/lean/token_table.h"
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/parser_config.h"
#include "frontends/lean/local_ref_info.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_assert_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 name   * g_tmp_prefix      = nullptr;

class nat_numeral_pp {
    expr m_num_type;
    name m_nat;
    expr m_nat_of_num;
    expr m_zero;
    expr m_succ;
public:
    nat_numeral_pp():
        m_num_type(mk_constant(get_num_name())),
        m_nat(get_nat_name()),
        m_nat_of_num(mk_constant(get_nat_of_num_name())),
        m_zero(mk_constant(get_nat_zero_name())),
        m_succ(mk_constant(get_nat_succ_name())) {
    }

    // Return ture if the environment has a coercion from num->nat
    bool has_coercion_num_nat(environment const & env) const {
        list<expr> coes = get_coercions(env, m_num_type, m_nat);
        if (length(coes) != 1)
            return false;
        return head(coes) == m_nat_of_num;
    }

    // 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_zero) {
                return optional<unsigned>(r);
            } else if (is_app(*it) && app_fn(*it) == m_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 {
                return optional<unsigned>();
            }
        }
    }
};

static nat_numeral_pp * g_nat_numeral_pp = nullptr;

static bool has_coercion_num_nat(environment const & env) {
    return g_nat_numeral_pp->has_coercion_num_nat(env);
}

static optional<unsigned> to_unsigned(expr const & e) {
    return g_nat_numeral_pp->to_unsigned(e);
}

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("\u03BB")));
    g_lambda_fmt      = new format(highlight_keyword(format("fun")));
    g_forall_n_fmt    = new format(highlight_keyword(format("\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("\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_assert_fmt      = new format(highlight_keyword(format("assert")));
    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_tmp_prefix      = new name(name::mk_internal_unique_name());
    g_nat_numeral_pp  = new nat_numeral_pp();
}

void finalize_pp() {
    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_assert_fmt;
    delete g_from_fmt;
    delete g_visible_fmt;
    delete g_show_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) {
    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 = 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_meta(l))
                return some_level(mk_meta_univ(mk_metavar_name(meta_id(l))));
            return none_level();
        });
}

/** \brief Make sure that all metavariables have reasonable names,
    and for all local constants l1 l2, local_pp_name(l1) != local_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.
*/
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 (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)));
            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) {
    m_options         = o;
    bool all          = get_pp_all(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         = all || get_pp_implicit(o);
    m_unicode         = get_pp_unicode(o);
    m_coercion        = all || get_pp_coercions(o);
    m_notation        = !all && get_pp_notation(o);
    m_universes       = all || get_pp_universes(o);
    m_full_names      = all || 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_purify_locals   = get_pp_purify_locals(o);
    m_beta            = !all && get_pp_beta(o);
    m_numerals        = get_pp_numerals(o);
    m_abbreviations   = !all && 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);
}

void pretty_fn::set_options(options const & o) {
    if (is_eqp(o, m_options))
        return;
    set_options_core(o);
}

format pretty_fn::pp_level(level const & l) {
    return ::lean::pp(l, m_unicode, m_indent);
}

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 {
        binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f).first).first);
        return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit();
    } catch (exception &) {
        return false;
    }
}

bool pretty_fn::is_prop(expr const & e) {
    try {
        return m_env.impredicative() && m_tc.is_prop(e).first;
    } catch (exception &) {
        return false;
    }
}

auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide) -> result {
    if (sz == 1) {
        return pp_child(app_arg(e), max_bp()-1, ignore_hide);
    } else if (is_app(e) && is_implicit(app_fn(e))) {
        return pp_coercion_fn(app_fn(e), sz-1, ignore_hide);
    } else {
        expr const & fn = app_fn(e);
        result res_fn   = pp_coercion_fn(fn, sz-1, ignore_hide);
        format fn_fmt   = res_fn.fmt();
        if (m_implict && sz == 2 && has_implicit_args(fn))
            fn_fmt = compose(*g_explicit_fmt, fn_fmt);
        result res_arg  = pp_child(app_arg(e), max_bp(), ignore_hide);
        return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
    }
}

auto pretty_fn::pp_coercion(expr const & e, unsigned bp, bool ignore_hide) -> result {
    buffer<expr> args;
    expr const & f = get_app_args(e, args);
    optional<pair<name, unsigned>> r = is_coercion(m_env, f);
    lean_assert(r);
    if (r->second >= args.size()) {
        return pp_child_core(e, bp, ignore_hide);
    } else if (r->second == args.size() - 1) {
        return pp_child(args.back(), bp, ignore_hide);
    } else {
        unsigned sz = args.size() - r->second;
        lean_assert(sz >= 2);
        auto r = pp_coercion_fn(e, sz, ignore_hide);
        if (r.rbp() < bp) {
            return result(paren(r.fmt()));
        } else {
            return r;
        }
    }
}

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_info(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) || local_pp_name(e_arg) != local_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);
}

bool pretty_fn::ignore_local_ref(expr const & e) {
    expr const & fn = get_app_fn(e);
    return m_full_names && (!is_constant(fn) || !const_name(fn).is_atomic());
}

// 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> {
    if (ignore_local_ref(e))
        return 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();
}

auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result {
    if (auto it = is_abbreviated(e))
        return pp_abbreviation(e, *it, false, bp, ignore_hide);
    if (is_app(e)) {
        if (auto r = pp_local_ref(e))
            return add_paren_if_needed(*r, bp);
        expr const & f = app_fn(e);
        if (auto it = is_abbreviated(f)) {
            return pp_abbreviation(e, *it, true, bp, ignore_hide);
        } else if (is_implicit(f)) {
            return pp_child(f, bp, ignore_hide);
        } else if (!m_coercion && is_coercion(m_env, f)) {
            return pp_coercion(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 {
    if (m_env.impredicative() && e == mk_Prop()) {
        return result(format("Prop"));
    } else if (m_universes) {
        return result(group(format("Type.{") + nest(6, pp_level(sort_level(e))) + format("}")));
    } else {
        return result(format("Type"));
    }
}

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>();
    }
}

optional<name> pretty_fn::is_abbreviated(expr const & e) const {
    if (m_abbreviations)
        return ::lean::is_abbreviated(m_env, e);
    return optional<name>();
}

auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ_params) -> result {
    if (auto it = is_abbreviated(e))
        return pp_abbreviation(e, *it, false);
    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.
    name n = const_name(e);
    if (!m_full_names) {
        if (auto it = is_aliased(n)) {
            if (!m_private_names || !hidden_to_user_name(m_env, n))
                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))) {
                        n = new_n;
                        break;
                    }
                }
            }
        }
    }
    if (!m_private_names) {
        if (auto n1 = hidden_to_user_name(m_env, n))
            n = *n1;
    }
    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(format(n));
            else
                first_idx = *num_ref_univ_params;
        }
        format r = compose(format(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(format(n));
    }
}

auto pretty_fn::pp_meta(expr const & e) -> result {
    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 {
    return result(format(local_pp_name(e)));
}

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;
    }
    name_generator ngen(*g_tmp_prefix);
    try {
        expr type = m_tc.whnf(m_tc.infer(f).first).first;
        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 = mk_local(ngen.next(), binding_name(type), binding_domain(type), binding_info(type));
            type = m_tc.whnf(instantiate(binding_body(type), local)).first;
        }
        return false;
    } catch (exception &) {
        return false;
    }
}

auto pretty_fn::pp_app(expr const & e) -> result {
    if (auto r = pp_local_ref(e))
        return *r;
    expr const & fn = app_fn(e);
    if (auto it = is_abbreviated(fn))
        return pp_abbreviation(e, *it, true);
    // 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) || (!ignore_local_ref(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_block(buffer<name> const & names, expr const & type, binder_info const & bi) {
    format r;
    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));
    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(local_pp_name(local));
    format r;
    for (unsigned i = 1; i < num; i++) {
        expr local = locals[i];
        if (mlocal_type(local) == type && local_info(local) == bi) {
            names.push_back(local_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(local_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 += 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());
        result rhs = pp_child(lift_free_vars(binding_body(e), 1), 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 += 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 = local_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  = (binding_info(binding).is_contextual()) ? *g_assert_fmt : *g_have_fmt;
    format r = head_fmt + space() + format(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();
{'fraction_non_alphanumeric': 0.12958448551884733, 'fraction_numerical': 0.0023650123708339396, 'mean_word_length': 2.755482680877229, 'pattern_counts': {'":': 2, '<': 89, '<?xml version=': 0, '>': 121, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7455225', 'n_tokens_mistral': 19259, 'n_tokens_neox': 18927, 'n_words': 4146}