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

fix(inductive_compiler/ginductive.cpp): populate new fields of entry

Browse source
This commit is contained in:
Daniel Selsam 2017-03-03 19:20:01 -08:00 • committed by Leonardo de Moura
parent 616a4ce5c5
commit dc5b57bff6
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/inductive_compiler/ginductive.cpp
View file

@ -27,6 +27,7 @@ static unsigned compute_idx_number(expr const & e) {
return idx;
} else if (is_constant(fn) && const_name(fn) == get_psum_inr_name()) {
idx++;
lean_assert(args.size() == 2);
it = args[2];
} else {
return idx;
@ -257,6 +258,7 @@ struct ginductive_modification : public modification {
environment register_ginductive_decl(environment const & env, ginductive_decl const & decl, ginductive_kind k) {
ginductive_entry entry;
entry.m_kind = k;
entry.m_from_mutual = decl.is_from_mutual();
entry.m_num_params = decl.get_num_params();
buffer<name> inds;
@ -274,6 +276,9 @@ environment register_ginductive_decl(environment const & env, ginductive_decl co
}
entry.m_intro_rules = to_list(intro_rules);
entry.m_ir_offsets = to_list(decl.get_ir_offsets());
entry.m_idx_to_ir_range = to_list(decl.get_idx_to_ir_range());
return module::add_and_perform(env, std::make_shared<ginductive_modification>(entry));
}

2
src/library/inductive_compiler/ginductive_decl.h
View file

@ -24,8 +24,6 @@ class ginductive_decl {
optional<simp_lemmas> m_sizeof_lemmas;
public:
ginductive_decl() {}
ginductive_decl(unsigned nest_depth, buffer<name> const & lp_names, buffer<expr> const & params, buffer<unsigned> const & ir_offsets):
m_nest_depth(nest_depth), m_from_mutual(true), m_lp_names(lp_names), m_params(params), m_ir_offsets(ir_offsets) {}