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

fix(frontends/lean/elaborator): fix segfault

Browse source
This commit is contained in:
Gabriel Ebner 2017-05-09 18:06:25 +02:00
parent 8f7608433a
commit d2b6b3f573
1 changed files with 13 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/frontends/lean/elaborator.cpp
View file

@ -2777,17 +2777,19 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
expr fval = *new_new_fval;
buffer<expr> args;
expr fn = get_app_args(fval, args);
declaration decl = m_env.get(const_name(fn));
expr default_val = instantiate_value_univ_params(decl, const_levels(fn));
// clean up 'id' application inserted by `structure_cmd::declare_defaults`
default_val = replace(default_val, [](expr const & e) {
if (is_app_of(e, get_id_name(), 2)) {
return some_expr(app_arg(e));
}
return none_expr();
});
fval = mk_app(default_val, args);
fval = head_beta_reduce(fval);
if (is_constant(fn)) {
declaration decl = m_env.get(const_name(fn));
expr default_val = instantiate_value_univ_params(decl, const_levels(fn));
// clean up 'id' application inserted by `structure_cmd::declare_defaults`
default_val = replace(default_val, [](expr const &e) {
if (is_app_of(e, get_id_name(), 2)) {
return some_expr(app_arg(e));
}
return none_expr();
});
fval = mk_app(default_val, args);
fval = head_beta_reduce(fval);
}
if (!reduce_and_check_deps(fval))
return;