From 9d01d1bb04bb02687bb2752dca9fc2b63786e444 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 May 2016 11:24:12 -0700 Subject: [PATCH] chore(library/compiler/preprocess_rec): add extra assertions --- src/library/compiler/preprocess_rec.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/library/compiler/preprocess_rec.cpp b/src/library/compiler/preprocess_rec.cpp index 5a413af610..617f44bfd5 100644 --- a/src/library/compiler/preprocess_rec.cpp +++ b/src/library/compiler/preprocess_rec.cpp @@ -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 aux_decls; v = elim_recursors(m_env, d.get_name(), v, aux_decls); for (name const & n : aux_decls) {