<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 <utility>
#include <string>
#include <limits>
#include <vector>
#include "util/interrupt.h"
#include "util/script_exception.h"
#include "util/sstream.h"
#include "util/flet.h"
#include "util/lean_path.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/error_msgs.h"
#include "library/parser_nested_exception.h"
#include "library/aliases.h"
#include "library/constants.h"
#include "library/private.h"
#include "library/locals.h"
#include "library/protected.h"
#include "library/choice.h"
#include "library/placeholder.h"
#include "library/deep_copy.h"
#include "library/module.h"
#include "library/scoped_ext.h"
#include "library/explicit.h"
#include "library/typed_expr.h"
#include "library/let.h"
#include "library/num.h"
#include "library/string.h"
#include "library/sorry.h"
#include "library/flycheck.h"
#include "library/pp_options.h"
#include "library/error_handling/error_handling.h"
#include "library/tactic/expr_to_tactic.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/parser_bindings.h"
#include "frontends/lean/notation_cmd.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/parse_rewrite_tactic.h"
#include "frontends/lean/update_environment_exception.h"
#include "frontends/lean/local_ref_info.h"
#include "frontends/lean/opt_cmd.h"

#ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
#define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
#endif

#ifndef LEAN_DEFAULT_PARSER_PARALLEL_IMPORT
#define LEAN_DEFAULT_PARSER_PARALLEL_IMPORT false
#endif

namespace lean {
// ==========================================
// Parser configuration options
static name * g_parser_show_errors;
static name * g_parser_parallel_import;

bool get_parser_show_errors(options const & opts) {
    return opts.get_bool(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS);
}

bool get_parser_parallel_import(options const & opts) {
    return opts.get_bool(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT);
}
// ==========================================

parser::local_scope::local_scope(parser & p, bool save_options):
    m_p(p), m_env(p.env()) {
    m_p.push_local_scope(save_options);
}
parser::local_scope::local_scope(parser & p, environment const & env):
    m_p(p), m_env(p.env()) {
    m_p.m_env = env;
    m_p.push_local_scope();
}
parser::local_scope::local_scope(parser & p, optional<environment> const & env):
    m_p(p), m_env(p.env()) {
    if (env)
        m_p.m_env = *env;
    m_p.push_local_scope();
}
parser::local_scope::~local_scope() {
    m_p.pop_local_scope();
    m_p.m_env = m_env;
}

parser::undef_id_to_const_scope::undef_id_to_const_scope(parser & p):
    flet<undef_id_behavior>(p.m_undef_id_behavior, undef_id_behavior::AssumeConstant) {}
parser::undef_id_to_local_scope::undef_id_to_local_scope(parser & p):
    flet<undef_id_behavior>(p.m_undef_id_behavior, undef_id_behavior::AssumeLocal) {}

static name * g_tmp_prefix = nullptr;

void parser::init_stop_at(options const & opts) {
    unsigned col;
    if (has_show_goal(opts, m_stop_at_line, col)) {
        m_stop_at      = true;
    } else if (has_show_hole(opts, m_stop_at_line, col)) {
        m_stop_at      = true;
    } else {
        m_stop_at      = false;
    }
}

parser::parser(environment const & env, io_state const & ios,
               std::istream & strm, char const * strm_name,
               bool use_exceptions, unsigned num_threads,
               snapshot const * s, snapshot_vector * sv, info_manager * im,
               keep_theorem_mode tmode):
    m_env(env), m_ios(ios), m_ngen(*g_tmp_prefix),
    m_verbose(true), m_use_exceptions(use_exceptions),
    m_scanner(strm, strm_name, s ? s->m_line : 1),
    m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
    m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) {
    m_local_decls_size_at_beg_cmd = 0;
    m_in_backtick = false;
    m_profile     = ios.get_options().get_bool("profile", false);
    init_stop_at(ios.get_options());
    if (num_threads > 1 && m_profile)
        throw exception("option --profile cannot be used when theorems are compiled in parallel");
    m_has_params = false;
    m_keep_theorem_mode = tmode;
    if (s) {
        m_ngen               = s->m_ngen;
        m_local_level_decls  = s->m_lds;
        m_local_decls        = s->m_eds;
        m_level_variables    = s->m_lvars;
        m_variables          = s->m_vars;
        m_include_vars       = s->m_include_vars;
        m_parser_scope_stack = s->m_parser_scope_stack;
    }
    m_num_threads = num_threads;
    m_undef_id_behavior = undef_id_behavior::Error;
    m_found_errors = false;
    m_used_sorry = false;
    updt_options();
    m_next_tag_idx = 0;
    m_curr = scanner::token_kind::Identifier;
    protected_call([&]() { scan(); },
                   [&]() { sync_command(); });
}

