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

Author: <NAME>
*/
#include <vector>
#include "kernel/kernel_exception.h"

namespace lean {
format kernel_exception::pp(formatter const &, options const &) const {
    return format(what());
}

format unknown_name_exception::pp(formatter const &, options const &) const {
    return format{format("unknown object '"), format(get_name()), format("'")};
}

format already_declared_exception::pp(formatter const &, options const &) const {
    return format{format("invalid object declaration, environment already has an object named '"), format(get_name()), format("'")};
}

format has_no_type_exception::pp(formatter const &, options const &) const {
    return format{format("object '"), format(const_name(m_const)), format("' has no type associated with it")};
}

format app_type_mismatch_exception::pp(formatter const & fmt, options const & opts) const {
    unsigned indent     = get_pp_indent(opts);
    context const & ctx = get_context();
    expr const & app    = get_application();
    format app_fmt      = fmt(ctx, app, false, opts);
    std::vector<expr> const & arg_types = get_arg_types();
    auto it = arg_types.begin();
    format f_type_fmt   = fmt(ctx, *it, false, opts);
    format arg_types_fmt;
    ++it;
    for (unsigned i = 1; it != arg_types.end(); ++it, ++i) {
        expr const & a    = arg(app, i);
        format arg_fmt    = fmt(ctx, a, false, opts);
        if (is_pi(a) || is_lambda(a) || is_let(a))
            arg_fmt = paren(arg_fmt);
        format arg_type_fmt = fmt(ctx, *it, false, opts);
        arg_types_fmt += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), arg_type_fmt})})));<commit_msg>fix(kernel/kernel_exception): incorrect pp method<commit_after>/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <vector>
#include "kernel/kernel_exception.h"

namespace lean {
format kernel_exception::pp(formatter const &, options const &) const {
    return format(what());
}

format unknown_name_exception::pp(formatter const &, options const &) const {
    return format{format(what()), format(" '"), format(get_name()), format("'")};
}

format already_declared_exception::pp(formatter const &, options const &) const {
    return format{format("invalid object declaration, environment already has an object named '"), format(get_name()), format("'")};
}

format has_no_type_exception::pp(formatter const &, options const &) const {
    return format{format("object '"), format(const_name(m_const)), format("' has no type associated with it")};
}

format app_type_mismatch_exception::pp(formatter const & fmt, options const & opts) const {
    unsigned indent     = get_pp_indent(opts);
    context const & ctx = get_context();
    expr const & app    = get_application();
    format app_fmt      = fmt(ctx, app, false, opts);
    std::vector<expr> const & arg_types = get_arg_types();
    auto it = arg_types.begin();
    format f_type_fmt   = fmt(ctx, *it, false, opts);
    format arg_types_fmt;
    ++it;
    for (unsigned i = 1; it != arg_types.end(); ++it, ++i) {
        expr const & a    = arg(app, i);
        format arg_fmt    = fmt(ctx, a, false, opts);
        if (is_pi(a) || is_lambda(a) || is_let(a))
            arg_fmt = paren(arg_fmt);
        format arg_type_fmt = fmt(ctx, *it, false, opts);
        arg_types_fmt += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), arg_type_fmt})})));
{'fraction_non_alphanumeric': 0.14405405405405405, 'fraction_numerical': 0.0037837837837837837, 'mean_word_length': 4.249645390070922, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, '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': '102943', 'n_tokens_mistral': 1149, 'n_tokens_neox': 1124, 'n_words': 326}