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

fix(library/compiler/simp_inductive): adjust kernel projections

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-02 18:18:45 -07:00
parent c9aab6ef50
commit 1b95cbeca1
1 changed files with 21 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/library/compiler/simp_inductive.cpp
View file

@ -212,6 +212,26 @@ class erase_trivial_structures_fn : public simp_inductive_core_fn {
}
}
virtual expr visit_proj(expr const & e) override {
name const & S = proj_sname(e);
inductive_val S_val = env().get(S).to_inductive_val();
lean_assert(S_val.get_ncnstrs() == 1);
name const & k = head(S_val.get_cnstrs());
buffer<bool> rel_fields;
get_constructor_info(k, rel_fields);
unsigned idx = proj_idx(e).get_small_value();
lean_assert(idx < rel_fields.size());
if (!rel_fields[idx])
return mk_enf_neutral();
unsigned new_idx = 0;
for (unsigned j = 0; j < idx; j++) {
if (rel_fields[j])
new_idx++;
}
expr new_s = visit(proj_expr(e));
return mk_proj(S, new_idx, new_s);
}
virtual expr visit_app(expr const & e) override {
buffer<expr> args;
expr const & fn = get_app_args(e, args);
@ -227,6 +247,7 @@ class erase_trivial_structures_fn : public simp_inductive_core_fn {
}
return compiler_step_visitor::visit_app(e);
}
public:
erase_trivial_structures_fn(environment const & env, abstract_context_cache & cache):
simp_inductive_core_fn(env, cache) {}