parser::~parser() {
    try {
        if (!m_theorem_queue.done()) {
            m_theorem_queue.interrupt();
            m_theorem_queue.join();
        }
    } catch (...) {}
}

void parser::cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
                              level_param_names const & ls, expr const & type, expr const & value) {
    if (m_cache)
        m_cache->add(m_env, n, pre_type, pre_value, ls, type, value);
}

auto parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value)
-> optional<std::tuple<level_param_names, expr, expr>> {
    if (m_cache)
        return m_cache->find(m_env, n, pre_type, pre_value);
    else
        return optional<std::tuple<level_param_names, expr, expr>>();
}

void parser::add_decl_index(name const & n, pos_info const & pos, name const & k, expr const & t) {
    if (m_index)
        m_index->add_decl(get_stream_name(), pos, n, k, t);
}

void parser::add_ref_index(name const & n, pos_info const & pos) {
    if (m_index)
        m_index->add_ref(get_stream_name(), pos, n);
}

void parser::add_abbrev_index(name const & a, name const & d) {
    if (m_index)
        m_index->add_abbrev(a, d);
}

bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const {
    if (!m_info_manager)
        return true; // we are not tracking info
    for (unsigned i = start_line; i <= end_line; i++)
        if (m_info_manager->is_invalidated(i))
            return false;
    return true;
}

