From 04eb1ec1c5ed87f6b4c570a48614078bc19aa31f Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 9 Aug 2017 20:55:27 +0200
Subject: [PATCH] Fixes to the Coq backend

Formerly, clauses introduced by the theory were left as is, but it
should instead be 'clausified' i.e transformed into what msat expects
(which is an encoding of clauses).
---
 src/backend/coq.ml | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/backend/coq.ml b/src/backend/coq.ml
index 39009c2a..35ff1ab9 100644
--- a/src/backend/coq.ml
+++ b/src/backend/coq.ml
@@ -32,6 +32,7 @@ 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 ^ "_or"
 
   let pp_atom fmt a =
     if a == S.St.(a.var.pa) then
@@ -63,7 +64,9 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     Format.fprintf fmt "@].@\n";
     m
 
-  let clausify 
+  let clausify fmt clause =
+    Format.fprintf fmt "assert (%s: %a).@\nintros; try destruct %s; auto. clear %s.@\n"
+      (name clause) pp_clause clause (name_tmp clause) (name_tmp clause)
 
   let elim_duplicate fmt goal hyp _ =
     (** Printing info comment in coq *)
@@ -94,7 +97,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     Format.fprintf fmt "exact (%s%a).@\n"
       (name h1) (fun fmt -> Array.iter (fun b ->
           if b == a then begin
-            Format.fprintf fmt " (fun p => %s%a"
+            Format.fprintf fmt " (fun p => %s%a)"
               (name h2) (fun fmt -> (Array.iter (fun c ->
                   if c == a.S.St.neg then
                     Format.fprintf fmt " (fun np => np p)"
@@ -110,11 +113,14 @@ 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 clause) clause
+      A.prove_hyp fmt (name_tmp clause) clause;
+      clausify fmt clause
     | S.Assumption ->
-      A.prove_assumption fmt (name clause) clause
+      A.prove_assumption fmt (name_tmp clause) clause;
+      clausify fmt clause
     | S.Lemma _ ->
-      A.prove_lemma fmt (name clause) clause
+      A.prove_lemma fmt (name_tmp clause) clause;
+      clausify fmt clause
     | S.Duplicate (p, l) ->
       let c = (S.expand p).S.conclusion in
       elim_duplicate fmt clause c l
@@ -130,7 +136,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     let aux () node =
       Format.fprintf fmt "%a@\n@\n" (prove_node h) node
     in
-    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
+    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n@\n";
     S.fold aux () p
 
 end