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

fix(frontends/lean): race condition

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-21 09:32:13 -07:00
parent de657e8df0
commit ad87c0b3e1
3 changed files with 9 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/decl_cmds.cpp
View file

@ -265,15 +265,16 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
if (is_theorem) {
if (p.num_threads() > 1) {
// add as axiom, and create a task to prove the theorem
expr saved_type = type;
expr saved_value = value;
environment saved_env = env;
expr saved_type = type;
expr saved_value = value;
environment saved_env = env;
local_level_decls saved_lls = p.get_local_level_decls();
std::tie(type, new_ls) = p.elaborate_type(type);
env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
p.add_delayed_theorem([=, &p]() {
level_param_names new_ls;
expr type, value;
std::tie(type, value, new_ls) = p.elaborate_definition_at(saved_env, n, saved_type, saved_value);
std::tie(type, value, new_ls) = p.elaborate_definition_at(saved_env, saved_lls, n, saved_type, saved_value);
return check(saved_env, mk_theorem(real_n, append(ls, new_ls), type, value));
});
} else {

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

@ -494,10 +494,10 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name cons
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp);
}
std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, name const & n, expr const & t,
expr const & v) {
std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
name const & n, expr const & t, expr const & v) {
parser_pos_provider pp = get_pos_provider();
return ::lean::elaborate(env, m_local_level_decls, m_ios, n, t, v, &pp);
return ::lean::elaborate(env, lls, m_ios, n, t, v, &pp);
}
[[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {

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

@ -263,7 +263,7 @@ public:
/** \brief Elaborate the definition n : t := v */
std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
/** \brief Elaborate the definition n : t := v in the given environment*/
std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, name const & n, expr const & t, expr const & v);
std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls, name const & n, expr const & t, expr const & v);
parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); }