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

fix(frontends/lean/parser): save noncomputable theory flag in snapshots

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-30 11:15:30 +01:00 • committed by Leonardo de Moura
parent 941ba6d96c
commit 0f96809f7a
2 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -166,6 +166,7 @@ parser::parser(environment const & env, io_state const & ios,
m_imports_parsed(false),
m_snapshot_vector(sv) {
m_next_inst_idx = 1;
m_ignore_noncomputable = false;
if (s) {
m_env = s->m_env;
m_ios.set_options(s->m_options);
@ -176,10 +177,10 @@ parser::parser(environment const & env, io_state const & ios,
m_variables = s->m_vars;
m_include_vars = s->m_include_vars;
m_imports_parsed = s->m_imports_parsed;
m_ignore_noncomputable = s->m_noncomputable_theory;
m_parser_scope_stack = s->m_parser_scope_stack;
m_next_inst_idx = s->m_next_inst_idx;
}
m_ignore_noncomputable = false;
m_profile = ios.get_options().get_bool("profiler", false);
m_in_quote = false;
m_in_pattern = false;
@ -2385,7 +2386,7 @@ void parser::save_snapshot(scope_message_context & smc, pos_info p) {
m_snapshot_vector->push_back(std::make_shared<snapshot>(
m_env, smc.get_sub_buckets(), m_local_level_decls, m_local_decls,
m_level_variables, m_variables, m_include_vars,
m_ios.get_options(), m_imports_parsed, m_parser_scope_stack, m_next_inst_idx, p,
m_ios.get_options(), m_imports_parsed, m_ignore_noncomputable, m_parser_scope_stack, m_next_inst_idx, p,
m_required_successes));
}
}

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

@ -64,16 +64,17 @@ struct snapshot {
name_set m_include_vars; // subset of m_eds that must be included
options m_options;
bool m_imports_parsed;
bool m_noncomputable_theory;
parser_scope_stack m_parser_scope_stack;
unsigned m_next_inst_idx;
pos_info m_pos;
list<generic_task_result> m_required_successes;
snapshot(environment const & env, name_set const & sub_buckets, 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, parser_scope_stack const & pss,
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, list<generic_task_result> const & required_successes):
m_env(env), m_sub_buckets(sub_buckets), 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_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_required_successes(required_successes) {}
};