From beb355f798e7ef90cc0696981ee64459c2a8d505 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 9 Jan 2017 17:02:41 +0100
Subject: [PATCH] feat(tools/super): clausify during preprocessing

Some inference produce terms with large useless redexes such as
(prod.fst (prod.mk _ _)).  Since we do normalization during
preprocessing, we can avoid ever even looking at these terms.
---
 library/tools/super/clausifier.lean | 9 ++++++++-
 library/tools/super/prover.lean     | 1 +
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/library/tools/super/clausifier.lean b/library/tools/super/clausifier.lean
index fc755ce154..9a184f44b1 100644
--- a/library/tools/super/clausifier.lean
+++ b/library/tools/super/clausifier.lean
@@ -269,7 +269,14 @@ local_false ← target,
 l ← local_context,
 monad.for l (clause.of_proof local_false)
 
-@[super.inf]
+meta def clausify_pre := preprocessing_rule $ take new, lift list.join $ for new $ λ dc, do
+cs ← get_clauses_classical [dc^.c],
+if cs^.length ≤ 1 then
+  return (for cs $ λ c, { dc with c := c })
+else
+  for cs (λc, mk_derived c dc^.sc)
+
+-- @[super.inf]
 meta def clausification_inf : inf_decl := inf_decl.mk 0 $
 λgiven, list.foldr orelse (return ()) $
         do r ← clausification_rules_classical,
diff --git a/library/tools/super/prover.lean b/library/tools/super/prover.lean
index ba3110b4ed..03a64b69a8 100644
--- a/library/tools/super/prover.lean
+++ b/library/tools/super/prover.lean
@@ -74,6 +74,7 @@ run_prover_loop (i+1)
 
 meta def default_preprocessing : list (prover unit) :=
 [
+clausify_pre,
 factor_dup_lits_pre,
 remove_duplicates_pre,
 refl_r_pre,