contrib/dp: tactique ergo (voir ergo.lri.fr)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9453 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 21 insertions, 2 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 412786e1f8..1702aecf50 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -639,7 +639,7 @@ let tr_goal gl =
   hyps, c
 
 
-type prover = Simplify | CVCLite | Harvey | Zenon
+type prover = Simplify | Ergo | CVCLite | Harvey | Zenon
 
 let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ())
 
@@ -661,6 +661,18 @@ let call_simplify fwhy =
   if not !debug then remove_files [fwhy; fsx];
   r
 
+let call_ergo fwhy =
+  let cmd = 
+    sprintf "timeout %d ergo %s > out 2>&1 && grep -q -w Valid out" 
+      !timeout fwhy
+  in
+  let out = Sys.command cmd in
+  let r = 
+    if out = 0 then Valid None else if out = 1 then Invalid else Timeout 
+  in
+  if not !debug then remove_files [fwhy];
+  r
+
 let call_zenon fwhy =
   let cmd = sprintf "why --no-prelude --no-zenon-prelude --zenon %s" fwhy in
   if Sys.command cmd <> 0 then
@@ -724,9 +736,10 @@ let call_harvey fwhy =
 let call_prover prover q =
   let fwhy = Filename.temp_file "coq_dp" ".why" in
   Dp_why.output_file fwhy q;
-  if !debug then ignore (Sys.command (sprintf "cat %s" fwhy));
+  if !debug then Format.eprintf "Why file: %s@." fwhy;
   match prover with
     | Simplify -> call_simplify fwhy
+    | Ergo -> call_ergo fwhy
     | Zenon -> call_zenon fwhy
     | CVCLite -> call_cvcl fwhy
     | Harvey -> call_harvey fwhy
@@ -748,6 +761,7 @@ let dp prover gl =
   
 
 let simplify = tclTHEN intros (dp Simplify)
+let ergo = tclTHEN intros (dp Ergo)
 let cvc_lite = tclTHEN intros (dp CVCLite)
 let harvey = dp Harvey
 let zenon = tclTHEN intros (dp Zenon)
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index 841c388730..5fa4a6d574 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -3,6 +3,7 @@ open Libnames
 open Proof_type
 
 val simplify : tactic
+val ergo : tactic
 val cvc_lite : tactic
 val harvey : tactic
 val zenon : tactic
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index afbd592246..e22339e1ed 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -16,6 +16,10 @@ TACTIC EXTEND Simplify
   [ "simplify" ] -> [ simplify ]
 END
 
+TACTIC EXTEND Simplify
+  [ "ergo" ] -> [ ergo ]
+END
+
 TACTIC EXTEND CVCLite
   [ "cvcl" ] -> [ cvc_lite ]
 END