void parser::remove_proof_state_info(pos_info const & start, pos_info const & end) {
    if (m_info_manager)<commit_msg>fix(frontends/lean/parser): caching problem when using "show hole" and "show goal" command line options<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 <utility>
#include <string>
#include <limits>
#include <vector>
#include "util/interrupt.h"
#include "util/script_exception.h"
#include "util/sstream.h"
#include "util/flet.h"
#include "util/lean_path.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/error_msgs.h"
#include "library/parser_nested_exception.h"
#include "library/aliases.h"
#include "library/constants.h"
#include "library/private.h"
#include "library/locals.h"
#include "library/protected.h"
#include "library/choice.h"
#include "library/placeholder.h"
#include "library/deep_copy.h"
#include "library/module.h"
#include "library/scoped_ext.h"
#include "library/explicit.h"
#include "library/typed_expr.h"
#include "library/let.h"
#include "library/num.h"
#include "library/string.h"
#include "library/sorry.h"
#include "library/flycheck.h"
#include "library/pp_options.h"
#include "library/error_handling/error_handling.h"
#include "library/tactic/expr_to_tactic.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/parser_bindings.h"
#include "frontends/lean/notation_cmd.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/parse_rewrite_tactic.h"
#include "frontends/lean/update_environment_exception.h"
#include "frontends/lean/local_ref_info.h"
#include "frontends/lean/opt_cmd.h"

#ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
#define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
#endif

#ifndef LEAN_DEFAULT_PARSER_PARALLEL_IMPORT
#define LEAN_DEFAULT_PARSER_PARALLEL_IMPORT false
#endif

namespace lean {
// ==========================================
// Parser configuration options
static name * g_parser_show_errors;
static name * g_parser_parallel_import;

bool get_parser_show_errors(options const & opts) {
    return opts.get_bool(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS);
}

bool get_parser_parallel_import(options const & opts) {
    return opts.get_bool(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT);
}
// ==========================================

parser::local_scope::local_scope(parser & p, bool save_options):
    m_p(p), m_env(p.env()) {
    m_p.push_local_scope(save_options);
}
parser::local_scope::local_scope(parser & p, environment const & env):
    m_p(p), m_env(p.env()) {
    m_p.m_env = env;
    m_p.push_local_scope();
}
parser::local_scope::local_scope(parser & p, optional<environment> const & env):
    m_p(p), m_env(p.env()) {
    if (env)
        m_p.m_env = *env;
    m_p.push_local_scope();
}
parser::local_scope::~local_scope() {
    m_p.pop_local_scope();
    m_p.m_env = m_env;
}

parser::undef_id_to_const_scope::undef_id_to_const_scope(parser & p):
    flet<undef_id_behavior>(p.m_undef_id_behavior, undef_id_behavior::AssumeConstant) {}
parser::undef_id_to_local_scope::undef_id_to_local_scope(parser & p):
    flet<undef_id_behavior>(p.m_undef_id_behavior, undef_id_behavior::AssumeLocal) {}

static name * g_tmp_prefix = nullptr;

void parser::init_stop_at(options const & opts) {
    unsigned col;
    if (has_show_goal(opts, m_stop_at_line, col)) {
        m_stop_at      = true;
    } else if (has_show_hole(opts, m_stop_at_line, col)) {
        m_stop_at      = true;
    } else {
        m_stop_at      = false;
    }
}

parser::parser(environment const & env, io_state const & ios,
               std::istream & strm, char const * strm_name,
               bool use_exceptions, unsigned num_threads,
               snapshot const * s, snapshot_vector * sv, info_manager * im,
               keep_theorem_mode tmode):
    m_env(env), m_ios(ios), m_ngen(*g_tmp_prefix),
    m_verbose(true), m_use_exceptions(use_exceptions),
    m_scanner(strm, strm_name, s ? s->m_line : 1),
    m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
    m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) {
    m_local_decls_size_at_beg_cmd = 0;
    m_in_backtick = false;
    m_profile     = ios.get_options().get_bool("profile", false);
    init_stop_at(ios.get_options());
    if (num_threads > 1 && m_profile)
        throw exception("option --profile cannot be used when theorems are compiled in parallel");
    m_has_params = false;
    m_keep_theorem_mode = tmode;
    if (s) {
        m_ngen               = s->m_ngen;
        m_local_level_decls  = s->m_lds;
        m_local_decls        = s->m_eds;
        m_level_variables    = s->m_lvars;
        m_variables          = s->m_vars;
        m_include_vars       = s->m_include_vars;
        m_parser_scope_stack = s->m_parser_scope_stack;
    }
    m_num_threads = num_threads;
    m_undef_id_behavior = undef_id_behavior::Error;
    m_found_errors = false;
    m_used_sorry = false;
    updt_options();
    m_next_tag_idx = 0;
    m_curr = scanner::token_kind::Identifier;
    protected_call([&]() { scan(); },
                   [&]() { sync_command(); });
}

parser::~parser() {
    try {
        if (!m_theorem_queue.done()) {
            m_theorem_queue.interrupt();
            m_theorem_queue.join();
        }
    } catch (...) {}
}

void parser::cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
                              level_param_names const & ls, expr const & type, expr const & value) {
    if (m_cache)
        m_cache->add(m_env, n, pre_type, pre_value, ls, type, value);
}

auto parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value)
-> optional<std::tuple<level_param_names, expr, expr>> {
    if (m_cache)
        return m_cache->find(m_env, n, pre_type, pre_value);
    else
        return optional<std::tuple<level_param_names, expr, expr>>();
}

void parser::add_decl_index(name const & n, pos_info const & pos, name const & k, expr const & t) {
    if (m_index)
        m_index->add_decl(get_stream_name(), pos, n, k, t);
}

void parser::add_ref_index(name const & n, pos_info const & pos) {
    if (m_index)
        m_index->add_ref(get_stream_name(), pos, n);
}

void parser::add_abbrev_index(name const & a, name const & d) {
    if (m_index)
        m_index->add_abbrev(a, d);
}

bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const {
    if (m_stop_at) {
        if (start_line <= m_stop_at_line && m_stop_at_line <= end_line)
            return false;
    }
    if (m_info_manager) {
        // we are tracking info
        for (unsigned i = start_line; i <= end_line; i++)
            if (m_info_manager->is_invalidated(i))
                return false;
    }
    return true;
}

void parser::remove_proof_state_info(pos_info const & start, pos_info const & end) {
    if (m_info_manager)
{'fraction_non_alphanumeric': 0.13619763694951664, 'fraction_numerical': 0.001861797350519155, 'mean_word_length': 3.987857142857143, 'pattern_counts': {'":': 0, '<': 31, '<?xml version=': 0, '>': 61, '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': '3491404', 'n_tokens_mistral': 5012, 'n_tokens_neox': 4981, 'n_words': 947}