bugs dp

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

5 files changed, 64 insertions, 14 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 8ac31ce93..b5ba3b00e 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -466,12 +466,14 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
 		   let b = br.(j) in
 		   let rec_vars, b = decompose_lam b in
 		   let rec_vars, env = coq_rename_vars env rec_vars in
-		   let b = substl (List.map mkVar rec_vars) b in
+		   let coq_rec_vars = List.map mkVar rec_vars in
+		   let b = substl coq_rec_vars b in
 		   let rec_vars = List.rev rec_vars in
+		   let coq_rec_term = applist (cj, List.rev coq_rec_vars) in
+		   let b = replace_vars [x, coq_rec_term] b in
 		   let bv = bv @ rec_vars in
 		   let rec_vars = List.map string_of_id rec_vars in
-		   let fol_var x =
-		     Fol.App (x, []) in
+		   let fol_var x = Fol.App (x, []) in
 		   let fol_rec_vars = List.map fol_var rec_vars in
 		   let fol_rec_term = App (idc, fol_rec_vars) in
 		   let rec_vars = List.combine rec_vars l in
@@ -641,14 +643,14 @@ let tr_goal gl =
   hyps, c
 
 
-type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon
+type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy
 
 let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ())
 
 let sprintf = Format.sprintf
 
 let call_simplify fwhy =
-  let cmd = sprintf "why --no-arrays --simplify --encoding strat %s" fwhy in
+  let cmd = sprintf "why --no-arrays --simplify --encoding sstrat %s" fwhy in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
   let cmd = 
@@ -755,6 +757,11 @@ let call_harvey fwhy =
   if not !debug then remove_files [fwhy; frv; outf];
   r
 
+let call_gwhy fwhy =
+  let cmd = sprintf "gwhy --no-arrays  %s" fwhy in
+  if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
+  NoAnswer
+
 let ergo_proof_from_file f gl =
   let s =
     let buf = Buffer.create 1024 in
@@ -780,6 +787,7 @@ let call_prover prover q =
     | Zenon -> call_zenon fwhy
     | CVCLite -> call_cvcl fwhy
     | Harvey -> call_harvey fwhy
+    | Gwhy -> call_gwhy fwhy
   
 let dp prover gl =
   let concl_type = pf_type_of gl (pf_concl gl) in
@@ -793,6 +801,7 @@ let dp prover gl =
       | Invalid -> error "Invalid"
       | DontKnow -> error "Don't know"
       | Timeout -> error "Timeout"
+      | NoAnswer -> Tacticals.tclIDTAC gl
     end
   with NotFO ->
     error "Not a first order goal"
@@ -804,6 +813,7 @@ let yices = tclTHEN intros (dp Yices)
 let cvc_lite = tclTHEN intros (dp CVCLite)
 let harvey = dp Harvey
 let zenon = tclTHEN intros (dp Zenon)
+let gwhy = tclTHEN intros (dp Gwhy)
 
 let dp_hint l =
   let env = Global.env () in
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index 1e47c950f..871a0631b 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -8,6 +8,7 @@ val yices : tactic
 val cvc_lite : tactic
 val harvey : tactic
 val zenon : tactic
+val gwhy : tactic
 
 val dp_hint : reference list -> unit
 val set_timeout : int -> unit
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
index 5347a86f2..db1fd430f 100644
--- a/contrib/dp/fol.mli
+++ b/contrib/dp/fol.mli
@@ -45,4 +45,10 @@ type query = decl list * form
 
 (* prover result *)
 
-type prover_answer = Valid of string option | Invalid | DontKnow | Timeout
+type prover_answer = 
+  | Valid of string option 
+  | Invalid
+  | DontKnow
+  | Timeout
+  | NoAnswer
+
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 3e083dbd1..9f5fe5be9 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -36,6 +36,10 @@ TACTIC EXTEND Zenon
   [ "zenon" ] -> [ zenon ]
 END
 
+TACTIC EXTEND Gwhy
+  [ "gwhy" ] -> [ gwhy ]
+END
+
 (* should be part of basic tactics syntax *)
 TACTIC EXTEND admit
   [ "admit"    ] -> [ Tactics.admit_as_an_axiom ]
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index b32c45e74..0284623c4 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -2,15 +2,45 @@
 Require Import ZArith.
 Require Import Classical.
 
-Require Export zenon.
-
 Dp_debug.
 Dp_timeout 3.
 
+
+Inductive expr: Set := Some: expr -> expr -> expr | None: expr. 
+Parameter depth: expr -> expr -> nat. 
+
+Fixpoint length (t: expr) : nat :=
+  match t with
+  | None => 0
+  | Some t1 t2 => depth t t1
+  end.
+
+Goal forall e, length e = 0. 
+intros. 
+gwhy.
+ergo.
+Qed.
+
+
+(* polymorphism *)
+Require Import List.
+
+Inductive mylist (A:Set) : Set :=
+  mynil : mylist A
+| mycons : forall a:A, mylist A -> mylist A.
+
+Parameter nlist: mylist nat -> Prop.
+
+ Goal forall l,  nlist l -> True.
+ intros.
+gwhy.
+ simplify. 
+Qed.
+
 (* First example with the 0 and the equality translated *)
 
 Goal 0 = 0.
-zenon.
+simplify.
 Qed.
 
 (* Examples in the Propositional Calculus
@@ -19,27 +49,26 @@ Qed.
 Parameter A C : Prop.
 
 Goal A -> A.
-zenon.
+simplify.
 Qed.
 
 
 Goal A -> (A \/ C).
 
-zenon.
+simplify.
 Qed.
 
 
 Parameter x y z : Z.
 
 Goal x = y -> y = z -> x = z.
-
-zenon.
+ergo.
 Qed.
 
 
 Goal ((((A -> C) -> A) -> A) -> C) -> C.
 
-zenon.
+ergo.
 Qed.
 
 (* Arithmetic *)