max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean): save/restore fresh name_generator state in parser snapshots

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-06 13:25:34 -08:00
parent 799cc9b03d
commit 8eb34a39cb
3 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/module_parser.cpp
View file

@ -34,7 +34,7 @@ module_parser::~module_parser() {}
pair<cancellation_token, task<module_parser_result>>
module_parser::resume(module_parser_result const & res, optional<std::vector<gtask>> const & dependencies) {
auto & s = *res.m_snapshot_at_end;
snapshot const & s = *res.m_snapshot_at_end;
m_parser.m_scanner.skip_to_pos(s.m_pos);
m_parser.m_env = s.m_env;
m_parser.m_ios.set_options(s.m_options);
@ -47,7 +47,7 @@ module_parser::resume(module_parser_result const & res, optional<std::vector<gta
m_parser.m_ignore_noncomputable = s.m_noncomputable_theory;
m_parser.m_parser_scope_stack = s.m_parser_scope_stack;
m_parser.m_next_inst_idx = s.m_next_inst_idx;
set_fresh_name_generator(s.m_name_gen_snapshot);
auto lt = res.m_lt;
scope_log_tree_core scope_lt(&lt);
return parse_next_command_like(dependencies);

2
src/frontends/lean/module_parser.h
View file

@ -43,7 +43,7 @@ class module_parser : public std::enable_shared_from_this<module_parser> {
public:
module_parser(std::string const & file_name, std::string const & content,
environment const & initial_env, module_loader const & import_fn);
environment const & initial_env, module_loader const & import_fn);
~module_parser();
void use_separate_tasks(bool separate_tasks) { m_separate_tasks = separate_tasks; }

5
src/frontends/lean/parser_state.h
View file

@ -522,12 +522,15 @@ struct snapshot {
parser_scope_stack m_parser_scope_stack;
unsigned m_next_inst_idx;
pos_info m_pos;
name_generator m_name_gen_snapshot;
snapshot(environment const & env, local_level_decls const & lds,
local_expr_decls const & eds, name_set const & lvars, name_set const & vars,
name_set const & includes, options const & opts, bool imports_parsed, bool noncomputable_theory, parser_scope_stack const & pss,
unsigned next_inst_idx, pos_info const & pos):
m_env(env), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
m_options(opts), m_imports_parsed(imports_parsed), m_noncomputable_theory(noncomputable_theory), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos) {}
m_options(opts), m_imports_parsed(imports_parsed), m_noncomputable_theory(noncomputable_theory),
m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos),
m_name_gen_snapshot(get_fresh_name_generator_snapshot()) {}
};
}