<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 "util/sstream.h"
#include "library/tactic/proof_state.h"

namespace lean {
format proof_state::pp(formatter const & fmt, options const & opts) const {
    format r;
    bool first = true;
    for (auto const & p : m_goals) {
        if (first)
            first = false;
        else
            r += line();
        r += group(format{format(p.first), colon(), line(), p.second.pp(fmt, opts)});
    }
    return r;
}

void swap(proof_state & s1, proof_state & s2) {
    swap(s1.m_goals, s2.m_goals);
    swap(s1.m_menv, s2.m_menv);
    swap(s1.m_proof_builder, s2.m_proof_builder);
}

static name g_main("main");

proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) {
    auto gfn         = to_goal(env, ctx, t);
    goal g           = gfn.first;
    goal_proof_fn fn = gfn.second;
    proof_builder p  = mk_proof_builder(
        [=](proof_map const & m, environment const &, assignment const &) -> expr {
            expr p = find(m, g_main);
            if (!p)
                throw exception(sstream() << "failed to find proof for '" << g_main << "' goal");
            return fn(p);
        });
    return proof_state(goals(mk_pair(g_main, g)), metavar_env(), p);
}
}
<commit_msg>feat(library/tactic/proof_state): remove goal name when pretty printing the proof state<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 "util/sstream.h"
#include "library/tactic/proof_state.h"

namespace lean {
format proof_state::pp(formatter const & fmt, options const & opts) const {
    format r;
    bool first = true;
    for (auto const & p : m_goals) {
        if (first)
            first = false;
        else
            r += line();
        r += p.second.pp(fmt, opts);
    }
    return r;
}

void swap(proof_state & s1, proof_state & s2) {
    swap(s1.m_goals, s2.m_goals);
    swap(s1.m_menv, s2.m_menv);
    swap(s1.m_proof_builder, s2.m_proof_builder);
}

static name g_main("main");

proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) {
    auto gfn         = to_goal(env, ctx, t);
    goal g           = gfn.first;
    goal_proof_fn fn = gfn.second;
    proof_builder p  = mk_proof_builder(
        [=](proof_map const & m, environment const &, assignment const &) -> expr {
            expr p = find(m, g_main);
            if (!p)
                throw exception(sstream() << "failed to find proof for '" << g_main << "' goal");
            return fn(p);
        });
    return proof_state(goals(mk_pair(g_main, g)), metavar_env(), p);
}
}

{'fraction_non_alphanumeric': 0.12991150442477875, 'fraction_numerical': 0.00991150442477876, 'mean_word_length': 2.6417525773195876, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 7, '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': '4313556', 'n_tokens_mistral': 963, 'n_tokens_neox': 946, 'n_words': 264}