aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/dp
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-11-06 15:25:07 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-11-06 15:25:07 +0000
commit556df3bfae8a80563f9415199fa8651666eb1932 (patch)
tree56e5429be2cd9ea74366ecc56b235862313d392a /contrib/dp
parent0ef55db448fcdefe398f8b586d7a28c4f85abf04 (diff)
bugs dp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10293 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/dp')
-rw-r--r--contrib/dp/dp.ml20
-rw-r--r--contrib/dp/dp.mli1
-rw-r--r--contrib/dp/fol.mli8
-rw-r--r--contrib/dp/g_dp.ml44
-rw-r--r--contrib/dp/tests.v45
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 *)