1e6b3614ab
@Kha, we now support variable/constant shadowing in patterns.
A constant may occur in a pattern if it is a constructor or tagged with
the new [pattern] attribute. In the standard library, I have tagged
'add', 'zero', 'one', 'bit0', 'bit1' and 'rfl' with this new attribute.
BTW, arbitrary constants and variables may occur nested in type ascriptions and
inaccessible terms.
Here is an example:
meta_definition tactic_result_to_string {A : Type} : tactic_result A → string
| (success a s) := to_string a
| (exception ⌞A⌟ e s) := "Exception: " ++ to_string (e ())
I had to use the inaccessible ⌞A⌟ in the example above, otherwise, we would be shadowing the parameter
{A : Type}, and we would get a type error.
The new validation is performed at to_pattern_fn (parser.cpp).
2535 lines
88 KiB
C++
2535 lines
88 KiB
C++
/*
|
|
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 <string>
|
|
#include <limits>
|
|
#include <vector>
|
|
#include <util/utf8.h>
|
|
#include <library/export_decl.h>
|
|
#include "util/interrupt.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/find_fn.h"
|
|
#include "kernel/abstract.h"
|
|
#include "kernel/instantiate.h"
|
|
#include "kernel/error_msgs.h"
|
|
#include "library/trace.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/local_context.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/noncomputable.h"
|
|
#include "library/error_handling.h"
|
|
#include "library/scope_pos_info_provider.h"
|
|
#include "library/legacy_type_context.h"
|
|
#include "library/definitional/equations.h"
|
|
#include "frontends/lean/tokens.h"
|
|
#include "frontends/lean/parser.h"
|
|
#include "frontends/lean/util.h"
|
|
#include "frontends/lean/notation_cmd.h"
|
|
#include "frontends/lean/info_annotation.h"
|
|
#include "frontends/lean/parser_pos_provider.h"
|
|
#include "frontends/lean/update_environment_exception.h"
|
|
#include "frontends/lean/local_ref_info.h"
|
|
#include "frontends/lean/opt_cmd.h"
|
|
#include "frontends/lean/builtin_cmds.h"
|
|
#include "frontends/lean/prenum.h"
|
|
#include "frontends/lean/elaborator.h"
|
|
#include "frontends/lean/pattern_attribute.h"
|
|
// LEGACY
|
|
#include "frontends/lean/old_elaborator.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;
|
|
static name * g_new_elaborator;
|
|
|
|
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);
|
|
}
|
|
|
|
bool get_new_elaborator(options const & opts) {
|
|
return opts.get_bool(*g_new_elaborator, false);
|
|
}
|
|
// ==========================================
|
|
|
|
static name * g_anonymous_inst_name_prefix = nullptr;
|
|
|
|
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::quote_scope::quote_scope(parser & p, bool q):
|
|
m_p(p), m_id_behavior(m_p.m_id_behavior), m_in_quote(q) {
|
|
if (q) {
|
|
lean_assert(!m_p.m_in_quote);
|
|
m_p.m_id_behavior = id_behavior::AssumeLocalIfUndef;
|
|
m_p.m_in_quote = true;
|
|
m_p.push_local_scope(false);
|
|
m_p.m_quote_stack = cons(m_p.mk_parser_scope(), m_p.m_quote_stack);
|
|
m_p.clear_locals();
|
|
} else {
|
|
lean_assert(m_p.m_in_quote);
|
|
lean_assert(m_p.m_quote_stack);
|
|
m_p.m_id_behavior = id_behavior::ErrorIfUndef;
|
|
m_p.push_local_scope(false);
|
|
m_p.m_in_quote = false;
|
|
m_p.restore_parser_scope(head(m_p.m_quote_stack));
|
|
}
|
|
}
|
|
|
|
parser::quote_scope::~quote_scope() {
|
|
if (m_in_quote) {
|
|
lean_assert(m_p.m_in_quote);
|
|
m_p.m_in_quote = false;
|
|
m_p.pop_local_scope();
|
|
m_p.m_quote_stack = tail(m_p.m_quote_stack);
|
|
} else {
|
|
lean_assert(!m_p.m_in_quote);
|
|
m_p.m_in_quote = true;
|
|
m_p.pop_local_scope();
|
|
}
|
|
m_p.m_id_behavior = m_id_behavior;
|
|
}
|
|
|
|
parser::undef_id_to_const_scope::undef_id_to_const_scope(parser & p):
|
|
flet<id_behavior>(p.m_id_behavior, id_behavior::AssumeConstantIfUndef) {}
|
|
parser::undef_id_to_local_scope::undef_id_to_local_scope(parser & p):
|
|
flet<id_behavior>(p.m_id_behavior, id_behavior::AssumeLocalIfUndef) {}
|
|
parser::error_if_undef_scope::error_if_undef_scope(parser & p):
|
|
flet<id_behavior>(p.m_id_behavior, id_behavior::ErrorIfUndef) {}
|
|
parser::all_id_local_scope::all_id_local_scope(parser & p):
|
|
flet<id_behavior>(p.m_id_behavior, id_behavior::AllLocal) {}
|
|
|
|
static name * g_tmp_prefix = nullptr;
|
|
|
|
void parser::init_stop_at(options const & opts) {
|
|
unsigned col;
|
|
m_info_at = false;
|
|
m_stop_at = false;
|
|
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 if (has_show_info(opts, m_info_at_line, m_info_at_col)) {
|
|
m_info_at = true;
|
|
m_stop_at = true;
|
|
m_stop_at_line = m_info_at_line;
|
|
}
|
|
}
|
|
|
|
parser::parser(environment const & env, io_state const & ios,
|
|
std::istream & strm, char const * strm_name, optional<std::string> const & base_dir,
|
|
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_verbose(true), m_use_exceptions(use_exceptions),
|
|
m_scanner(strm, strm_name, s ? s->m_line : 1),
|
|
m_base_dir(base_dir),
|
|
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_ignore_noncomputable = 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_in_quote = false;
|
|
m_has_params = false;
|
|
m_keep_theorem_mode = tmode;
|
|
if (s) {
|
|
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_id_behavior = id_behavior::ErrorIfUndef;
|
|
m_found_errors = false;
|
|
m_used_sorry = false;
|
|
updt_options();
|
|
m_next_tag_idx = 0;
|
|
m_next_inst_idx = 1;
|
|
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::scan() {
|
|
if (m_info_at) {
|
|
m_curr = m_scanner.scan(m_env);
|
|
pos_info p = pos();
|
|
if (p.first == m_info_at_line) {
|
|
if (curr_is_identifier()) {
|
|
name const & id = get_name_val();
|
|
if (p.second <= m_info_at_col && m_info_at_col < p.second + id.utf8_size()) {
|
|
print_lean_info_header(m_ios.get_regular_stream());
|
|
bool ok = true;
|
|
try {
|
|
bool show_value = false;
|
|
ok = print_id_info(*this, id, show_value, p);
|
|
} catch (exception &) {
|
|
ok = false;
|
|
}
|
|
if (!ok)
|
|
m_ios.get_regular_stream() << "unknown identifier '" << id << "'\n";
|
|
print_lean_info_footer(m_ios.get_regular_stream());
|
|
m_info_at = false;
|
|
}
|
|
} else if (curr_is_keyword()) {
|
|
name const & tk = get_token_info().token();
|
|
if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.utf8_size()) {
|
|
print_lean_info_header(m_ios.get_regular_stream());
|
|
try {
|
|
print_token_info(*this, tk);
|
|
} catch (exception &) {}
|
|
print_lean_info_footer(m_ios.get_regular_stream());
|
|
m_info_at = false;
|
|
}
|
|
} else if (curr_is_command()) {
|
|
name const & tk = get_token_info().token();
|
|
if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.utf8_size()) {
|
|
print_lean_info_header(m_ios.get_regular_stream());
|
|
m_ios.get_regular_stream() << "'" << tk << "' is a command\n";
|
|
print_lean_info_footer(m_ios.get_regular_stream());
|
|
m_info_at = false;
|
|
}
|
|
}
|
|
}
|
|
} else {
|
|
m_curr = m_scanner.scan(m_env);
|
|
}
|
|
}
|
|
|
|
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, bool is_trusted) {
|
|
if (m_cache)
|
|
m_cache->add(m_env, n, pre_type, pre_value, ls, type, value, is_trusted);
|
|
}
|
|
|
|
auto parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value, bool is_trusted)
|
|
-> optional<std::tuple<level_param_names, expr, expr>> {
|
|
if (m_cache)
|
|
return m_cache->find(m_env, n, pre_type, pre_value, is_trusted);
|
|
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)
|
|
// m_info_manager->remove_proof_state_info(start.first, start.second, end.first, end.second);
|
|
}
|
|
|
|
expr parser::mk_sorry(pos_info const & p) {
|
|
m_used_sorry = true;
|
|
{
|
|
#ifndef LEAN_IGNORE_SORRY
|
|
// TODO(Leo): remove the #ifdef.
|
|
// The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
|
|
// We use it to avoid a buch of warnings on cdash.
|
|
flycheck_warning wrn(m_ios);
|
|
display_warning_pos(p.first, p.second);
|
|
m_ios.get_regular_stream() << " using 'sorry'" << std::endl;
|
|
#endif
|
|
}
|
|
return save_pos(::lean::mk_sorry(), p);
|
|
}
|
|
|
|
void parser::declare_sorry() {
|
|
m_used_sorry = true;
|
|
m_env = ::lean::declare_sorry(m_env);
|
|
}
|
|
|
|
void parser::updt_options() {
|
|
m_verbose = get_verbose(m_ios.get_options());
|
|
m_show_errors = get_parser_show_errors(m_ios.get_options());
|
|
m_new_elaborator = get_new_elaborator(m_ios.get_options());
|
|
try {
|
|
set_max_memory_megabyte(get_max_memory(m_ios.get_options()));
|
|
} catch (exception&) {
|
|
if (m_ios.get_options().contains(get_max_memory_opt_name())) {
|
|
static bool m_already_reported = false;
|
|
if (!m_already_reported) {
|
|
m_already_reported = true;
|
|
throw;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
void parser::display_warning_pos(unsigned line, unsigned pos) {
|
|
legacy_type_context tc(env(), get_options());
|
|
auto out = regular(env(), ios(), tc);
|
|
::lean::display_warning_pos(out, get_stream_name().c_str(), line, pos);
|
|
}
|
|
void parser::display_warning_pos(pos_info p) { display_warning_pos(p.first, p.second); }
|
|
|
|
void parser::display_information_pos(pos_info pos) {
|
|
::lean::display_information_pos(ios().get_regular_stream(), get_options(),
|
|
get_stream_name().c_str(), pos.first, pos.second);
|
|
}
|
|
|
|
void parser::display_error_pos(unsigned line, unsigned pos) {
|
|
::lean::display_error_pos(ios().get_regular_stream(), get_options(),
|
|
get_stream_name().c_str(), line, pos);
|
|
}
|
|
void parser::display_error_pos(pos_info p) { display_error_pos(p.first, p.second); }
|
|
|
|
void parser::display_error(char const * msg, unsigned line, unsigned pos) {
|
|
flycheck_error err(ios());
|
|
display_error_pos(line, pos);
|
|
ios().get_regular_stream() << " " << msg << std::endl;
|
|
}
|
|
|
|
void parser::display_error(char const * msg, pos_info p) { display_error(msg, p.first, p.second); }
|
|
|
|
void parser::display_error(throwable const & ex) {
|
|
legacy_type_context tc(env(), get_options());
|
|
auto out = regular(env(), ios(), tc);
|
|
::lean::display_error(out, this, ex);
|
|
}
|
|
|
|
void parser::throw_parser_exception(char const * msg, pos_info p) {
|
|
throw parser_exception(msg, get_stream_name().c_str(), p.first, p.second);
|
|
}
|
|
|
|
void parser::throw_nested_exception(throwable const & ex, pos_info p) {
|
|
throw parser_nested_exception(std::shared_ptr<throwable>(ex.clone()),
|
|
std::make_shared<parser_pos_provider>(m_pos_table, get_stream_name(), p));
|
|
}
|
|
|
|
#define CATCH(ShowError, ThrowError) \
|
|
save_pre_info_data(); \
|
|
m_found_errors = true; \
|
|
if (!m_use_exceptions && m_show_errors) { ShowError ; } \
|
|
sync(); \
|
|
if (m_use_exceptions) { ThrowError ; }
|
|
|
|
void parser::protected_call(std::function<void()> && f, std::function<void()> && sync) {
|
|
try {
|
|
try {
|
|
f();
|
|
} catch (update_environment_exception & ex) {
|
|
m_env = ex.get_env();
|
|
ex.get_exception().rethrow();
|
|
}
|
|
} catch (parser_exception & ex) {
|
|
CATCH(flycheck_error err(ios()); ios().get_regular_stream() << ex.what() << std::endl,
|
|
throw);
|
|
} catch (parser_error & ex) {
|
|
CATCH(display_error(ex.what(), ex.m_pos),
|
|
throw_parser_exception(ex.what(), ex.m_pos));
|
|
} catch (interrupted & ex) {
|
|
save_pre_info_data();
|
|
reset_interrupt();
|
|
if (m_verbose)
|
|
ios().get_regular_stream() << "!!!Interrupted!!!" << std::endl;
|
|
sync();
|
|
if (m_use_exceptions || m_info_manager)
|
|
throw;
|
|
} catch (throwable & ex) {
|
|
reset_interrupt();
|
|
CATCH(display_error(ex), throw_nested_exception(ex, m_last_cmd_pos));
|
|
}
|
|
}
|
|
|
|
void parser::sync_command() {
|
|
// Keep consuming tokens until we find a Command or End-of-file
|
|
while (curr() != scanner::token_kind::CommandKeyword && curr() != scanner::token_kind::Eof)
|
|
next();
|
|
if (m_info_manager)
|
|
m_info_manager->commit_upto(m_scanner.get_line()+1, false);
|
|
}
|
|
|
|
tag parser::get_tag(expr e) {
|
|
tag t = e.get_tag();
|
|
if (t == nulltag) {
|
|
t = m_next_tag_idx;
|
|
e.set_tag(t);
|
|
m_next_tag_idx++;
|
|
}
|
|
return t;
|
|
}
|
|
|
|
name parser::mk_anonymous_inst_name() {
|
|
name n = g_anonymous_inst_name_prefix->append_after(m_next_inst_idx);
|
|
m_next_inst_idx++;
|
|
return n;
|
|
}
|
|
|
|
bool parser::is_anonymous_inst_name(name const & n) const {
|
|
return
|
|
n.is_atomic() &&
|
|
n.is_string() &&
|
|
strlen(n.get_string()) >= strlen(g_anonymous_inst_name_prefix->get_string()) &&
|
|
memcmp(n.get_string(), g_anonymous_inst_name_prefix->get_string(), strlen(g_anonymous_inst_name_prefix->get_string())) == 0;
|
|
}
|
|
|
|
expr parser::save_pos(expr e, pos_info p) {
|
|
auto t = get_tag(e);
|
|
if (!m_pos_table.contains(t))
|
|
m_pos_table.insert(t, p);
|
|
return e;
|
|
}
|
|
|
|
expr parser::update_pos(expr e, pos_info p) {
|
|
auto t = get_tag(e);
|
|
m_pos_table.insert(t, p);
|
|
return e;
|
|
}
|
|
|
|
expr parser::rec_save_pos(expr const & e, pos_info p) {
|
|
unsigned m = std::numeric_limits<unsigned>::max();
|
|
pos_info dummy(m, 0);
|
|
for_each(e, [&](expr const & e, unsigned) {
|
|
if (pos_of(e, dummy).first == m) {
|
|
save_pos(e, p);
|
|
return true;
|
|
} else {
|
|
return false;
|
|
}
|
|
});
|
|
return e;
|
|
}
|
|
|
|
/** \brief Create a copy of \c e, and the position of new expression with p */
|
|
expr parser::copy_with_new_pos(expr const & e, pos_info p) {
|
|
if (is_let_value(e))
|
|
return e;
|
|
switch (e.kind()) {
|
|
case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta:
|
|
case expr_kind::Local: case expr_kind::Var:
|
|
return save_pos(copy(e), p);
|
|
case expr_kind::App:
|
|
return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
|
|
copy_with_new_pos(app_arg(e), p)),
|
|
p);
|
|
case expr_kind::Lambda: case expr_kind::Pi:
|
|
return save_pos(update_binding(e,
|
|
copy_with_new_pos(binding_domain(e), p),
|
|
copy_with_new_pos(binding_body(e), p)),
|
|
p);
|
|
case expr_kind::Let:
|
|
return save_pos(update_let(e,
|
|
copy_with_new_pos(let_type(e), p),
|
|
copy_with_new_pos(let_value(e), p),
|
|
copy_with_new_pos(let_body(e), p)),
|
|
p);
|
|
case expr_kind::Macro: {
|
|
buffer<expr> args;
|
|
for (unsigned i = 0; i < macro_num_args(e); i++)
|
|
args.push_back(copy_with_new_pos(macro_arg(e, i), p));
|
|
return save_pos(update_macro(e, args.size(), args.data()), p);
|
|
}}
|
|
lean_unreachable(); // LCOV_EXCL_LINE
|
|
}
|
|
|
|
pos_info parser::pos_of(expr const & e, pos_info default_pos) const {
|
|
tag t = e.get_tag();
|
|
if (t == nulltag)
|
|
return default_pos;
|
|
if (auto it = m_pos_table.find(t))
|
|
return *it;
|
|
else
|
|
return default_pos;
|
|
}
|
|
|
|
bool parser::curr_is_token(name const & tk) const {
|
|
return
|
|
(curr() == scanner::token_kind::Keyword || curr() == scanner::token_kind::CommandKeyword) &&
|
|
get_token_info().value() == tk;
|
|
}
|
|
|
|
bool parser::curr_is_token_or_id(name const & tk) const {
|
|
if (curr() == scanner::token_kind::Keyword || curr() == scanner::token_kind::CommandKeyword)
|
|
return get_token_info().value() == tk;
|
|
else if (curr() == scanner::token_kind::Identifier)
|
|
return get_name_val() == tk;
|
|
else
|
|
return false;
|
|
}
|
|
|
|
void parser::check_token_next(name const & tk, char const * msg) {
|
|
if (!curr_is_token(tk))
|
|
throw parser_error(msg, pos());
|
|
next();
|
|
}
|
|
|
|
void parser::check_token_or_id_next(name const & tk, char const * msg) {
|
|
if (!curr_is_token_or_id(tk))
|
|
throw parser_error(msg, pos());
|
|
next();
|
|
}
|
|
|
|
name parser::check_id_next(char const * msg) {
|
|
if (!curr_is_identifier())
|
|
throw parser_error(msg, pos());
|
|
name r = get_name_val();
|
|
next();
|
|
return r;
|
|
}
|
|
|
|
static void check_not_internal(name const & id, pos_info const & p) {
|
|
if (is_internal_name(id))
|
|
throw parser_error(sstream() << "invalid declaration name '" << id << "', identifiers starting with '_' are reserved to the system", p);
|
|
}
|
|
|
|
name parser::check_decl_id_next(char const * msg) {
|
|
auto p = pos();
|
|
name id = check_id_next(msg);
|
|
check_not_internal(id, p);
|
|
return id;
|
|
}
|
|
|
|
name parser::check_atomic_id_next(char const * msg) {
|
|
auto p = pos();
|
|
name id = check_id_next(msg);
|
|
if (!id.is_atomic())
|
|
throw parser_error(msg, p);
|
|
return id;
|
|
}
|
|
|
|
name parser::check_atomic_decl_id_next(char const * msg) {
|
|
auto p = pos();
|
|
name id = check_atomic_id_next(msg);
|
|
check_not_internal(id, p);
|
|
return id;
|
|
}
|
|
|
|
expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
|
|
return save_pos(::lean::mk_app(fn, arg), p);
|
|
}
|
|
|
|
expr parser::mk_app(std::initializer_list<expr> const & args, pos_info const & p) {
|
|
lean_assert(args.size() >= 2);
|
|
auto it = args.begin();
|
|
expr r = *it;
|
|
it++;
|
|
for (; it != args.end(); it++)
|
|
r = mk_app(r, *it, p);
|
|
return r;
|
|
}
|
|
|
|
parser_scope parser::mk_parser_scope(optional<options> const & opts) {
|
|
return parser_scope(opts, m_level_variables, m_variables, m_include_vars,
|
|
m_undef_ids.size(), m_next_inst_idx, m_has_params,
|
|
m_local_level_decls, m_local_decls);
|
|
}
|
|
|
|
void parser::restore_parser_scope(parser_scope const & s) {
|
|
if (s.m_options) {
|
|
m_ios.set_options(*s.m_options);
|
|
updt_options();
|
|
}
|
|
m_local_level_decls = s.m_local_level_decls;
|
|
m_local_decls = s.m_local_decls;
|
|
m_level_variables = s.m_level_variables;
|
|
m_variables = s.m_variables;
|
|
m_include_vars = s.m_include_vars;
|
|
m_has_params = s.m_has_params;
|
|
m_next_inst_idx = s.m_next_inst_idx;
|
|
}
|
|
|
|
void parser::push_local_scope(bool save_options) {
|
|
optional<options> opts;
|
|
if (save_options)
|
|
opts = m_ios.get_options();
|
|
m_parser_scope_stack = cons(mk_parser_scope(opts), m_parser_scope_stack);
|
|
}
|
|
|
|
void parser::pop_local_scope() {
|
|
if (!m_parser_scope_stack) {
|
|
throw parser_error("invalid 'end', there is no open namespace/section", pos());
|
|
}
|
|
auto s = head(m_parser_scope_stack);
|
|
restore_parser_scope(s);
|
|
m_undef_ids.shrink(s.m_num_undef_ids);
|
|
m_parser_scope_stack = tail(m_parser_scope_stack);
|
|
}
|
|
|
|
void parser::clear_locals() {
|
|
m_local_level_decls = local_level_decls();
|
|
m_local_decls = local_expr_decls();
|
|
}
|
|
|
|
void parser::add_local_level(name const & n, level const & l, bool is_variable) {
|
|
if (m_env.is_universe(n))
|
|
throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a global universe");
|
|
if (m_local_level_decls.contains(n))
|
|
throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a local universe");
|
|
m_local_level_decls.insert(n, l);
|
|
if (is_variable) {
|
|
lean_assert(is_param(l));
|
|
m_level_variables.insert(n);
|
|
}
|
|
}
|
|
|
|
void parser::add_local_expr(name const & n, expr const & p, bool is_variable) {
|
|
m_local_decls.insert(n, p);
|
|
if (is_variable) {
|
|
lean_assert(is_local(p));
|
|
m_variables.insert(local_pp_name(p));
|
|
}
|
|
}
|
|
|
|
environment parser::add_local_ref(environment const & env, name const & n, expr const & ref) {
|
|
add_local_expr(n, ref, false);
|
|
if (is_as_atomic(ref)) {
|
|
buffer<expr> args;
|
|
expr f = get_app_args(get_as_atomic_arg(ref), args);
|
|
if (is_explicit(f))
|
|
f = get_explicit_arg(f);
|
|
if (is_constant(f)) {
|
|
return save_local_ref_info(env, const_name(f), ref);
|
|
} else {
|
|
return env;
|
|
}
|
|
} else if (is_constant(ref) && const_levels(ref)) {
|
|
return save_local_ref_info(env, const_name(ref), ref);
|
|
} else {
|
|
return env;
|
|
}
|
|
}
|
|
|
|
static void check_no_metavars(name const & n, expr const & e) {
|
|
lean_assert(is_local(e));
|
|
if (has_metavar(e)) {
|
|
throw_generic_exception(none_expr(), [=](formatter const & fmt) {
|
|
format r("failed to add declaration '");
|
|
r += format(n);
|
|
r += format("' to local context, type has metavariables");
|
|
r += pp_until_meta_visible(fmt, mlocal_type(e));
|
|
return r;
|
|
});
|
|
}
|
|
}
|
|
|
|
void parser::add_variable(name const & n, expr const & v) {
|
|
lean_assert(is_local(v));
|
|
check_no_metavars(n, v);
|
|
add_local_expr(n, v, true);
|
|
}
|
|
|
|
void parser::add_parameter(name const & n, expr const & p) {
|
|
lean_assert(is_local(p));
|
|
check_no_metavars(n, p);
|
|
add_local_expr(n, p, false);
|
|
m_has_params = true;
|
|
}
|
|
|
|
bool parser::update_local_binder_info(name const & n, binder_info const & bi) {
|
|
auto it = get_local(n);
|
|
if (!it || !is_local(*it)) return false;
|
|
|
|
buffer<pair<name, expr>> entries;
|
|
to_buffer(m_local_decls.get_entries(), entries);
|
|
std::reverse(entries.begin(), entries.end());
|
|
unsigned idx = m_local_decls.find_idx(n);
|
|
lean_assert(idx > 0);
|
|
lean_assert_eq(entries[idx-1].second, *it);
|
|
|
|
buffer<expr> old_locals;
|
|
buffer<expr> new_locals;
|
|
old_locals.push_back(*it);
|
|
expr new_l = update_local(*it, bi);
|
|
entries[idx-1].second = new_l;
|
|
new_locals.push_back(new_l);
|
|
|
|
for (unsigned i = idx; i < entries.size(); i++) {
|
|
expr const & curr_e = entries[i].second;
|
|
expr r = is_local(curr_e) ? mlocal_type(curr_e) : curr_e;
|
|
if (std::any_of(old_locals.begin(), old_locals.end(), [&](expr const & l) { return depends_on(r, l); })) {
|
|
r = instantiate_rev(abstract_locals(r, old_locals.size(), old_locals.data()),
|
|
new_locals.size(), new_locals.data());
|
|
if (is_local(curr_e)) {
|
|
expr new_e = update_mlocal(curr_e, r);
|
|
entries[i].second = new_e;
|
|
old_locals.push_back(curr_e);
|
|
new_locals.push_back(new_e);
|
|
} else {
|
|
entries[i].second = r;
|
|
}
|
|
}
|
|
}
|
|
auto new_entries = m_local_decls.get_entries();
|
|
unsigned sz_to_updt = entries.size() - idx + 1;
|
|
for (unsigned i = 0; i < sz_to_updt; i++)
|
|
new_entries = tail(new_entries); // remove entries that will be updated
|
|
for (unsigned i = idx-1; i < entries.size(); i++)
|
|
new_entries = cons(entries[i], new_entries);
|
|
m_local_decls.update_entries(new_entries);
|
|
return true;
|
|
}
|
|
|
|
unsigned parser::get_local_index(name const & n) const {
|
|
return m_local_decls.find_idx(n);
|
|
}
|
|
|
|
void parser::get_include_variables(buffer<expr> & vars) const {
|
|
m_include_vars.for_each([&](name const & n) {
|
|
vars.push_back(*get_local(n));
|
|
});
|
|
}
|
|
|
|
list<expr> parser::locals_to_context() const {
|
|
return map_filter<expr>(m_local_decls.get_entries(),
|
|
[](pair<name, expr> const & p, expr & out) {
|
|
out = p.second;
|
|
return is_local(p.second);
|
|
});
|
|
}
|
|
|
|
static unsigned g_level_add_prec = 10;
|
|
static unsigned g_level_cup_prec = 5;
|
|
|
|
unsigned parser::get_small_nat() {
|
|
mpz val = get_num_val().get_numerator();
|
|
lean_assert(val >= 0);
|
|
if (!val.is_unsigned_int())
|
|
throw parser_error("invalid level expression, value does not fit in a machine integer", pos());
|
|
return val.get_unsigned_int();
|
|
}
|
|
|
|
unsigned parser::parse_small_nat() {
|
|
if (!curr_is_numeral())
|
|
throw parser_error("(small) natural number expected", pos());
|
|
unsigned r = get_small_nat();
|
|
next();
|
|
return r;
|
|
}
|
|
|
|
double parser::parse_double() {
|
|
if (curr() != scanner::token_kind::Decimal)
|
|
throw parser_error("decimal value expected", pos());
|
|
double r =get_num_val().get_double();
|
|
next();
|
|
return r;
|
|
}
|
|
|
|
static level lift(level l, unsigned k) {
|
|
while (k > 0) {
|
|
k--;
|
|
l = mk_succ(l);
|
|
}
|
|
return l;
|
|
}
|
|
|
|
unsigned parser::curr_level_lbp() const {
|
|
if (curr_is_token(get_cup_tk()))
|
|
return g_level_cup_prec;
|
|
else if (curr_is_token(get_add_tk()))
|
|
return g_level_add_prec;
|
|
else
|
|
return 0;
|
|
}
|
|
|
|
level parser::parse_max_imax(bool is_max) {
|
|
auto p = pos();
|
|
next();
|
|
buffer<level> lvls;
|
|
while (curr_is_identifier() || curr_is_numeral() || curr_is_token(get_lparen_tk())) {
|
|
lvls.push_back(parse_level());
|
|
}
|
|
if (lvls.size() < 2)
|
|
throw parser_error("invalid level expression, max must have at least two arguments", p);
|
|
unsigned i = lvls.size() - 1;
|
|
level r = lvls[i];
|
|
while (i > 0) {
|
|
--i;
|
|
if (is_max)
|
|
r = mk_max(lvls[i], r);
|
|
else
|
|
r = mk_imax(lvls[i], r);
|
|
}
|
|
return r;
|
|
}
|
|
|
|
level parser::parse_level_id() {
|
|
auto p = pos();
|
|
name id = get_name_val();
|
|
next();
|
|
if (auto it = m_local_level_decls.find(id))
|
|
return *it;
|
|
|
|
for (name const & ns : get_namespaces(m_env)) {
|
|
auto new_id = ns + id;
|
|
if (!ns.is_anonymous() && m_env.is_universe(new_id))
|
|
return mk_global_univ(new_id);
|
|
}
|
|
|
|
if (m_env.is_universe(id))
|
|
return mk_global_univ(id);
|
|
if (auto it = get_level_alias(m_env, id))
|
|
return mk_global_univ(*it);
|
|
throw parser_error(sstream() << "unknown universe '" << id << "'", p);
|
|
}
|
|
|
|
level parser::parse_level_nud() {
|
|
if (curr_is_token_or_id(get_max_tk())) {
|
|
return parse_max_imax(true);
|
|
} else if (curr_is_token_or_id(get_imax_tk())) {
|
|
return parse_max_imax(false);
|
|
} else if (curr_is_token_or_id(get_placeholder_tk())) {
|
|
next();
|
|
return mk_level_placeholder();
|
|
} else if (curr_is_token(get_lparen_tk())) {
|
|
next();
|
|
level l = parse_level();
|
|
check_token_next(get_rparen_tk(), "invalid level expression, ')' expected");
|
|
return l;
|
|
} else if (curr_is_numeral()) {
|
|
unsigned k = parse_small_nat();
|
|
return lift(level(), k);
|
|
} else if (curr_is_identifier()) {
|
|
return parse_level_id();
|
|
} else {
|
|
throw parser_error("invalid level expression", pos());
|
|
}
|
|
}
|
|
|
|
level parser::parse_level_led(level left) {
|
|
auto p = pos();
|
|
if (curr_is_token(get_cup_tk())) {
|
|
next();
|
|
level right = parse_level(g_level_cup_prec);
|
|
return mk_max(left, right);
|
|
} else if (curr_is_token(get_add_tk())) {
|
|
next();
|
|
if (curr_is_numeral()) {
|
|
unsigned k = parse_small_nat();
|
|
return lift(left, k);
|
|
} else {
|
|
throw parser_error("invalid level expression, right hand side of '+' "
|
|
"(aka universe lift operator) must be a numeral", p);
|
|
}
|
|
} else {
|
|
throw parser_error("invalid level expression", p);
|
|
}
|
|
}
|
|
|
|
level parser::parse_level(unsigned rbp) {
|
|
level left = parse_level_nud();
|
|
while (rbp < curr_level_lbp()) {
|
|
left = parse_level_led(left);
|
|
}
|
|
return left;
|
|
}
|
|
|
|
/** \brief Temporary helper class that allows us to convert local_expr_decls into local_context,
|
|
and translate expressions back and forth the two representations.
|
|
|
|
This helper class is needed because the old elaborator is based on the local_expr_decls
|
|
structure, and the new one on the more efficient local_context.
|
|
|
|
After the old elaborator is removed from the code base, we will be able to replace
|
|
local_expr_decls with local_context in the parser, and avoid this adapter. */
|
|
class local_context_adapter {
|
|
local_context m_lctx;
|
|
buffer<expr> m_locals;
|
|
buffer<expr> m_local_refs;
|
|
|
|
/* Return true iff \c e has a local_decl reference */
|
|
static bool has_local_ref(expr const & e) {
|
|
return static_cast<bool>(find(e, [](expr const & e, unsigned) { return is_local_decl_ref(e); }));
|
|
}
|
|
|
|
/* Return true iff \c e has a local constant that is not a local_decl reference */
|
|
static bool has_regular_local(expr const & e) {
|
|
return static_cast<bool>(find(e, [](expr const & e, unsigned) { return is_local(e) && !is_local_decl_ref(e); }));
|
|
}
|
|
|
|
void add_local(expr const & local) {
|
|
expr const & local_type = mlocal_type(local);
|
|
expr new_local_type = translate_to(local_type);
|
|
expr new_local_ref = m_lctx.mk_local_decl(local_pp_name(local), new_local_type, local_info(local));
|
|
m_locals.push_back(local);
|
|
m_local_refs.push_back(new_local_ref);
|
|
}
|
|
|
|
public:
|
|
void init(local_expr_decls const & ldecls) {
|
|
lean_assert(m_lctx.empty() && m_locals.empty());
|
|
buffer<pair<name, expr>> entries;
|
|
to_buffer(ldecls.get_entries(), entries);
|
|
unsigned i = entries.size();
|
|
while (i > 0) {
|
|
--i;
|
|
pair<name, expr> const & entry = entries[i];
|
|
expr const & local = entry.second;
|
|
if (!is_local(local)) continue;
|
|
add_local(local);
|
|
}
|
|
}
|
|
|
|
void init(list<expr> const & lctx) {
|
|
lean_assert(std::all_of(lctx.begin(), lctx.end(), is_local));
|
|
lean_assert(m_lctx.empty() && m_locals.empty());
|
|
buffer<expr> entries;
|
|
to_buffer(lctx, entries);
|
|
unsigned i = entries.size();
|
|
while (i > 0) {
|
|
--i;
|
|
add_local(entries[i]);
|
|
}
|
|
}
|
|
|
|
expr translate_to(expr const & e) const {
|
|
lean_assert(!has_local_ref(e));
|
|
expr r = instantiate_rev(abstract_locals(e, m_locals.size(), m_locals.data()),
|
|
m_local_refs.size(), m_local_refs.data());
|
|
lean_assert(!has_regular_local(r));
|
|
return r;
|
|
}
|
|
|
|
expr translate_from(expr const & e) const {
|
|
lean_assert(!has_regular_local(e));
|
|
expr r = instantiate_rev(abstract_locals(e, m_local_refs.size(), m_local_refs.data()),
|
|
m_locals.size(), m_locals.data());
|
|
lean_assert(!has_local_ref(r));
|
|
return r;
|
|
}
|
|
|
|
local_context const & lctx() const { return m_lctx; }
|
|
};
|
|
|
|
pair<expr, level_param_names> parser::elaborate(metavar_context & mctx, local_context_adapter const & adapter,
|
|
expr const & e, bool check_unassigned) {
|
|
expr tmp_e = adapter.translate_to(e);
|
|
pair<expr, level_param_names> r =
|
|
::lean::elaborate(m_env, get_options(), mctx, adapter.lctx(), tmp_e, check_unassigned);
|
|
expr new_e = r.first;
|
|
new_e = adapter.translate_from(new_e);
|
|
return mk_pair(new_e, r.second);
|
|
}
|
|
|
|
pair<expr, level_param_names> parser::elaborate(metavar_context & mctx, list<expr> const & lctx, expr const & e, bool check_unassigned) {
|
|
local_context_adapter adapter;
|
|
adapter.init(lctx);
|
|
return elaborate(mctx, adapter, e, check_unassigned);
|
|
}
|
|
|
|
pair<expr, level_param_names> parser::elaborate(metavar_context & mctx, expr const & e, bool check_unassigned) {
|
|
local_context_adapter adapter;
|
|
adapter.init(m_local_decls);
|
|
return elaborate(mctx, adapter, e, check_unassigned);
|
|
}
|
|
|
|
pair<expr, level_param_names> parser::elaborate(expr const & e) {
|
|
metavar_context mctx;
|
|
return elaborate(mctx, list<expr>(), e, true);
|
|
}
|
|
|
|
pair<expr, level_param_names> parser::elaborate(list<expr> const & ctx, expr const & e) {
|
|
metavar_context mctx;
|
|
return elaborate(mctx, ctx, e, true);
|
|
}
|
|
|
|
pair<expr, level_param_names> parser::elaborate_type(list<expr> const & ctx, expr const & e) {
|
|
metavar_context mctx;
|
|
expr Type = copy_tag(e, mk_sort(mk_level_placeholder()));
|
|
expr new_e = copy_tag(e, mk_typed_expr(Type, e));
|
|
return elaborate(mctx, ctx, new_e, true);
|
|
}
|
|
|
|
pair<expr, level_param_names> parser::elaborate_type(metavar_context & mctx, expr const & e) {
|
|
expr Type = copy_tag(e, mk_sort(mk_level_placeholder()));
|
|
expr new_e = copy_tag(e, mk_typed_expr(Type, e));
|
|
return elaborate(mctx, new_e, true);
|
|
}
|
|
|
|
/* =========== BEGIN OF OLD ELABORATOR LEGACY CODE =========== */
|
|
elaborator_context parser::mk_elaborator_context(bool check_unassigned) {
|
|
return elaborator_context(m_env, get_options(), m_local_level_decls, check_unassigned);
|
|
}
|
|
|
|
elaborator_context parser::mk_elaborator_context(environment const & env) {
|
|
return elaborator_context(env, get_options(), m_local_level_decls, true);
|
|
}
|
|
|
|
elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls) {
|
|
return elaborator_context(env, get_options(), lls, true);
|
|
}
|
|
|
|
std::tuple<expr, level_param_names> parser::old_elaborate_relaxed(expr const & e, list<expr> const & ctx) {
|
|
bool check_unassigned = false;
|
|
bool ensure_type = false;
|
|
bool nice_mvar_names = true;
|
|
elaborator_context env = mk_elaborator_context(check_unassigned);
|
|
auto r = ::lean::elaborate(env, ctx, e, ensure_type, nice_mvar_names);
|
|
m_pre_info_manager.clear();
|
|
return r;
|
|
}
|
|
|
|
std::tuple<expr, level_param_names> parser::old_elaborate(expr const & e, list<expr> const & ctx) {
|
|
bool check_unassigned = true;
|
|
bool ensure_type = false;
|
|
elaborator_context env = mk_elaborator_context(check_unassigned);
|
|
auto r = ::lean::elaborate(env, ctx, e, ensure_type);
|
|
m_pre_info_manager.clear();
|
|
return r;
|
|
}
|
|
|
|
std::tuple<expr, level_param_names> parser::old_elaborate_type(expr const & e, list<expr> const & ctx, bool clear_pre_info) {
|
|
bool check_unassigned = true;
|
|
bool ensure_type = true;
|
|
elaborator_context env = mk_elaborator_context(check_unassigned);
|
|
auto r = ::lean::elaborate(env, ctx, e, ensure_type);
|
|
if (clear_pre_info)
|
|
m_pre_info_manager.clear();
|
|
return r;
|
|
}
|
|
|
|
std::tuple<expr, level_param_names> parser::old_elaborate_at(environment const & env, expr const & e) {
|
|
elaborator_context eenv = mk_elaborator_context(env);
|
|
auto r = ::lean::elaborate(eenv, list<expr>(), e);
|
|
m_pre_info_manager.clear();
|
|
return r;
|
|
}
|
|
|
|
auto parser::old_elaborate_definition(name const & n, expr const & t, expr const & v)
|
|
-> std::tuple<expr, expr, level_param_names> {
|
|
elaborator_context eenv = mk_elaborator_context();
|
|
auto r = ::lean::elaborate(eenv, n, t, v);
|
|
m_pre_info_manager.clear();
|
|
return r;
|
|
}
|
|
|
|
auto parser::old_elaborate_definition_at(environment const & env, local_level_decls const & lls,
|
|
name const & n, expr const & t, expr const & v)
|
|
-> std::tuple<expr, expr, level_param_names> {
|
|
elaborator_context eenv = mk_elaborator_context(env, lls);
|
|
auto r = ::lean::elaborate(eenv, n, t, v);
|
|
m_pre_info_manager.clear();
|
|
return r;
|
|
}
|
|
/* =========== END OF OLD ELABORATOR LEGACY CODE =========== */
|
|
|
|
[[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {
|
|
throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos);
|
|
}
|
|
|
|
/**
|
|
\brief Return an optional binder_info object based on the current token
|
|
- '(' : default
|
|
- '{' : implicit
|
|
- '{{' or '⦃' : strict implicit
|
|
- '[' : inst_implicit (i.e., implicit argument that should be
|
|
synthesized using type class resolution)
|
|
|
|
If simple_only, then only `(` is considered
|
|
*/
|
|
optional<binder_info> parser::parse_optional_binder_info(bool simple_only) {
|
|
if (curr_is_token(get_lparen_tk())) {
|
|
next();
|
|
return some(binder_info());
|
|
} else if (simple_only) {
|
|
return optional<binder_info>();
|
|
} else if (curr_is_token(get_lcurly_tk())) {
|
|
next();
|
|
if (curr_is_token(get_lcurly_tk())) {
|
|
next();
|
|
return some(mk_strict_implicit_binder_info());
|
|
} else {
|
|
return some(mk_implicit_binder_info());
|
|
}
|
|
} else if (curr_is_token(get_lbracket_tk())) {
|
|
next();
|
|
return some(mk_inst_implicit_binder_info());
|
|
} else if (curr_is_token(get_ldcurly_tk())) {
|
|
next();
|
|
return some(mk_strict_implicit_binder_info());
|
|
} else {
|
|
return optional<binder_info>();
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Return binder_info object based on the current token, it fails if the current token
|
|
is not '(', '{', '{{', '⦃', or '['
|
|
|
|
\see parse_optional_binder_info
|
|
*/
|
|
binder_info parser::parse_binder_info(bool simple_only) {
|
|
auto p = pos();
|
|
if (auto bi = parse_optional_binder_info(simple_only)) {
|
|
return *bi;
|
|
} else {
|
|
throw_invalid_open_binder(p);
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Consume the next token based on the value of \c bi
|
|
- none : do not consume anything
|
|
- default : consume ')'
|
|
- implicit : consume '}'
|
|
- strict implicit : consume '}}' or '⦄'
|
|
- inst implicit : consume ']'
|
|
*/
|
|
void parser::parse_close_binder_info(optional<binder_info> const & bi) {
|
|
if (!bi) {
|
|
return;
|
|
} else if (bi->is_implicit()) {
|
|
check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected");
|
|
} else if (bi->is_inst_implicit()) {
|
|
check_token_next(get_rbracket_tk(), "invalid declaration, ']' expected");
|
|
} else if (bi->is_strict_implicit()) {
|
|
if (curr_is_token(get_rcurly_tk())) {
|
|
next();
|
|
check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected");
|
|
} else {
|
|
check_token_next(get_rdcurly_tk(), "invalid declaration, '⦄' expected");
|
|
}
|
|
} else {
|
|
check_token_next(get_rparen_tk(), "invalid declaration, ')' expected");
|
|
}
|
|
}
|
|
|
|
/** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
|
|
expr parser::parse_binder_core(binder_info const & bi, unsigned rbp) {
|
|
auto p = pos();
|
|
name id = check_atomic_id_next("invalid binder, atomic identifier expected");
|
|
expr type;
|
|
if (curr_is_token(get_colon_tk())) {
|
|
next();
|
|
type = parse_expr(rbp);
|
|
} else {
|
|
type = save_pos(mk_expr_placeholder(), p);
|
|
}
|
|
save_identifier_info(p, id);
|
|
return save_pos(mk_local(id, type, bi), p);
|
|
}
|
|
|
|
expr parser::parse_binder(unsigned rbp) {
|
|
if (curr_is_identifier()) {
|
|
return parse_binder_core(binder_info(), rbp);
|
|
} else {
|
|
bool simple_only = false;
|
|
binder_info bi = parse_binder_info(simple_only);
|
|
rbp = 0;
|
|
auto r = parse_binder_core(bi, rbp);
|
|
parse_close_binder_info(bi);
|
|
return r;
|
|
}
|
|
}
|
|
|
|
/* Lean allow binders of the form <tt>ID_1 ... ID_n 'op' S</tt>
|
|
Where 'op' is an infix operator, and s an expression (i.e., "collection").
|
|
This notation expands to:
|
|
(ID_1 ... ID_n : _) (H_1 : ID_1 'op' S) ... (H_n : ID_n 'op' S)
|
|
|
|
This method return true if the next token is an infix operator,
|
|
and populates r with the locals above.
|
|
*/
|
|
bool parser::parse_binder_collection(buffer<pair<pos_info, name>> const & names, binder_info const & bi, buffer<expr> & r) {
|
|
if (!curr_is_keyword())
|
|
return false;
|
|
name tk = get_token_info().value();
|
|
list<pair<notation::transition, parse_table>> trans_list = led().find(tk);
|
|
if (length(trans_list) != 1)
|
|
return false;
|
|
pair<notation::transition, parse_table> const & p = head(trans_list);
|
|
list<notation::accepting> const & acc_lst = p.second.is_accepting();
|
|
if (length(acc_lst) != 1)
|
|
return false; // no overloading
|
|
notation::accepting const & acc = head(acc_lst);
|
|
lean_assert(!acc.get_postponed());
|
|
expr pred = acc.get_expr();
|
|
unsigned rbp = p.first.get_action().rbp();
|
|
next(); // consume tk
|
|
expr S = parse_expr(rbp);
|
|
unsigned old_sz = r.size();
|
|
/* Add (ID_1 ... ID_n : _) to r */
|
|
for (auto p : names) {
|
|
expr arg_type = save_pos(mk_expr_placeholder(), p.first);
|
|
save_identifier_info(p.first, p.second);
|
|
expr local = save_pos(mk_local(p.second, arg_type, bi), p.first);
|
|
add_local(local);
|
|
r.push_back(local);
|
|
}
|
|
/* Add (H_1 : ID_1 'op' S) ... (H_n : ID_n 'op' S) */
|
|
unsigned i = old_sz;
|
|
for (auto p : names) {
|
|
expr ID = r[i];
|
|
expr args[2] = {ID, S};
|
|
expr ID_op_S = instantiate_rev(pred, 2, args);
|
|
expr local = save_pos(mk_local("H", ID_op_S, bi), p.first);
|
|
add_local(local);
|
|
r.push_back(local);
|
|
i++;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
/**
|
|
\brief Parse <tt>ID ... ID ':' expr</tt>, where the expression
|
|
represents the type of the identifiers.
|
|
*/
|
|
void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp) {
|
|
buffer<pair<pos_info, name>> names;
|
|
while (curr_is_identifier()) {
|
|
auto p = pos();
|
|
names.emplace_back(p, check_atomic_id_next("invalid binder, atomic identifier expected"));
|
|
}
|
|
if (names.empty())
|
|
throw parser_error("invalid binder, identifier expected", pos());
|
|
optional<expr> type;
|
|
if (curr_is_token(get_colon_tk())) {
|
|
next();
|
|
type = parse_expr(rbp);
|
|
} else if (parse_binder_collection(names, bi, r)) {
|
|
return;
|
|
}
|
|
for (auto p : names) {
|
|
expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);
|
|
save_identifier_info(p.first, p.second);
|
|
expr local = save_pos(mk_local(p.second, arg_type, bi), p.first);
|
|
add_local(local);
|
|
r.push_back(local);
|
|
}
|
|
}
|
|
|
|
expr parser::parse_inst_implicit_decl() {
|
|
binder_info bi = mk_inst_implicit_binder_info();
|
|
auto id_pos = pos();
|
|
name id;
|
|
expr type;
|
|
if (curr_is_identifier()) {
|
|
id = get_name_val();
|
|
next();
|
|
if (curr_is_token(get_colon_tk())) {
|
|
next();
|
|
type = parse_expr();
|
|
} else {
|
|
expr left = id_to_expr(id, id_pos);
|
|
id = mk_anonymous_inst_name();
|
|
unsigned rbp = 0;
|
|
while (rbp < curr_lbp()) {
|
|
left = parse_led(left);
|
|
}
|
|
type = left;
|
|
}
|
|
} else {
|
|
id = mk_anonymous_inst_name();
|
|
type = parse_expr();
|
|
}
|
|
save_identifier_info(id_pos, id);
|
|
expr local = save_pos(mk_local(id, type, bi), id_pos);
|
|
add_local(local);
|
|
return local;
|
|
}
|
|
|
|
|
|
void parser::parse_inst_implicit_decl(buffer<expr> & r) {
|
|
expr local = parse_inst_implicit_decl();
|
|
r.push_back(local);
|
|
}
|
|
|
|
void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries,
|
|
bool & last_block_delimited, unsigned rbp, bool simple_only) {
|
|
while (true) {
|
|
if (curr_is_identifier()) {
|
|
parse_binder_block(r, binder_info(), rbp);
|
|
last_block_delimited = false;
|
|
} else {
|
|
optional<binder_info> bi = parse_optional_binder_info(simple_only);
|
|
if (bi) {
|
|
rbp = 0;
|
|
last_block_delimited = true;
|
|
if (bi->is_inst_implicit()) {
|
|
parse_inst_implicit_decl(r);
|
|
} else {
|
|
if (simple_only || !parse_local_notation_decl(nentries))
|
|
parse_binder_block(r, *bi, rbp);
|
|
}
|
|
parse_close_binder_info(bi);
|
|
} else {
|
|
return;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries,
|
|
bool & last_block_delimited, bool allow_empty, unsigned rbp,
|
|
bool simple_only) {
|
|
flet<environment> save1(m_env, m_env); // save environment
|
|
flet<local_expr_decls> save2(m_local_decls, m_local_decls);
|
|
unsigned old_sz = r.size();
|
|
parse_binders_core(r, nentries, last_block_delimited, rbp, simple_only);
|
|
if (!allow_empty && old_sz == r.size())
|
|
throw_invalid_open_binder(pos());
|
|
return local_environment(m_env);
|
|
}
|
|
|
|
bool parser::parse_local_notation_decl(buffer<notation_entry> * nentries) {
|
|
if (curr_is_notation_decl(*this)) {
|
|
parser::in_notation_ctx ctx(*this);
|
|
buffer<token_entry> new_tokens;
|
|
bool overload = false;
|
|
bool allow_local = true;
|
|
auto ne = ::lean::parse_notation(*this, overload, new_tokens, allow_local);
|
|
for (auto const & te : new_tokens)
|
|
m_env = add_token(m_env, te);
|
|
if (nentries) nentries->push_back(ne);
|
|
m_env = add_notation(m_env, ne);
|
|
return true;
|
|
} else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
void parser::process_postponed(buffer<expr> const & args, bool is_left,
|
|
buffer<notation::action_kind> const & kinds,
|
|
buffer<list<expr>> const & nargs,
|
|
buffer<expr> const & ps,
|
|
buffer<pair<unsigned, pos_info>> const & scoped_info,
|
|
list<notation::action> const & postponed,
|
|
pos_info const & p,
|
|
buffer<expr> & new_args) {
|
|
unsigned args_idx = 0;
|
|
if (is_left) {
|
|
new_args.push_back(args[0]);
|
|
args_idx = 1;
|
|
}
|
|
unsigned kinds_idx = 0;
|
|
unsigned nargs_idx = 0;
|
|
unsigned scoped_idx = 0;
|
|
list<notation::action> it = postponed;
|
|
for (; kinds_idx < kinds.size(); kinds_idx++, args_idx++) {
|
|
auto k = kinds[kinds_idx];
|
|
switch (k) {
|
|
case notation::action_kind::Exprs: {
|
|
if (!it || head(it).kind() != k || nargs_idx >= nargs.size())
|
|
throw exception("ill-formed parsing tables");
|
|
notation::action const & a = head(it);
|
|
buffer<expr> r_args;
|
|
to_buffer(nargs[nargs_idx], r_args);
|
|
nargs_idx++;
|
|
expr rec = copy_with_new_pos(a.get_rec(), p);
|
|
expr r;
|
|
if (a.is_fold_right()) {
|
|
if (a.get_initial()) {
|
|
r = instantiate_rev(copy_with_new_pos(*a.get_initial(), p), new_args.size(), new_args.data());
|
|
} else {
|
|
r = r_args.back();
|
|
r_args.pop_back();
|
|
}
|
|
unsigned i = r_args.size();
|
|
while (i > 0) {
|
|
--i;
|
|
new_args.push_back(r_args[i]);
|
|
new_args.push_back(r);
|
|
r = instantiate_rev(rec, new_args.size(), new_args.data());
|
|
new_args.pop_back(); new_args.pop_back();
|
|
}
|
|
} else {
|
|
unsigned fidx = 0;
|
|
if (a.get_initial()) {
|
|
r = instantiate_rev(copy_with_new_pos(*a.get_initial(), p), new_args.size(), new_args.data());
|
|
} else {
|
|
r = r_args[0];
|
|
fidx++;
|
|
}
|
|
for (unsigned i = fidx; i < r_args.size(); i++) {
|
|
new_args.push_back(r_args[i]);
|
|
new_args.push_back(r);
|
|
r = instantiate_rev(rec, new_args.size(), new_args.data());
|
|
new_args.pop_back(); new_args.pop_back();
|
|
}
|
|
}
|
|
new_args.push_back(r);
|
|
it = tail(it);
|
|
break;
|
|
}
|
|
case notation::action_kind::ScopedExpr: {
|
|
if (!it || head(it).kind() != k || scoped_idx >= scoped_info.size())
|
|
throw exception("ill-formed parsing tables");
|
|
expr r = args[args_idx];
|
|
notation::action const & a = head(it);
|
|
bool no_cache = false;
|
|
unsigned ps_sz = scoped_info[scoped_idx].first;
|
|
pos_info binder_pos = scoped_info[scoped_idx].second;
|
|
scoped_idx++;
|
|
if (is_var(a.get_rec(), 0)) {
|
|
if (a.use_lambda_abstraction())
|
|
r = Fun(ps_sz, ps.data(), r, no_cache);
|
|
else
|
|
r = Pi(ps_sz, ps.data(), r, no_cache);
|
|
r = rec_save_pos(r, binder_pos);
|
|
} else {
|
|
expr rec = copy_with_new_pos(a.get_rec(), p);
|
|
unsigned i = ps_sz;
|
|
while (i > 0) {
|
|
--i;
|
|
expr const & l = ps[i];
|
|
if (a.use_lambda_abstraction())
|
|
r = Fun(l, r, no_cache);
|
|
else
|
|
r = Pi(l, r, no_cache);
|
|
r = save_pos(r, binder_pos);
|
|
new_args.push_back(r);
|
|
r = instantiate_rev(rec, new_args.size(), new_args.data());
|
|
new_args.pop_back();
|
|
}
|
|
}
|
|
new_args.push_back(r);
|
|
it = tail(it);
|
|
break;
|
|
}
|
|
default:
|
|
new_args.push_back(args[args_idx]);
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
|
|
// Return true iff the current token is the terminator of some Exprs action, and store the matching pair in r
|
|
static bool curr_is_terminator_of_exprs_action(parser const & p, list<pair<notation::transition, parse_table>> const & lst, pair<notation::transition, parse_table> const * & r) {
|
|
for (auto const & pr : lst) {
|
|
notation::action const & a = pr.first.get_action();
|
|
if (a.kind() == notation::action_kind::Exprs &&
|
|
a.get_terminator() &&
|
|
p.curr_is_token(name(utf8_trim(a.get_terminator()->to_string())))) {
|
|
r = ≺
|
|
return true;
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
// Return true iff \c lst contains a Skip action, and store the matching pair in r.
|
|
static bool has_skip(list<pair<notation::transition, parse_table>> const & lst, pair<notation::transition, parse_table> const * & r) {
|
|
for (auto const & p : lst) {
|
|
notation::action const & a = p.first.get_action();
|
|
if (a.kind() == notation::action_kind::Skip) {
|
|
r = &p;
|
|
return true;
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
static pair<notation::transition, parse_table> const * get_non_skip(list<pair<notation::transition, parse_table>> const & lst) {
|
|
for (auto const & p : lst) {
|
|
notation::action const & a = p.first.get_action();
|
|
if (a.kind() != notation::action_kind::Skip)
|
|
return &p;
|
|
}
|
|
return nullptr;
|
|
}
|
|
|
|
expr parser::parse_notation(parse_table t, expr * left) {
|
|
lean_assert(curr() == scanner::token_kind::Keyword);
|
|
auto p = pos();
|
|
if (m_info_manager)
|
|
m_info_manager->add_symbol_info(p.first, p.second, get_token_info().token());
|
|
buffer<expr> args;
|
|
buffer<notation::action_kind> kinds;
|
|
buffer<list<expr>> nargs; // nary args
|
|
buffer<expr> ps;
|
|
buffer<pair<unsigned, pos_info>> scoped_info; // size of ps and binder_pos for scoped_exprs
|
|
// Invariants:
|
|
// args.size() == kinds.size() if not left
|
|
// args.size() == kinds.size()+1 if left
|
|
// nargs.size() == number of Exprs in kinds
|
|
// scoped_info.size() == number of Scoped_Exprs in kinds
|
|
bool has_Exprs = false;
|
|
local_environment lenv(m_env);
|
|
pos_info binder_pos;
|
|
if (left)
|
|
args.push_back(*left);
|
|
while (true) {
|
|
if (curr() != scanner::token_kind::Keyword)
|
|
break;
|
|
auto r = t.find(get_token_info().value());
|
|
if (!r)
|
|
break;
|
|
pair<notation::transition, parse_table> const * curr_pair = nullptr;
|
|
if (tail(r)) {
|
|
// There is more than one possible actions.
|
|
// In the current implementation, we support the following possible cases (Skip, Expr), (Skip, Exprs) amd (Skip, ScopedExpr)
|
|
next();
|
|
if (curr_is_terminator_of_exprs_action(*this, r, curr_pair)) {
|
|
lean_assert(curr_pair->first.get_action().kind() == notation::action_kind::Exprs);
|
|
} else if (has_skip(r, curr_pair) && !curr_starts_expr()) {
|
|
lean_assert(curr_pair->first.get_action().kind() == notation::action_kind::Skip);
|
|
} else {
|
|
curr_pair = get_non_skip(r);
|
|
}
|
|
} else {
|
|
// there is only one possible action
|
|
curr_pair = &head(r);
|
|
if (curr_pair->first.get_action().kind() != notation::action_kind::Ext)
|
|
next();
|
|
}
|
|
lean_assert(curr_pair);
|
|
notation::action const & a = curr_pair->first.get_action();
|
|
switch (a.kind()) {
|
|
case notation::action_kind::Skip:
|
|
break;
|
|
case notation::action_kind::Expr:
|
|
args.push_back(parse_expr(a.rbp()));
|
|
kinds.push_back(a.kind());
|
|
break;
|
|
case notation::action_kind::Exprs: {
|
|
buffer<expr> r_args;
|
|
auto terminator = a.get_terminator();
|
|
if (terminator)
|
|
terminator = some(name(utf8_trim(terminator->to_string()))); // remove padding
|
|
if (!terminator || !curr_is_token(*terminator)) {
|
|
r_args.push_back(parse_expr(a.rbp()));
|
|
name sep = utf8_trim(a.get_sep().to_string()); // remove padding
|
|
while (curr_is_token(sep)) {
|
|
next();
|
|
r_args.push_back(parse_expr(a.rbp()));
|
|
}
|
|
}
|
|
if (terminator) {
|
|
if (curr_is_token(*terminator)) {
|
|
next();
|
|
} else {
|
|
throw parser_error(sstream() << "invalid composite expression, '" << *terminator << "' expected", pos());
|
|
}
|
|
}
|
|
has_Exprs = true;
|
|
args.push_back(expr()); // placeholder
|
|
kinds.push_back(a.kind());
|
|
nargs.push_back(to_list(r_args));
|
|
break;
|
|
}
|
|
case notation::action_kind::Binder:
|
|
binder_pos = pos();
|
|
ps.push_back(parse_binder(a.rbp()));
|
|
break;
|
|
case notation::action_kind::Binders:
|
|
binder_pos = pos();
|
|
lenv = parse_binders(ps, a.rbp());
|
|
break;
|
|
case notation::action_kind::ScopedExpr: {
|
|
expr r = parse_scoped_expr(ps, lenv, a.rbp());
|
|
args.push_back(r);
|
|
kinds.push_back(a.kind());
|
|
scoped_info.push_back(mk_pair(ps.size(), binder_pos));
|
|
break;
|
|
}
|
|
case notation::action_kind::Ext:
|
|
args.push_back(a.get_parse_fn()(*this, args.size(), args.data(), p));
|
|
kinds.push_back(a.kind());
|
|
break;
|
|
}
|
|
t = curr_pair->second;
|
|
}
|
|
list<notation::accepting> const & as = t.is_accepting();
|
|
save_overload_notation(as, p);
|
|
if (is_nil(as)) {
|
|
if (p == pos())
|
|
throw parser_error(sstream() << "invalid expression", pos());
|
|
else
|
|
throw parser_error(sstream() << "invalid expression starting at " << p.first << ":" << p.second, pos());
|
|
}
|
|
lean_assert(left || args.size() == kinds.size());
|
|
lean_assert(!left || args.size() == kinds.size() + 1);
|
|
/*
|
|
IF there are multiple choices and Exprs was not used, we create a lambda for each choice.
|
|
In this case, we copy args to actual_args and store local constants in args. */
|
|
buffer<expr> actual_args;
|
|
buffer<expr> cs;
|
|
bool create_lambdas = length(as) > 1 && !has_Exprs;
|
|
if (create_lambdas) {
|
|
name x("x");
|
|
unsigned idx = 1;
|
|
for (expr & arg : args) {
|
|
actual_args.push_back(arg);
|
|
arg = mk_local(mk_fresh_name(), x.append_after(idx), mk_expr_placeholder(), binder_info());
|
|
idx++;
|
|
}
|
|
}
|
|
for (notation::accepting const & a : as) {
|
|
expr r = copy_with_new_pos(a.get_expr(), p);
|
|
list<notation::action> const & postponed = a.get_postponed();
|
|
if (postponed) {
|
|
buffer<expr> new_args;
|
|
process_postponed(args, left, kinds, nargs, ps, scoped_info, postponed, p, new_args);
|
|
lean_assert(!args.empty());
|
|
r = instantiate_rev(r, new_args.size(), new_args.data());
|
|
} else {
|
|
lean_assert(nargs.empty() && scoped_info.empty());
|
|
if (args.empty()) {
|
|
// Notation does not have arguments. Thus, the info-manager should treat is as a single thing.
|
|
r = mk_notation_info(r, r.get_tag());
|
|
} else {
|
|
r = instantiate_rev(r, args.size(), args.data());
|
|
}
|
|
}
|
|
if (create_lambdas) {
|
|
bool no_cache = false;
|
|
r = rec_save_pos(eta_reduce(Fun(args, r, no_cache)), p);
|
|
}
|
|
cs.push_back(r);
|
|
}
|
|
expr r = save_pos(mk_choice(cs.size(), cs.data()), p);
|
|
if (create_lambdas) {
|
|
r = rec_save_pos(::lean::mk_app(r, actual_args), p);
|
|
}
|
|
save_type_info(r);
|
|
return r;
|
|
}
|
|
|
|
expr parser::parse_nud_notation() {
|
|
return parse_notation(nud(), nullptr);
|
|
}
|
|
|
|
expr parser::parse_led_notation(expr left) {
|
|
if (led().find(get_token_info().value())) {
|
|
return parse_notation(led(), &left);
|
|
} else {
|
|
return mk_app(left, parse_expr(get_max_prec()), pos_of(left));
|
|
}
|
|
}
|
|
|
|
struct to_pattern_fn {
|
|
parser & m_parser;
|
|
buffer<expr> & m_new_locals;
|
|
name_map<expr> m_vars;
|
|
|
|
environment const & env() { return m_parser.env(); }
|
|
|
|
to_pattern_fn(parser & p, buffer<expr> & new_locals):
|
|
m_parser(p), m_new_locals(new_locals) {}
|
|
|
|
/* Return true iff the constant n may occur in a pattern */
|
|
bool is_pattern_constant(name const & n) {
|
|
if (inductive::is_intro_rule(env(), n))
|
|
return true;
|
|
if (has_pattern_attribute(env(), n))
|
|
return true;
|
|
return false;
|
|
}
|
|
|
|
expr visit_local(expr const & e) {
|
|
if (auto r = m_vars.find(local_pp_name(e)))
|
|
return *r;
|
|
bool resolve_only = true;
|
|
expr new_e = m_parser.id_to_expr(local_pp_name(e), m_parser.pos_of(e), resolve_only);
|
|
if (is_constant(new_e) && is_pattern_constant(const_name(new_e))) {
|
|
return new_e;
|
|
} else if (is_choice(new_e)) {
|
|
bool all_pattern_constant = true;
|
|
bool has_pattern_constant = false;
|
|
for (unsigned i = 0; i < get_num_choices(new_e); i++) {
|
|
expr const & c = get_choice(new_e, i);
|
|
if (is_constant(c) && is_pattern_constant(const_name(c)))
|
|
has_pattern_constant = true;
|
|
else
|
|
all_pattern_constant = false;
|
|
}
|
|
if (all_pattern_constant) {
|
|
return new_e;
|
|
} else if (has_pattern_constant) {
|
|
throw parser_error(sstream() << "invalid pattern, '" << e << "' is overloaded, "
|
|
<< "and some interpretations may occur in patterns and others not "
|
|
<< "(solution: use fully qualified names)",
|
|
m_parser.pos_of(e));
|
|
} else {
|
|
// assume e is a variable shadowing overloaded constants
|
|
}
|
|
}
|
|
if (!local_pp_name(e).is_atomic()) {
|
|
throw parser_error("invalid pattern, variable, constructor or constant tagged as pattern expected",
|
|
m_parser.pos_of(e));
|
|
}
|
|
m_vars.insert(local_pp_name(e), e);
|
|
m_new_locals.push_back(e);
|
|
return e;
|
|
}
|
|
|
|
expr to_expr(expr const & e) {
|
|
return replace(e, [&](expr const & e, unsigned) {
|
|
if (is_local(e)) {
|
|
if (auto r = m_vars.find(local_pp_name(e)))
|
|
return some_expr(*r);
|
|
else
|
|
return some_expr(m_parser.patexpr_to_expr(e));
|
|
}
|
|
return none_expr();
|
|
});
|
|
}
|
|
|
|
expr visit(expr const & e, bool skip_main_fn) {
|
|
if (is_typed_expr(e)) {
|
|
expr new_v = visit(get_typed_expr_expr(e), false);
|
|
expr new_t = to_expr(get_typed_expr_type(e));
|
|
return copy_tag(e, mk_typed_expr(new_t, new_v));
|
|
} else if (is_prenum(e)) {
|
|
return e;
|
|
} else if (is_inaccessible(e)) {
|
|
return to_expr(e);
|
|
} else if (is_placeholder(e)) {
|
|
return e;
|
|
} else if (is_app(e)) {
|
|
expr new_f = visit(app_fn(e), skip_main_fn);
|
|
expr new_a = visit(app_arg(e), false);
|
|
return update_app(e, new_f, new_a);
|
|
} else if (is_local(e)) {
|
|
if (skip_main_fn)
|
|
return e;
|
|
else
|
|
return visit_local(e);
|
|
} else if (is_annotation(e)) {
|
|
return copy_tag(e, mk_annotation(get_annotation_kind(e), visit(get_annotation_arg(e), skip_main_fn)));
|
|
} else if (is_constant(e) && is_pattern_constant(const_name(e))) {
|
|
return e;
|
|
} else {
|
|
throw parser_error("invalid pattern, must be an application, "
|
|
"constant, variable, type ascription or inaccessible term",
|
|
m_parser.pos_of(e));
|
|
}
|
|
}
|
|
|
|
expr operator()(expr const & e, bool skip_main_fn) {
|
|
return visit(e, skip_main_fn);
|
|
}
|
|
};
|
|
|
|
expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buffer<expr> & new_locals) {
|
|
undef_id_to_local_scope scope(*this);
|
|
return to_pattern_fn(*this, new_locals)(pat_or_expr, skip_main_fn);
|
|
}
|
|
|
|
expr parser::parse_pattern_or_expr(unsigned rbp) {
|
|
if (m_in_quote) {
|
|
throw parser_error("patterns cannot occur inside of quoted terms", pos());
|
|
}
|
|
all_id_local_scope scope(*this);
|
|
return parse_expr(rbp);
|
|
}
|
|
|
|
expr parser::patexpr_to_expr(expr const & pat_or_expr) {
|
|
error_if_undef_scope scope(*this);
|
|
return replace(pat_or_expr, [&](expr const & e, unsigned) {
|
|
if (is_local(e)) {
|
|
return some_expr(id_to_expr(local_pp_name(e), pos_of(e), true));
|
|
}
|
|
return none_expr();
|
|
});
|
|
}
|
|
|
|
expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only) {
|
|
buffer<level> lvl_buffer;
|
|
levels ls;
|
|
bool explicit_levels = false;
|
|
if (!resolve_only && curr_is_token(get_llevel_curly_tk())) {
|
|
next();
|
|
explicit_levels = true;
|
|
while (!curr_is_token(get_rcurly_tk())) {
|
|
lvl_buffer.push_back(parse_level());
|
|
}
|
|
next();
|
|
ls = to_list(lvl_buffer.begin(), lvl_buffer.end());
|
|
}
|
|
|
|
if (!explicit_levels && m_id_behavior == id_behavior::AllLocal) {
|
|
return save_pos(mk_local(id, mk_expr_placeholder()), p);
|
|
}
|
|
|
|
// locals
|
|
if (auto it1 = m_local_decls.find(id)) {
|
|
if (ls && m_id_behavior != id_behavior::AssumeConstantIfUndef)
|
|
throw parser_error("invalid use of explicit universe parameter, identifier is a variable, "
|
|
"parameter or a constant bound to parameters in a section", p);
|
|
auto r = copy_with_new_pos(*it1, p);
|
|
if (!resolve_only) {
|
|
save_type_info(r);
|
|
save_identifier_info(p, id);
|
|
}
|
|
return r;
|
|
}
|
|
|
|
for (name const & ns : get_namespaces(m_env)) {
|
|
auto new_id = ns + id;
|
|
if (!ns.is_anonymous() && m_env.find(new_id) &&
|
|
(!id.is_atomic() || !is_protected(m_env, new_id))) {
|
|
auto r = save_pos(mk_constant(new_id, ls), p);
|
|
if (!resolve_only) {
|
|
save_type_info(r);
|
|
add_ref_index(new_id, p);
|
|
save_identifier_info(p, new_id);
|
|
}
|
|
return r;
|
|
}
|
|
}
|
|
|
|
if (!id.is_atomic()) {
|
|
name new_id = id;
|
|
new_id = remove_root_prefix(new_id);
|
|
if (m_env.find(new_id)) {
|
|
auto r = save_pos(mk_constant(new_id, ls), p);
|
|
if (!resolve_only) {
|
|
save_type_info(r);
|
|
add_ref_index(new_id, p);
|
|
save_identifier_info(p, new_id);
|
|
}
|
|
return r;
|
|
}
|
|
}
|
|
|
|
optional<expr> r;
|
|
// globals
|
|
if (m_env.find(id))
|
|
r = save_pos(mk_constant(id, ls), p);
|
|
// aliases
|
|
auto as = get_expr_aliases(m_env, id);
|
|
if (!is_nil(as)) {
|
|
buffer<expr> new_as;
|
|
if (r)
|
|
new_as.push_back(*r);
|
|
for (auto const & e : as) {
|
|
new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p));
|
|
}
|
|
r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
|
|
if (!resolve_only)
|
|
save_overload(*r);
|
|
}
|
|
if (!r) {
|
|
if (m_id_behavior == id_behavior::AssumeConstantIfUndef) {
|
|
r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
|
|
} else if (m_id_behavior == id_behavior::AssumeLocalIfUndef) {
|
|
expr local = mk_local(id, mk_expr_placeholder());
|
|
if (!resolve_only)
|
|
m_undef_ids.push_back(local);
|
|
r = save_pos(local, p);
|
|
}
|
|
}
|
|
if (!r)
|
|
throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
|
|
if (!resolve_only) {
|
|
save_type_info(*r);
|
|
if (is_constant(*r)) {
|
|
add_ref_index(const_name(*r), p);
|
|
save_identifier_info(p, const_name(*r));
|
|
} else if (is_local(*r)) {
|
|
save_identifier_info(p, local_pp_name(*r));
|
|
}
|
|
}
|
|
return *r;
|
|
}
|
|
|
|
list<name> parser::to_constants(name const & id, char const * msg, pos_info const & p) const {
|
|
buffer<name> rs;
|
|
|
|
std::function<void(expr const & e)> extract_names = [&](expr const & e) {
|
|
if (in_section(m_env) && is_as_atomic(e)) {
|
|
extract_names(get_app_fn(get_as_atomic_arg(e)));
|
|
} else if (is_explicit(e)) {
|
|
extract_names(get_explicit_arg(e));
|
|
} else if (is_choice(e)) {
|
|
for (unsigned i = 0; i < get_num_choices(e); i++)
|
|
extract_names(get_choice(e, i));
|
|
} else if (is_constant(e)) {
|
|
rs.push_back(const_name(e));
|
|
} else {
|
|
throw parser_error(msg, p);
|
|
}
|
|
};
|
|
|
|
// locals
|
|
if (auto it1 = m_local_decls.find(id)) {
|
|
extract_names(*it1);
|
|
return to_list(rs);
|
|
}
|
|
|
|
for (name const & ns : get_namespaces(m_env)) {
|
|
auto new_id = ns + id;
|
|
if (!ns.is_anonymous() && m_env.find(new_id) &&
|
|
(!id.is_atomic() || !is_protected(m_env, new_id))) {
|
|
return to_list(new_id);
|
|
}
|
|
}
|
|
|
|
if (!id.is_atomic()) {
|
|
name new_id = id;
|
|
new_id = remove_root_prefix(new_id);
|
|
if (m_env.find(new_id))
|
|
return to_list(new_id);
|
|
}
|
|
|
|
buffer<expr> alts;
|
|
// globals
|
|
if (m_env.find(id))
|
|
rs.push_back(id);
|
|
// aliases
|
|
auto as = get_expr_aliases(m_env, id);
|
|
for (name const & n : as) {
|
|
rs.push_back(n);
|
|
}
|
|
|
|
if (rs.empty()) {
|
|
throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
|
|
}
|
|
|
|
return to_list(rs);
|
|
}
|
|
|
|
name parser::to_constant(name const & id, char const * msg, pos_info const & p) {
|
|
return head(to_constants(id, msg, p));
|
|
}
|
|
|
|
name parser::check_constant_next(char const * msg) {
|
|
auto p = pos();
|
|
name id = check_id_next(msg);
|
|
return to_constant(id, msg, p);
|
|
}
|
|
|
|
expr parser::parse_id() {
|
|
auto p = pos();
|
|
name id = get_name_val();
|
|
next();
|
|
return id_to_expr(id, p);
|
|
}
|
|
|
|
expr parser::parse_numeral_expr(bool user_notation) {
|
|
auto p = pos();
|
|
mpz n = get_num_val().get_numerator();
|
|
next();
|
|
list<expr> vals;
|
|
if (user_notation)
|
|
vals = get_mpz_notation(m_env, n);
|
|
if (!vals) {
|
|
return save_pos(mk_prenum(n), p);
|
|
} else {
|
|
buffer<expr> cs;
|
|
cs.push_back(save_pos(mk_prenum(n), p));
|
|
for (expr const & c : vals)
|
|
cs.push_back(copy_with_new_pos(c, p));
|
|
if (cs.size() == 1)
|
|
return cs[0];
|
|
else
|
|
return save_pos(mk_choice(cs.size(), cs.data()), p);
|
|
}
|
|
}
|
|
|
|
expr parser::parse_decimal_expr() {
|
|
auto p = pos();
|
|
mpq val = get_num_val();
|
|
next();
|
|
expr num = save_pos(mk_prenum(val.get_numerator()), p);
|
|
if (val.get_denominator() == 1) {
|
|
return num;
|
|
} else {
|
|
expr den = save_pos(mk_prenum(val.get_denominator()), p);
|
|
expr div = save_pos(mk_constant(get_div_name()), p);
|
|
return save_pos(lean::mk_app(div, num, den), p);
|
|
}
|
|
}
|
|
|
|
expr parser::parse_string_expr() {
|
|
std::string v = get_str_val();
|
|
next();
|
|
return from_string(v);
|
|
}
|
|
|
|
expr parser::parse_char_expr() {
|
|
auto p = pos();
|
|
std::string v = get_str_val();
|
|
lean_assert(v.size() == 1);
|
|
next();
|
|
return mk_app(save_pos(mk_constant(get_char_of_nat_name()), p),
|
|
save_pos(mk_prenum(mpz(static_cast<unsigned>(v[0]))), p),
|
|
p);
|
|
}
|
|
|
|
expr parser::parse_nud() {
|
|
switch (curr()) {
|
|
case scanner::token_kind::Keyword: return parse_nud_notation();
|
|
case scanner::token_kind::Identifier: return parse_id();
|
|
case scanner::token_kind::Numeral: return parse_numeral_expr();
|
|
case scanner::token_kind::Decimal: return parse_decimal_expr();
|
|
case scanner::token_kind::String: return parse_string_expr();
|
|
case scanner::token_kind::Char: return parse_char_expr();
|
|
default: throw parser_error("invalid expression, unexpected token", pos());
|
|
}
|
|
}
|
|
|
|
// Return true if the current token can be the beginning of an expression
|
|
bool parser::curr_starts_expr() {
|
|
switch (curr()) {
|
|
case scanner::token_kind::Keyword:
|
|
return !is_nil(nud().find(get_token_info().value()));
|
|
case scanner::token_kind::Identifier:
|
|
case scanner::token_kind::Numeral:
|
|
case scanner::token_kind::Decimal:
|
|
case scanner::token_kind::String:
|
|
default:
|
|
return false;
|
|
}
|
|
}
|
|
|
|
expr parser::parse_led(expr left) {
|
|
switch (curr()) {
|
|
case scanner::token_kind::Keyword: return parse_led_notation(left);
|
|
default: return mk_app(left, parse_expr(get_max_prec()), pos_of(left));
|
|
}
|
|
}
|
|
|
|
unsigned parser::curr_lbp() const {
|
|
switch (curr()) {
|
|
case scanner::token_kind::Keyword:
|
|
return get_token_info().expr_precedence();
|
|
case scanner::token_kind::CommandKeyword: case scanner::token_kind::Eof:
|
|
case scanner::token_kind::QuotedSymbol:
|
|
return 0;
|
|
case scanner::token_kind::Identifier: case scanner::token_kind::Numeral:
|
|
case scanner::token_kind::Decimal: case scanner::token_kind::String:
|
|
case scanner::token_kind::Char:
|
|
return get_max_prec();
|
|
}
|
|
lean_unreachable(); // LCOV_EXCL_LINE
|
|
}
|
|
|
|
expr parser::parse_expr(unsigned rbp) {
|
|
expr left = parse_nud();
|
|
while (rbp < curr_lbp()) {
|
|
left = parse_led(left);
|
|
}
|
|
return left;
|
|
}
|
|
|
|
pair<optional<name>, expr> parser::parse_id_tk_expr(name const & tk, unsigned rbp) {
|
|
if (curr_is_identifier()) {
|
|
auto id_pos = pos();
|
|
name id = get_name_val();
|
|
next();
|
|
if (curr_is_token(tk)) {
|
|
next();
|
|
return mk_pair(optional<name>(id), parse_expr(rbp));
|
|
} else {
|
|
expr left = id_to_expr(id, id_pos);
|
|
while (rbp < curr_lbp()) {
|
|
left = parse_led(left);
|
|
}
|
|
return mk_pair(optional<name>(), left);
|
|
}
|
|
} else {
|
|
return mk_pair(optional<name>(), parse_expr(rbp));
|
|
}
|
|
}
|
|
|
|
pair<optional<name>, expr> parser::parse_qualified_expr(unsigned rbp) {
|
|
return parse_id_tk_expr(get_colon_tk(), rbp);
|
|
}
|
|
|
|
pair<optional<name>, expr> parser::parse_optional_assignment(unsigned rbp) {
|
|
return parse_id_tk_expr(get_assign_tk(), rbp);
|
|
}
|
|
|
|
expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environment const & lenv, unsigned rbp) {
|
|
local_scope scope(*this);
|
|
m_env = lenv;
|
|
for (unsigned i = 0; i < num_ps; i++)
|
|
add_local(ps[i]);
|
|
return parse_expr(rbp);
|
|
}
|
|
|
|
expr parser::parse_expr_with_env(local_environment const & lenv, unsigned rbp) {
|
|
flet<environment> set_env(m_env, lenv);
|
|
return parse_expr(rbp);
|
|
}
|
|
|
|
expr parser::parse_tactic(unsigned) {
|
|
lean_unreachable();
|
|
}
|
|
|
|
/** \brief Helper class for creating type context only if needed */
|
|
class lazy_type_context : public abstract_type_context {
|
|
environment const & m_env;
|
|
options const & m_opts;
|
|
std::unique_ptr<legacy_type_context> m_ctx;
|
|
legacy_type_context & ctx() {
|
|
if (!m_ctx)
|
|
m_ctx.reset(new legacy_type_context(m_env, m_opts));
|
|
return *m_ctx;
|
|
}
|
|
public:
|
|
lazy_type_context(environment const & env, options const & opts):m_env(env), m_opts(opts) {}
|
|
virtual ~lazy_type_context() {}
|
|
virtual environment const & env() const override { return const_cast<lazy_type_context*>(this)->ctx().env(); }
|
|
virtual expr whnf(expr const & e) override { return ctx().whnf(e); }
|
|
virtual bool is_def_eq(expr const & e1, expr const & e2) override { return ctx().is_def_eq(e1, e2); }
|
|
virtual expr infer(expr const & e) override { return ctx().infer(e); }
|
|
virtual expr check(expr const & e) override { return ctx().check(e); }
|
|
virtual optional<expr> is_stuck(expr const & e) override { return ctx().is_stuck(e); }
|
|
};
|
|
|
|
void parser::parse_command() {
|
|
lean_assert(curr() == scanner::token_kind::CommandKeyword);
|
|
m_last_cmd_pos = pos();
|
|
name const & cmd_name = get_token_info().value();
|
|
m_cmd_token = get_token_info().token();
|
|
if (auto it = cmds().find(cmd_name)) {
|
|
lazy_type_context tc(m_env, get_options());
|
|
scope_global_ios scope1(m_ios);
|
|
scope_trace_env scope2(m_env, m_ios.get_options(), tc);
|
|
if (is_notation_cmd(cmd_name)) {
|
|
in_notation_ctx ctx(*this);
|
|
next();
|
|
m_env = it->get_fn()(*this);
|
|
} else {
|
|
next();
|
|
m_env = it->get_fn()(*this);
|
|
}
|
|
} else {
|
|
auto p = pos();
|
|
next();
|
|
throw parser_error(sstream() << "unknown command '" << cmd_name << "'", p);
|
|
}
|
|
}
|
|
|
|
static optional<std::string> try_file(std::string const & base, optional<unsigned> const & k, name const & f, char const * ext) {
|
|
try {
|
|
return optional<std::string>(find_file(base, k, f, ext));
|
|
} catch (...) {
|
|
return optional<std::string>();
|
|
}
|
|
}
|
|
|
|
void parser::parse_imports() {
|
|
buffer<module_name> olean_files;
|
|
bool prelude = false;
|
|
std::string base = m_base_dir ? *m_base_dir : dirname(get_stream_name().c_str());
|
|
bool imported = false;
|
|
unsigned fingerprint = 0;
|
|
if (curr_is_token(get_prelude_tk())) {
|
|
next();
|
|
prelude = true;
|
|
}
|
|
auto import_olean = [&](optional<unsigned> const & k, name const & f) {
|
|
if (auto it = try_file(base, k, f, ".olean")) {
|
|
olean_files.push_back(module_name(k, f));
|
|
} else {
|
|
m_found_errors = true;
|
|
if (!m_use_exceptions && m_show_errors) {
|
|
flycheck_error err(ios());
|
|
display_error_pos(pos());
|
|
ios().get_regular_stream() << " invalid import, unknown module '" << f << "'" << std::endl;
|
|
}
|
|
if (m_use_exceptions)
|
|
throw parser_error(sstream() << "invalid import, unknown module '" << f << "'", pos());
|
|
}
|
|
};
|
|
if (!prelude) {
|
|
import_olean(optional<unsigned>(), "init");
|
|
}
|
|
while (curr_is_token(get_import_tk())) {
|
|
imported = true;
|
|
m_last_cmd_pos = pos();
|
|
next();
|
|
while (true) {
|
|
optional<unsigned> k;
|
|
while (true) {
|
|
if (curr_is_token(get_period_tk())) {
|
|
next();
|
|
if (!k)
|
|
k = 0;
|
|
else
|
|
k = *k + 1;
|
|
} else if (curr_is_token(get_ellipsis_tk())) {
|
|
next();
|
|
if (!k)
|
|
k = 2;
|
|
else
|
|
k = *k + 3;
|
|
} else {
|
|
break;
|
|
}
|
|
}
|
|
if (!curr_is_identifier())
|
|
break;
|
|
name f = get_name_val();
|
|
fingerprint = hash(fingerprint, f.hash());
|
|
if (k)
|
|
fingerprint = hash(fingerprint, *k);
|
|
import_olean(k, f);
|
|
next();
|
|
}
|
|
}
|
|
unsigned num_threads = 0;
|
|
if (get_parser_parallel_import(m_ios.get_options()))
|
|
num_threads = m_num_threads;
|
|
bool keep_imported_thms = (m_keep_theorem_mode == keep_theorem_mode::All);
|
|
m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads,
|
|
keep_imported_thms, m_ios);
|
|
m_env = update_fingerprint(m_env, fingerprint);
|
|
m_env = activate_export_decls(m_env, {}); // explicitly activate exports in root namespace
|
|
m_env = replay_export_decls_core(m_env, m_ios);
|
|
if (imported)
|
|
commit_info(1, 0);
|
|
}
|
|
|
|
void parser::commit_info(unsigned line, unsigned col) {
|
|
save_snapshot();
|
|
if (m_info_manager) {
|
|
m_info_manager->save_environment_options(line, col, m_env, m_ios.get_options());
|
|
m_info_manager->commit_upto(line, true);
|
|
}
|
|
}
|
|
|
|
bool parser::parse_commands() {
|
|
// We disable hash-consing while parsing to make sure the pos-info are correct.
|
|
scoped_expr_caching disable(false);
|
|
scoped_set_distinguishing_pp_options set(get_distinguishing_pp_options());
|
|
scope_pos_info_provider scope1(*this);
|
|
scope_info_manager scope2(m_info_manager);
|
|
try {
|
|
bool done = false;
|
|
protected_call([&]() {
|
|
parse_imports();
|
|
},
|
|
[&]() { sync_command(); });
|
|
if (has_sorry(m_env)) {
|
|
#ifndef LEAN_IGNORE_SORRY
|
|
// TODO(Leo): remove the #ifdef.
|
|
// The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
|
|
// We use it to avoid a buch of warnings on cdash.
|
|
flycheck_warning wrn(ios());
|
|
display_warning_pos(pos());
|
|
ios().get_regular_stream() << " imported file uses 'sorry'" << std::endl;
|
|
#endif
|
|
}
|
|
while (!done) {
|
|
if (m_stop_at && pos().first > m_stop_at_line) {
|
|
throw interrupt_parser();
|
|
}
|
|
protected_call([&]() {
|
|
check_interrupted();
|
|
switch (curr()) {
|
|
case scanner::token_kind::CommandKeyword:
|
|
if (curr_is_token(get_end_tk()))
|
|
commit_info();
|
|
parse_command();
|
|
commit_info();
|
|
break;
|
|
case scanner::token_kind::Eof:
|
|
done = true;
|
|
break;
|
|
case scanner::token_kind::Keyword:
|
|
if (curr_is_token(get_period_tk())) {
|
|
next();
|
|
break;
|
|
}
|
|
default:
|
|
throw parser_error("command expected", pos());
|
|
}
|
|
},
|
|
[&]() { sync_command(); });
|
|
}
|
|
if (has_open_scopes(m_env)) {
|
|
m_found_errors = true;
|
|
if (!m_use_exceptions && m_show_errors)
|
|
display_error("invalid end of module, expecting 'end'", pos());
|
|
else if (m_use_exceptions)
|
|
throw_parser_exception("invalid end of module, expecting 'end'", pos());
|
|
}
|
|
} catch (interrupt_parser) {
|
|
commit_info();
|
|
while (has_open_scopes(m_env))
|
|
m_env = pop_scope_core(m_env, m_ios);
|
|
}
|
|
commit_info(m_scanner.get_line()+1, 0);
|
|
|
|
protected_call(
|
|
[&]() {
|
|
m_theorem_queue.for_each([&](certified_declaration const & thm) {
|
|
if (keep_new_thms()) {
|
|
name const & thm_name = thm.get_declaration().get_name();
|
|
if (m_env.get(thm_name).is_axiom())
|
|
replace_theorem(thm);
|
|
}
|
|
});
|
|
},
|
|
[]() {});
|
|
return !m_found_errors;
|
|
}
|
|
|
|
bool parser::curr_is_command_like() const {
|
|
switch (curr()) {
|
|
case scanner::token_kind::CommandKeyword:
|
|
return true;
|
|
case scanner::token_kind::Eof:
|
|
return true;
|
|
case scanner::token_kind::Keyword:
|
|
return curr_is_token(get_period_tk());
|
|
default:
|
|
return false;
|
|
}
|
|
}
|
|
|
|
void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls,
|
|
expr const & t, expr const & v) {
|
|
m_theorem_queue_set.insert(n);
|
|
m_theorem_queue.add(env, n, ls, get_local_level_decls(), t, v);
|
|
}
|
|
|
|
void parser::add_delayed_theorem(certified_declaration const & cd) {
|
|
m_theorem_queue_set.insert(cd.get_declaration().get_name());
|
|
m_theorem_queue.add(cd);
|
|
}
|
|
|
|
void parser::replace_theorem(certified_declaration const & thm) {
|
|
m_env = m_env.replace(thm);
|
|
name const & thm_name = thm.get_declaration().get_name();
|
|
if (!m_ignore_noncomputable && !check_computable(m_env, thm_name)) {
|
|
throw exception(sstream() << "declaration '" << thm_name
|
|
<< "' was marked as a theorem, but it is a noncomputable definition");
|
|
}
|
|
}
|
|
|
|
environment parser::reveal_theorems_core(buffer<name> const & ds, bool all) {
|
|
m_theorem_queue.for_each([&](certified_declaration const & thm) {
|
|
if (keep_new_thms()) {
|
|
name const & thm_name = thm.get_declaration().get_name();
|
|
if (m_env.get(thm_name).is_axiom() &&
|
|
(all || std::any_of(ds.begin(), ds.end(), [&](name const & n) { return n == thm_name; }))) {
|
|
replace_theorem(thm);
|
|
m_theorem_queue_set.erase(thm_name);
|
|
}
|
|
}
|
|
});
|
|
return m_env;
|
|
}
|
|
|
|
environment parser::reveal_theorems(buffer<name> const & ds) {
|
|
return reveal_theorems_core(ds, false);
|
|
}
|
|
|
|
environment parser::reveal_all_theorems() {
|
|
return reveal_theorems_core(buffer<name>(), true);
|
|
}
|
|
|
|
void parser::save_snapshot() {
|
|
m_pre_info_manager.clear();
|
|
if (!m_snapshot_vector)
|
|
return;
|
|
if (m_snapshot_vector->empty() || static_cast<int>(m_snapshot_vector->back().m_line) != m_scanner.get_line())
|
|
m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls,
|
|
m_level_variables, m_variables, m_include_vars,
|
|
m_ios.get_options(), m_parser_scope_stack, m_scanner.get_line()));
|
|
}
|
|
|
|
void parser::save_pre_info_data() {
|
|
// if elaborator failed, then m_pre_info_data contains type information before elaboration.
|
|
if (m_info_manager) {
|
|
bool overwrite = false;
|
|
m_info_manager->merge(m_pre_info_manager, overwrite);
|
|
m_pre_info_manager.clear();
|
|
}
|
|
}
|
|
|
|
void parser::save_overload(expr const & e) {
|
|
if (!m_info_manager || !is_choice(e))
|
|
return;
|
|
auto p = pos_of(e);
|
|
m_info_manager->add_overload_info(p.first, p.second, e);
|
|
}
|
|
|
|
void parser::save_overload_notation(list<expr> const & as, pos_info const & p) {
|
|
if (!m_info_manager || length(as) <= 1)
|
|
return;
|
|
m_info_manager->add_overload_notation_info(p.first, p.second, as);
|
|
}
|
|
void parser::save_overload_notation(list<notation::accepting> const & as, pos_info const & p) {
|
|
if (!m_info_manager || length(as) <= 1)
|
|
return;
|
|
list<expr> new_as =
|
|
map2<expr, notation::accepting, std::function<expr(notation::accepting const &)>>
|
|
(as, [](notation::accepting const & p) { return p.get_expr(); });
|
|
save_overload_notation(new_as, p);
|
|
}
|
|
void parser::save_identifier_info(pos_info const & p, name const & full_id) {
|
|
if (!m_info_manager)
|
|
return;
|
|
m_info_manager->add_identifier_info(p.first, p.second, full_id);
|
|
}
|
|
|
|
void parser::save_type_info(expr const & e) {
|
|
if (!m_info_manager)
|
|
return;
|
|
if (is_explicit(e)) {
|
|
save_type_info(get_explicit_arg(e));
|
|
} else if (is_as_atomic(e)) {
|
|
save_type_info(get_as_atomic_arg(e));
|
|
} else if (is_choice(e)) {
|
|
for (unsigned i = 0; i < get_num_choices(e); i++)
|
|
save_type_info(get_choice(e, i));
|
|
} else if (is_app(e)) {
|
|
save_type_info(get_app_fn(e));
|
|
} else if (is_constant(e)) {
|
|
auto d = m_env.find(const_name(e));
|
|
if (!d)
|
|
return;
|
|
auto p = pos_of(e);
|
|
m_pre_info_manager.add_type_info(p.first, p.second, d->get_type());
|
|
} else if (is_local(e)) {
|
|
auto p = pos_of(e);
|
|
expr t = mlocal_type(e);
|
|
if (is_meta(t))
|
|
return;
|
|
m_pre_info_manager.add_type_info(p.first, p.second, t);
|
|
}
|
|
}
|
|
|
|
optional<pos_info> parser::get_pos_info(expr const & e) const {
|
|
tag t = e.get_tag();
|
|
if (t == nulltag)
|
|
return optional<pos_info>();
|
|
if (auto it = m_pos_table.find(t))
|
|
return optional<pos_info>(*it);
|
|
else
|
|
return optional<pos_info>();
|
|
}
|
|
|
|
pos_info parser::get_some_pos() const {
|
|
return m_last_cmd_pos;
|
|
}
|
|
|
|
char const * parser::get_file_name() const {
|
|
return get_stream_name().c_str();
|
|
}
|
|
|
|
bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name,
|
|
optional<std::string> const & base_dir, bool use_exceptions,
|
|
unsigned num_threads, definition_cache * cache, declaration_index * index,
|
|
keep_theorem_mode tmode) {
|
|
parser p(env, ios, in, strm_name, base_dir, use_exceptions, num_threads, nullptr, nullptr, nullptr, tmode);
|
|
p.set_cache(cache);
|
|
p.set_index(index);
|
|
bool r = p();
|
|
ios = p.ios();
|
|
env = p.env();
|
|
return r;
|
|
}
|
|
|
|
bool parse_commands(environment & env, io_state & ios, char const * fname, optional<std::string> const & base_dir,
|
|
bool use_exceptions, unsigned num_threads,
|
|
definition_cache * cache, declaration_index * index, keep_theorem_mode tmode) {
|
|
std::ifstream in(fname);
|
|
if (in.bad() || in.fail())
|
|
throw exception(sstream() << "failed to open file '" << fname << "'");
|
|
return parse_commands(env, ios, in, fname, base_dir, use_exceptions, num_threads, cache, index, tmode);
|
|
}
|
|
|
|
void initialize_parser() {
|
|
g_parser_show_errors = new name{"parser", "show_errors"};
|
|
g_parser_parallel_import = new name{"parser", "parallel_import"};
|
|
g_new_elaborator = new name{"new_elaborator"};
|
|
register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS,
|
|
"(lean parser) display error messages in the regular output channel");
|
|
register_bool_option(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT,
|
|
"(lean parser) import modules in parallel");
|
|
register_bool_option(*g_new_elaborator, false, "(lean parser) use new elaborator");
|
|
g_tmp_prefix = new name(name::mk_internal_unique_name());
|
|
g_anonymous_inst_name_prefix = new name("_inst");
|
|
}
|
|
|
|
void finalize_parser() {
|
|
delete g_anonymous_inst_name_prefix;
|
|
delete g_tmp_prefix;
|
|
delete g_parser_show_errors;
|
|
delete g_parser_parallel_import;
|
|
delete g_new_elaborator;
|
|
}
|
|
}
|