From 887de5d0afc27b122472e2a5b7203a04ad6bc3c1 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 16 Aug 2017 11:49:51 +0200
Subject: [PATCH] Change coq backend requirements

Remove the automatic clausification encoding of the coq backend, which
was slow because of the 'tauto' tactic. It was particularly a problem
for long problems, since the tauto tactic would take longer each time
because of the new hypotheses. The buren is now on the hands of the
functor argument, which hopefully should be able to do it better.
---
 src/backend/coq.ml  | 16 +++-------------
 src/backend/coq.mli |  6 +++++-
 2 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/src/backend/coq.ml b/src/backend/coq.ml
index c8915000..43f618b8 100644
--- a/src/backend/coq.ml
+++ b/src/backend/coq.ml
@@ -32,7 +32,6 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     end)
 
   let name c = c.S.St.name
-  let name_tmp c = c.S.St.name ^ "_tmp"
 
   let pp_atom fmt a =
     if a == S.St.(a.var.pa) then
@@ -60,12 +59,6 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     in
     aux M.empty c.S.St.atoms 0
 
-  let clausify fmt clause =
-    Format.fprintf fmt "(* Encoding theory clause %s into: %s *)@\n"
-      (name_tmp clause) (name clause);
-    Format.fprintf fmt "assert (%s: %a).@\ntauto. clear %s.@\n"
-      (name clause) pp_clause clause (name_tmp clause)
-
   let clause_iter m format fmt clause =
     let aux atom = Format.fprintf fmt format (M.find atom m) in
     Array.iter aux clause.S.St.atoms
@@ -121,14 +114,11 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     let clause = node.S.conclusion in
     match node.S.step with
     | S.Hypothesis ->
-      A.prove_hyp fmt (name_tmp clause) clause;
-      clausify fmt clause
+      A.prove_hyp fmt (name clause) clause
     | S.Assumption ->
-      A.prove_assumption fmt (name_tmp clause) clause;
-      clausify fmt clause
+      A.prove_assumption fmt (name clause) clause
     | S.Lemma _ ->
-      A.prove_lemma fmt (name_tmp clause) clause;
-      clausify fmt clause
+      A.prove_lemma fmt (name clause) clause
     | S.Duplicate (p, l) ->
       let c = (S.expand p).S.conclusion in
       elim_duplicate fmt clause c l
diff --git a/src/backend/coq.mli b/src/backend/coq.mli
index 76faabfc..9d26b806 100644
--- a/src/backend/coq.mli
+++ b/src/backend/coq.mli
@@ -31,7 +31,11 @@ module type Arg = sig
   val prove_assumption : Format.formatter -> string -> assumption -> unit
   (** Proving function for hypotheses, lemmas and assumptions.
       [prove_x fmt name x] should prove [x], and be such that after
-      executing it, [x] is among the coq hypotheses under the name [name]. *)
+      executing it, [x] is among the coq hypotheses under the name [name].
+      The hypothesis should be the encoding of the given clause, i.e
+      for a clause [a \/ not b \/ c], the proved hypothesis should be:
+      [ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the
+      one in the atoms array of the clause. *)
 
 end