michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parser): add anonymous inst implicit name generator

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-13 11:45:47 -08:00
parent ef546c5c5b
commit a9b567296c
2 changed files with 22 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/frontends/lean/parser.cpp
View file

@ -80,6 +80,8 @@ bool get_parser_parallel_import(options const & opts) {
}
// ==========================================
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);
@ -156,7 +158,8 @@ parser::parser(environment const & env, io_state const & ios,
m_found_errors = false;
m_used_sorry = false;
updt_options();
m_next_tag_idx = 0;
m_next_tag_idx = 0;
m_next_inst_idx = 1;
m_curr = scanner::token_kind::Identifier;
protected_call([&]() { scan(); },
[&]() { sync_command(); });
@ -416,6 +419,12 @@ tag parser::get_tag(expr e) {
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;
}
expr parser::save_pos(expr e, pos_info p) {
auto t = get_tag(e);
if (!m_pos_table.contains(t))
@ -560,7 +569,7 @@ void parser::push_local_scope(bool save_options) {
if (save_options)
opts = m_ios.get_options();
m_parser_scope_stack = cons(parser_scope_stack_elem(opts, m_level_variables, m_variables, m_include_vars,
m_undef_ids.size(), m_has_params, m_local_level_decls,
m_undef_ids.size(), m_next_inst_idx, m_has_params, m_local_level_decls,
m_local_decls),
m_parser_scope_stack);
}
@ -580,6 +589,7 @@ void parser::pop_local_scope() {
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;
m_undef_ids.shrink(s.m_num_undef_ids);
m_parser_scope_stack = tail(m_parser_scope_stack);
}
@ -1069,7 +1079,7 @@ void parser::parse_inst_implicit_decl(buffer<expr> & r, binder_info const & bi)
type = parse_expr();
} else {
expr left = id_to_expr(id, id_pos);
id = name("_inst");
id = mk_anonymous_inst_name();
unsigned rbp = 0;
while (rbp < curr_expr_lbp()) {
left = parse_led(left);
@ -1077,7 +1087,7 @@ void parser::parse_inst_implicit_decl(buffer<expr> & r, binder_info const & bi)
type = left;
}
} else {
id = name("_inst");
id = mk_anonymous_inst_name();
type = parse_expr();
}
save_identifier_info(id_pos, id);
@ -2396,9 +2406,11 @@ void initialize_parser() {
g_tmp_prefix = new name(name::mk_internal_unique_name());
g_lua_module_key = new std::string("lua_module");
register_module_object_reader(*g_lua_module_key, lua_module_reader);
g_anonymous_inst_name_prefix = new name("_inst");
}
void finalize_parser() {
delete g_anonymous_inst_name_prefix;
delete g_lua_module_key;
delete g_tmp_prefix;
delete g_parser_show_errors;

8
src/frontends/lean/parser.h
View file

@ -52,14 +52,15 @@ struct parser_scope_stack_elem {
name_set m_variables;
name_set m_include_vars;
unsigned m_num_undef_ids;
unsigned m_next_inst_idx;
bool m_has_params;
local_level_decls m_local_level_decls;
local_expr_decls m_local_decls;
parser_scope_stack_elem(optional<options> const & o, name_set const & lvs, name_set const & vs, name_set const & ivs,
unsigned num_undef_ids, bool has_params,
unsigned num_undef_ids, unsigned next_inst_idx, bool has_params,
local_level_decls const & lld, local_expr_decls const & led):
m_options(o), m_level_variables(lvs), m_variables(vs), m_include_vars(ivs),
m_num_undef_ids(num_undef_ids), m_has_params(has_params), m_local_level_decls(lld), m_local_decls(led) {}
m_num_undef_ids(num_undef_ids), m_next_inst_idx(next_inst_idx), m_has_params(has_params), m_local_level_decls(lld), m_local_decls(led) {}
};
typedef list<parser_scope_stack_elem> parser_scope_stack;
@ -111,6 +112,7 @@ class parser {
pos_info m_last_cmd_pos;
pos_info m_last_script_pos;
unsigned m_next_tag_idx;
unsigned m_next_inst_idx;
bool m_found_errors;
bool m_used_sorry;
pos_info_table m_pos_table;
@ -185,6 +187,8 @@ class parser {
tag get_tag(expr e);
expr copy_with_new_pos(expr const & e, pos_info p);
name mk_anonymous_inst_name();
parse_table const & nud() const { return get_nud_table(env()); }
parse_table const & led() const { return get_led_table(env()); }
parse_table const & tactic_nud() const { return get_tactic_nud_table(env()); }