tactic haRVey pour appeler haRVey (contrib/dp)

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

3 files changed, 32 insertions, 5 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index fd508454a..9a0ad2bb6 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -266,6 +266,7 @@ let rec tr_arith_constant t = match kind_of_term t with
 (* translate a Coq term t:Set into a FOL type expression;
    tv = list of type variables *)
 and tr_type tv env t =
+  let t = Reductionops.nf_betadeltaiota env Evd.empty t in
   if t = Lazy.force coq_Z then 
     Tid ("int", [])
   else match kind_of_term t with
@@ -682,6 +683,28 @@ let call_cvcl fwhy =
   if not !debug then remove_files [fwhy; fcvc];
   r
 
+let call_harvey fwhy =
+  if Sys.command (sprintf "why --harvey %s" fwhy) <> 0 then
+    anomaly ("call to why --harvey " ^ fwhy ^ " failed; please report");
+  let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
+  let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in
+  if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed");
+  let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in
+  let outf = Filename.temp_file "rv" ".out" in
+  let out = 
+    Sys.command (sprintf "timeout 10 rv -e\"-T 2000\" %s > %s 2>&1" f outf) 
+  in
+  let r =
+    if out <> 0 then 
+      Timeout
+    else
+      let cmd = 
+	sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf
+      in
+      if Sys.command cmd = 0 then Valid else Invalid
+  in
+  if not !debug then remove_files [fwhy; frv; outf];
+  r
 
 let call_prover prover q =
   let fwhy = Filename.temp_file "coq_dp" ".why" in
@@ -691,7 +714,7 @@ let call_prover prover q =
     | Simplify -> call_simplify fwhy
     | Zenon -> call_zenon fwhy
     | CVCLite -> call_cvcl fwhy
-    | Harvey -> error "haRVey not yet interfaced"
+    | Harvey -> call_harvey fwhy
   
 let dp prover gl =
   let concl_type = pf_type_of gl (pf_concl gl) in
diff --git a/contrib/dp/test2.v b/contrib/dp/test2.v
index 8aba348d8..4e933a3cd 100644
--- a/contrib/dp/test2.v
+++ b/contrib/dp/test2.v
@@ -28,6 +28,11 @@ Goal 1::2::3::nil = 1::2::(1+2)::nil.
   zenon.
   Admitted.
 
+Definition T := nat.
+Parameter fct : T -> nat.
+Goal fct O = O.
+ Admitted.
+
 Fixpoint even (n:nat) : Prop :=
   match n with 
   O => True
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index c41a46173..52a57a0cb 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -56,7 +56,7 @@ Qed.
 (* Universal quantifier *)
 
 Goal (forall (x y : Z), x = y) -> 0=1.
-zenon.
+try zenon.
 simplify.
 Qed.
 
@@ -106,7 +106,6 @@ Inductive even : Z -> Prop :=
    unlike CVC Lite *)
 
 Goal even 4.
-
 cvcl.
 Qed.
 
@@ -185,7 +184,7 @@ Parameter foo : Set.
 Parameter ff : nat -> foo -> foo -> nat.
 Parameter g : foo -> foo.
 Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O.
-simplify.      
+zenon.
 Qed.
 
 
@@ -195,7 +194,7 @@ Qed.
 Parameter poly_f : forall A:Set, A->A.
 
 Goal forall x:nat, poly_f nat x = poly_f nat x.
-simplify.
+zenon.
 Qed.