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

chore(library/compiler/preprocess_rec): add extra assertions

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-11 11:24:12 -07:00
parent a581017d8d
commit 9d01d1bb04
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/compiler/preprocess_rec.cpp
View file

@ -117,15 +117,21 @@ public:
expr v = d.get_value();
lean_trace(name({"compiler", "input"}), tout() << "\n" << v << "\n";)
v = expand_aux_recursors(m_env, v);
lean_assert(check(d, v));
lean_trace(name({"compiler", "expand_aux_recursors"}), tout() << "\n" << v << "\n";)
v = mark_comp_irrelevant_subterms(m_env, v);
lean_assert(check(d, v));
v = eta_expand(m_env, v);
lean_assert(check(d, v));
lean_trace(name({"compiler", "eta_expansion"}), tout() << "\n" << v << "\n";)
v = simp_pr1_rec(m_env, v);
lean_assert(check(d, v));
lean_trace(name({"compiler", "simplify_pr1"}), tout() << "\n" << v << "\n";)
v = inline_simple_definitions(m_env, v);
lean_assert(check(d, v));
lean_trace(name({"compiler", "inline"}), tout() << "\n" << v << "\n";)
v = mark_comp_irrelevant_subterms(m_env, v);
lean_assert(check(d, v));
buffer<name> aux_decls;
v = elim_recursors(m_env, d.get_name(), v, aux_decls);
for (name const & n : aux_decls) {