diff options
| -rw-r--r-- | contrib/dp/dp.ml | 20 | ||||
| -rw-r--r-- | contrib/dp/dp.mli | 1 | ||||
| -rw-r--r-- | contrib/dp/fol.mli | 8 | ||||
| -rw-r--r-- | contrib/dp/g_dp.ml4 | 4 | ||||
| -rw-r--r-- | contrib/dp/tests.v | 45 |
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 *) |