summaryrefslogtreecommitdiff
path: root/contrib/dp
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /contrib/dp
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/dp')
-rw-r--r--contrib/dp/Dp.v120
-rw-r--r--contrib/dp/TODO4
-rw-r--r--contrib/dp/dp.ml316
-rw-r--r--contrib/dp/dp.mli8
-rw-r--r--contrib/dp/dp_cvcl.ml112
-rw-r--r--contrib/dp/dp_cvcl.mli4
-rw-r--r--contrib/dp/dp_gappa.ml445
-rw-r--r--contrib/dp/dp_simplify.ml117
-rw-r--r--contrib/dp/dp_simplify.mli4
-rw-r--r--contrib/dp/dp_sorts.ml51
-rw-r--r--contrib/dp/dp_sorts.mli4
-rw-r--r--contrib/dp/dp_why.ml12
-rw-r--r--contrib/dp/dp_why.mli17
-rw-r--r--contrib/dp/dp_zenon.ml103
-rw-r--r--contrib/dp/dp_zenon.mli5
-rw-r--r--contrib/dp/dp_zenon.mll181
-rw-r--r--contrib/dp/fol.mli9
-rw-r--r--contrib/dp/g_dp.ml443
-rw-r--r--contrib/dp/test2.v8
-rw-r--r--contrib/dp/test_gappa.v91
-rw-r--r--contrib/dp/tests.v116
-rw-r--r--contrib/dp/zenon.v94
22 files changed, 1393 insertions, 471 deletions
diff --git a/contrib/dp/Dp.v b/contrib/dp/Dp.v
new file mode 100644
index 00000000..857c182c
--- /dev/null
+++ b/contrib/dp/Dp.v
@@ -0,0 +1,120 @@
+(* Calls to external decision procedures *)
+
+Require Export ZArith.
+Require Export Classical.
+
+(* Zenon *)
+
+(* Copyright 2004 INRIA *)
+(* $Id: Dp.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+
+Lemma zenon_nottrue :
+ (~True -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_noteq : forall (T : Type) (t : T),
+ ((t <> t) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_and : forall P Q : Prop,
+ (P -> Q -> False) -> (P /\ Q -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_or : forall P Q : Prop,
+ (P -> False) -> (Q -> False) -> (P \/ Q -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_imply : forall P Q : Prop,
+ (~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_equiv : forall P Q : Prop,
+ (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notand : forall P Q : Prop,
+ (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notor : forall P Q : Prop,
+ (~P -> ~Q -> False) -> (~(P \/ Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notimply : forall P Q : Prop,
+ (P -> ~Q -> False) -> (~(P -> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notequiv : forall P Q : Prop,
+ (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
+ (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
+ ((P t) -> False) -> ((forall x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
+ (~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
+ (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
+Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.
+
+Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
+Proof. auto. Qed.
+
+Lemma zenon_equal_step :
+ forall (S T : Type) (fa fb : S -> T) (a b : S),
+ (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
+Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.
+
+Lemma zenon_pnotp : forall P Q : Prop,
+ (P = Q) -> (P -> ~Q -> False).
+Proof. intros P Q Ha. rewrite Ha. auto. Qed.
+
+Lemma zenon_notequal : forall (T : Type) (a b : T),
+ (a = b) -> (a <> b -> False).
+Proof. auto. Qed.
+
+Ltac zenon_intro id :=
+ intro id || let nid := fresh in (intro nid; clear nid)
+.
+
+Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
+Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
+Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
+Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
+Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
+Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
+Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
+Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
+Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
+Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.
+
+Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
+Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.
+
+(* Ergo *)
+
+Set Implicit Arguments.
+Section congr.
+ Variable t:Type.
+Lemma ergo_eq_concat_1 :
+ forall (P:t -> Prop) (x y:t),
+ P x -> x = y -> P y.
+Proof.
+ intros; subst; auto.
+Qed.
+
+Lemma ergo_eq_concat_2 :
+ forall (P:t -> t -> Prop) (x1 x2 y1 y2:t),
+ P x1 x2 -> x1 = y1 -> x2 = y2 -> P y1 y2.
+Proof.
+ intros; subst; auto.
+Qed.
+
+End congr.
diff --git a/contrib/dp/TODO b/contrib/dp/TODO
index 387cacdf..44349e21 100644
--- a/contrib/dp/TODO
+++ b/contrib/dp/TODO
@@ -21,8 +21,4 @@ TODO
BUGS
----
-- value = Some : forall A:Set, A -> option A
-
- -> eta_expanse échoue sur assert false (ligne 147)
-
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 131dd029..79ffaf3f 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -13,6 +13,8 @@
open Util
open Pp
+open Libobject
+open Summary
open Term
open Tacmach
open Tactics
@@ -25,12 +27,46 @@ open Coqlib
open Hipattern
open Libnames
open Declarations
+open Dp_why
let debug = ref false
+let set_debug b = debug := b
+let trace = ref false
+let set_trace b = trace := b
+let timeout = ref 10
+let set_timeout n = timeout := n
+
+let (dp_timeout_obj,_) =
+ declare_object
+ {(default_object "Dp_timeout") with
+ cache_function = (fun (_,x) -> set_timeout x);
+ load_function = (fun _ (_,x) -> set_timeout x);
+ export_function = (fun x -> Some x)}
+
+let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
+
+let (dp_debug_obj,_) =
+ declare_object
+ {(default_object "Dp_debug") with
+ cache_function = (fun (_,x) -> set_debug x);
+ load_function = (fun _ (_,x) -> set_debug x);
+ export_function = (fun x -> Some x)}
+
+let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
+
+let (dp_trace_obj,_) =
+ declare_object
+ {(default_object "Dp_trace") with
+ cache_function = (fun (_,x) -> set_trace x);
+ load_function = (fun _ (_,x) -> set_trace x);
+ export_function = (fun x -> Some x)}
+
+let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x)
let logic_dir = ["Coq";"Logic";"Decidable"]
let coq_modules =
init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
+ @ [["Coq"; "ZArith"; "BinInt"]]
@ [["Coq"; "omega"; "OmegaLemmas"]]
let constant = gen_constant_in_modules "dp" coq_modules
@@ -52,6 +88,7 @@ let coq_Zneg = lazy (constant "Zneg")
let coq_xH = lazy (constant "xH")
let coq_xI = lazy (constant "xI")
let coq_xO = lazy (constant "xO")
+let coq_iff = lazy (constant "iff")
(* not Prop typed expressions *)
exception NotProp
@@ -104,7 +141,7 @@ let coq_rename_vars env vars =
type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
let decomp_type_quantifiers env t =
let rec loop vars t = match kind_of_term t with
- | Prod (n, a, t) when is_Set a ->
+ | Prod (n, a, t) when is_Set a || is_Type a ->
loop ((n,a) :: vars) t
| _ ->
let vars, env = coq_rename_vars env vars in
@@ -116,7 +153,7 @@ let decomp_type_quantifiers env t =
(* same thing with lambda binders (for axiomatize body) *)
let decomp_type_lambdas env t =
let rec loop vars t = match kind_of_term t with
- | Lambda (n, a, t) when is_Set a ->
+ | Lambda (n, a, t) when is_Set a || is_Type a ->
loop ((n,a) :: vars) t
| _ ->
let vars, env = coq_rename_vars env vars in
@@ -314,7 +351,7 @@ and make_term_abstraction tv env c =
*)
and tr_decl env id ty =
let tv, env, t = decomp_type_quantifiers env ty in
- if is_Set t then
+ if is_Set t || is_Type t then
DeclType (id, List.length tv)
else if is_Prop t then
DeclPred (id, List.length tv, [])
@@ -329,8 +366,8 @@ and tr_decl env id ty =
DeclPred(id, List.length tv, l)
else
let s = Typing.type_of env Evd.empty t in
- if is_Set s then
- DeclFun(id, List.length tv, l, tr_type tv env t)
+ if is_Set s || is_Type s then
+ DeclFun (id, List.length tv, l, tr_type tv env t)
else
raise NotFO
@@ -364,17 +401,18 @@ and axiomatize_body env r id d = match r with
begin match (Global.lookup_constant c).const_body with
| Some b ->
let b = force b in
- let tv, env, b = decomp_type_lambdas env b in
let axioms =
(match d with
| DeclPred (id, _, []) ->
+ let tv, env, b = decomp_type_lambdas env b in
let value = tr_formula tv [] env b in
[id, Iff (Fatom (Pred (id, [])), value)]
| DeclFun (id, _, [], _) ->
+ let tv, env, b = decomp_type_lambdas env b in
let value = tr_term tv [] env b in
[id, Fatom (Eq (Fol.App (id, []), value))]
| DeclFun (id, _, l, _) | DeclPred (id, _, l) ->
- Format.eprintf "axiomatize_body %S@." id;
+ (*Format.eprintf "axiomatize_body %S@." id;*)
let b = match kind_of_term b with
(* a single recursive function *)
| Fix (_, (_,_,[|b|])) ->
@@ -391,6 +429,7 @@ and axiomatize_body env r id d = match r with
| _ ->
b
in
+ let tv, env, b = decomp_type_lambdas env b in
let vars, t = decompose_lam b in
let n = List.length l in
let k = List.length vars in
@@ -401,21 +440,21 @@ and axiomatize_body env r id d = match r with
let vars = List.rev vars in
let bv = vars in
let vars = List.map (fun x -> string_of_id x) vars in
- let fol_var x =
- Fol.App (x, []) in
+ let fol_var x = Fol.App (x, []) in
let fol_vars = List.map fol_var vars in
let vars = List.combine vars l in
begin match d with
- | DeclFun _ ->
+ | DeclFun (_, _, _, ty) ->
begin match kind_of_term t with
| Case (ci, _, e, br) ->
equations_for_case env id vars tv bv ci e br
| _ ->
- let p =
- Fatom (Eq (App (id, fol_vars),
- tr_term tv bv env t))
+ let t = tr_term tv bv env t in
+ let ax =
+ add_proof (Fun_def (id, vars, ty, t))
in
- [id, foralls vars p]
+ let p = Fatom (Eq (App (id, fol_vars), t)) in
+ [ax, foralls vars p]
end
| DeclPred _ ->
let value = tr_formula tv bv env t in
@@ -436,7 +475,7 @@ and axiomatize_body env r id d = match r with
| IndRef i ->
iter_all_constructors i
(fun _ c ->
- let rc = reference_of_constr c in
+ let rc = global_of_constr c in
try
begin match tr_global env rc with
| DeclFun (_, _, [], _) -> ()
@@ -453,18 +492,20 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
iter_all_constructors ci.ci_ind
(fun j cj ->
try
- let cjr = reference_of_constr cj in
+ let cjr = global_of_constr cj in
begin match tr_global env cjr with
| DeclFun (idc, _, l, _) ->
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
@@ -558,7 +599,7 @@ and tr_formula tv bv env f =
Fatom (Pred (rename_global (VarRef id), []))
| _, [t;a;b] when c = build_coq_eq () ->
let ty = Typing.type_of env Evd.empty t in
- if is_Set ty then
+ if is_Set ty || is_Type ty then
let _ = tr_type tv env t in
Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b))
else
@@ -581,6 +622,8 @@ and tr_formula tv bv env f =
And (tr_formula tv bv env a, tr_formula tv bv env b)
| _, [a;b] when c = build_coq_or () ->
Or (tr_formula tv bv env a, tr_formula tv bv env b)
+ | _, [a;b] when c = Lazy.force coq_iff ->
+ Iff (tr_formula tv bv env a, tr_formula tv bv env b)
| Prod (n, a, b), _ ->
if is_imp_term f then
Imp (tr_formula tv bv env a, tr_formula tv bv env b)
@@ -632,55 +675,164 @@ let tr_goal gl =
hyps, c
-type prover = Simplify | 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 file_contents f =
+ let buf = Buffer.create 1024 in
+ try
+ let c = open_in f in
+ begin try
+ while true do
+ let s = input_line c in Buffer.add_string buf s;
+ Buffer.add_char buf '\n'
+ done;
+ assert false
+ with End_of_file ->
+ close_in c;
+ Buffer.contents buf
+ end
+ with _ ->
+ sprintf "(cannot open %s)" f
+
+let timeout_sys_command cmd =
+ if !debug then Format.eprintf "command line: %s@." cmd;
+ let out = Filename.temp_file "out" "" in
+ let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in
+ let ret = Sys.command cmd in
+ if !debug then
+ Format.eprintf "Output file %s:@.%s@." out (file_contents out);
+ ret, out
+
+let timeout_or_failure c cmd out =
+ if c = 152 then
+ Timeout
+ else
+ Failure
+ (sprintf "command %s failed with output:\n%s " cmd (file_contents out))
+
+let prelude_files = ref ([] : string list)
+
+let set_prelude l = prelude_files := l
+
+let (dp_prelude_obj,_) =
+ declare_object
+ {(default_object "Dp_prelude") with
+ cache_function = (fun (_,x) -> set_prelude x);
+ load_function = (fun _ (_,x) -> set_prelude x);
+ export_function = (fun x -> Some x)}
+
+let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x)
+
+let why_files f = String.concat " " (!prelude_files @ [f])
+
let call_simplify fwhy =
- let cmd = sprintf "why --simplify %s" fwhy in
- if Sys.command cmd <> 0 then error ("Call to " ^ cmd ^ " failed");
+ let cmd =
+ sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files 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 =
- sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" fsx
+ sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out"
+ !timeout fsx
in
let out = Sys.command cmd in
- let r = if out = 0 then Valid else if out = 1 then Invalid else Timeout 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; fsx];
r
+let call_ergo fwhy =
+ let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in
+ if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+ let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
+ let ftrace = Filename.temp_file "ergo_trace" "" in
+ let cmd =
+ if !trace then
+ sprintf "ergo -cctrace %s %s" ftrace fwhy
+ else
+ sprintf "ergo %s" fwhy
+ in
+ let ret,out = timeout_sys_command cmd in
+ let r =
+ if ret <> 0 then
+ timeout_or_failure ret cmd out
+ else if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then
+ Valid (if !trace then Some ftrace else None)
+ else if Sys.command (sprintf "grep -q -w \"I don't know\" %s" out) = 0 then
+ DontKnow
+ else if Sys.command (sprintf "grep -q -w \"Invalid\" %s" out) = 0 then
+ Invalid
+ else
+ Failure ("command failed: " ^ cmd)
+ in
+ if not !debug then remove_files [fwhy; out];
+ r
+
let call_zenon fwhy =
- let cmd = sprintf "why --no-prelude --no-zenon-prelude --zenon %s" fwhy in
+ let cmd =
+ sprintf "why --no-prelude --no-zenon-prelude --zenon %s" (why_files fwhy)
+ in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in
+ let out = Filename.temp_file "dp_out" "" in
let cmd =
- sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" fznn
+ sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out
+ in
+ let c = Sys.command cmd in
+ if not !debug then remove_files [fwhy; fznn];
+ if c = 137 then
+ Timeout
+ else begin
+ if c <> 0 then anomaly ("command failed: " ^ cmd);
+ if Sys.command (sprintf "grep -q -w Error %s" out) = 0 then
+ error "Zenon failed";
+ let c = Sys.command (sprintf "grep -q PROOF-FOUND %s" out) in
+ if c = 0 then Valid (Some out) else Invalid
+ end
+
+let call_yices fwhy =
+ let cmd =
+ sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy)
+ in
+ if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+ let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
+ let cmd =
+ sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out"
+ !timeout fsmt
in
let out = Sys.command cmd in
let r =
- if out = 0 then Valid
- else if out = 1 then Invalid
- else if out = 137 then Timeout
- else anomaly ("malformed Zenon input file " ^ fznn)
+ if out = 0 then Valid None else if out = 1 then Invalid else Timeout
in
- if not !debug then remove_files [fwhy; fznn];
+ if not !debug then remove_files [fwhy; fsmt];
r
let call_cvcl fwhy =
- let cmd = sprintf "why --cvcl %s" fwhy in
+ let cmd =
+ sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy)
+ in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
let cmd =
- sprintf "timeout 10 cvcl < %s > out 2>&1 && grep -q -w Valid out" fcvc
+ sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out"
+ !timeout fcvc
in
let out = Sys.command cmd in
- let r = if out = 0 then Valid else if out = 1 then Invalid else Timeout 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; fcvc];
r
let call_harvey fwhy =
- let cmd = sprintf "why --harvey %s" fwhy in
+ let cmd =
+ sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy)
+ in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
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
@@ -688,7 +840,8 @@ let call_harvey fwhy =
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)
+ Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1"
+ !timeout f outf)
in
let r =
if out <> 0 then
@@ -697,40 +850,69 @@ let call_harvey fwhy =
let cmd =
sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf
in
- if Sys.command cmd = 0 then Valid else Invalid
+ if Sys.command cmd = 0 then Valid None else Invalid
in
if not !debug then remove_files [fwhy; frv; outf];
r
+let call_gwhy fwhy =
+ let cmd = sprintf "gwhy --no-arrays %s" (why_files 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
+ let c = open_in f in
+ try
+ while true do Buffer.add_string buf (input_line c) done; assert false
+ with End_of_file ->
+ close_in c;
+ Buffer.contents buf
+ in
+ let parsed_constr = Pcoq.parse_string Pcoq.Constr.constr s in
+ let t = Constrintern.interp_constr (project gl) (pf_env gl) parsed_constr in
+ exact_check t gl
+
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));
match prover with
| Simplify -> call_simplify fwhy
+ | Ergo -> call_ergo fwhy
+ | Yices -> call_yices fwhy
| Zenon -> call_zenon fwhy
| CVCLite -> call_cvcl fwhy
| Harvey -> call_harvey fwhy
+ | Gwhy -> call_gwhy fwhy
let dp prover gl =
+ Coqlib.check_required_library ["Coq";"ZArith";"ZArith"];
let concl_type = pf_type_of gl (pf_concl gl) in
if not (is_Prop concl_type) then error "Conclusion is not a Prop";
try
let q = tr_goal gl in
begin match call_prover prover q with
- | Valid -> Tactics.admit_as_an_axiom gl
+ | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
+ | Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl
+ | Valid _ -> Tactics.admit_as_an_axiom gl
| Invalid -> error "Invalid"
| DontKnow -> error "Don't know"
| Timeout -> error "Timeout"
+ | Failure s -> error s
+ | NoAnswer -> Tacticals.tclIDTAC gl
end
with NotFO ->
error "Not a first order goal"
-
+
let simplify = tclTHEN intros (dp Simplify)
+let ergo = tclTHEN intros (dp Ergo)
+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
@@ -741,7 +923,8 @@ let dp_hint l =
if is_Prop s then
try
let id = rename_global r in
- let d = Axiom (id, tr_formula [] [] env ty) in
+ let tv, env, ty = decomp_type_quantifiers env ty in
+ let d = Axiom (id, tr_formula tv [] env ty) in
add_global r (Gfo d);
globals_stack := d :: !globals_stack
with NotFO ->
@@ -757,3 +940,52 @@ let dp_hint l =
end
in
List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
+
+let (dp_hint_obj,_) =
+ declare_object
+ {(default_object "Dp_hint") with
+ cache_function = (fun (_,l) -> dp_hint l);
+ load_function = (fun _ (_,l) -> dp_hint l);
+ export_function = (fun x -> Some x)}
+
+let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l)
+
+let dp_predefined qid s =
+ let r = Nametab.global qid in
+ let ty = Global.type_of_global r in
+ let env = Global.env () in
+ let id = rename_global r in
+ try
+ let d = match tr_decl env id ty with
+ | DeclType (_, n) -> DeclType (s, n)
+ | DeclFun (_, n, tyl, ty) -> DeclFun (s, n, tyl, ty)
+ | DeclPred (_, n, tyl) -> DeclPred (s, n, tyl)
+ | Axiom _ as d -> d
+ in
+ match d with
+ | Axiom _ -> msg_warning (str " ignored (axiom)")
+ | d -> add_global r (Gfo d)
+ with NotFO ->
+ msg_warning (str " ignored (not a first order declaration)")
+
+let (dp_predefined_obj,_) =
+ declare_object
+ {(default_object "Dp_predefined") with
+ cache_function = (fun (_,(id,s)) -> dp_predefined id s);
+ load_function = (fun _ (_,(id,s)) -> dp_predefined id s);
+ export_function = (fun x -> Some x)}
+
+let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s))
+
+let _ = declare_summary "Dp options"
+ { freeze_function =
+ (fun () -> !debug, !trace, !timeout, !prelude_files);
+ unfreeze_function =
+ (fun (d,tr,tm,pr) ->
+ debug := d; trace := tr; timeout := tm; prelude_files := pr);
+ init_function =
+ (fun () ->
+ debug := false; trace := false; timeout := 10;
+ prelude_files := []);
+ survive_module = true;
+ survive_section = true }
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index 3dad469c..6dbc05e1 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -3,10 +3,18 @@ open Libnames
open Proof_type
val simplify : tactic
+val ergo : tactic
+val yices : tactic
val cvc_lite : tactic
val harvey : tactic
val zenon : tactic
+val gwhy : tactic
val dp_hint : reference list -> unit
+val dp_timeout : int -> unit
+val dp_debug : bool -> unit
+val dp_trace : bool -> unit
+val dp_prelude : string list -> unit
+val dp_predefined : reference -> string -> unit
diff --git a/contrib/dp/dp_cvcl.ml b/contrib/dp/dp_cvcl.ml
deleted file mode 100644
index 05d43081..00000000
--- a/contrib/dp/dp_cvcl.ml
+++ /dev/null
@@ -1,112 +0,0 @@
-
-open Format
-open Fol
-
-let rec print_list sep print fmt = function
- | [] -> ()
- | [x] -> print fmt x
- | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-
-let space fmt () = fprintf fmt "@ "
-let comma fmt () = fprintf fmt ",@ "
-
-let rec print_term fmt = function
- | Cst n ->
- fprintf fmt "%d" n
- | Plus (a, b) ->
- fprintf fmt "@[(%a@ +@ %a)@]" print_term a print_term b
- | Moins (a, b) ->
- fprintf fmt "@[(%a@ -@ %a)@]" print_term a print_term b
- | Mult (a, b) ->
- fprintf fmt "@[(%a@ *@ %a)@]" print_term a print_term b
- | Div (a, b) ->
- fprintf fmt "@[(%a@ /@ %a)@]" print_term a print_term b
- | App (id, []) ->
- fprintf fmt "@[%s@]" id
- | App (id, tl) ->
- fprintf fmt "@[%s(%a)@]" id print_terms tl
-
-and print_terms fmt tl =
- print_list comma print_term fmt tl
-
-let rec print_predicate fmt p =
- let pp = print_predicate in
- match p with
- | True ->
- fprintf fmt "TRUE"
- | False ->
- fprintf fmt "FALSE"
- | Fatom (Eq (a, b)) ->
- fprintf fmt "@[(%a = %a)@]" print_term a print_term b
- | Fatom (Le (a, b)) ->
- fprintf fmt "@[(%a@ <= %a)@]" print_term a print_term b
- | Fatom (Lt (a, b))->
- fprintf fmt "@[(%a@ < %a)@]" print_term a print_term b
- | Fatom (Ge (a, b)) ->
- fprintf fmt "@[(%a@ >= %a)@]" print_term a print_term b
- | Fatom (Gt (a, b)) ->
- fprintf fmt "@[(%a@ > %a)@]" print_term a print_term b
- | Fatom (Pred (id, [])) ->
- fprintf fmt "@[%s@]" id
- | Fatom (Pred (id, tl)) ->
- fprintf fmt "@[%s(%a)@]" id print_terms tl
- | Imp (a, b) ->
- fprintf fmt "@[(%a@ => %a)@]" pp a pp b
- | And (a, b) ->
- fprintf fmt "@[(%a@ AND@ %a)@]" pp a pp b
- | Or (a, b) ->
- fprintf fmt "@[(%a@ OR@ %a)@]" pp a pp b
- | Not a ->
- fprintf fmt "@[(NOT@ %a)@]" pp a
- | Forall (id, t, p) ->
- fprintf fmt "@[(FORALL (%s:%s): %a)@]" id t pp p
- | Exists (id, t, p) ->
- fprintf fmt "@[(EXISTS (%s:%s): %a)@]" id t pp p
-
-let rec string_of_type_list = function
- | [] -> assert false
- | [e] -> e
- | e :: l' -> e ^ ", " ^ (string_of_type_list l')
-
-let print_query fmt (decls,concl) =
- let print_decl = function
- | DeclVar (id, [], t) ->
- fprintf fmt "@[%s: %s;@]@\n" id t
- | DeclVar (id, [e], t) ->
- fprintf fmt "@[%s: [%s -> %s];@]@\n"
- id e t
- | DeclVar (id, l, t) ->
- fprintf fmt "@[%s: [[%s] -> %s];@]@\n"
- id (string_of_type_list l) t
- | DeclPred (id, []) ->
- fprintf fmt "@[%s: BOOLEAN;@]@\n" id
- | DeclPred (id, [e]) ->
- fprintf fmt "@[%s: [%s -> BOOLEAN];@]@\n"
- id e
- | DeclPred (id, l) ->
- fprintf fmt "@[%s: [[%s] -> BOOLEAN];@]@\n"
- id (string_of_type_list l)
- | DeclType id ->
- fprintf fmt "@[%s: TYPE;@]@\n" id
- | Assert (id, f) ->
- fprintf fmt "@[ASSERT %% %s@\n %a;@]@\n" id print_predicate f
- in
- List.iter print_decl decls;
- fprintf fmt "QUERY %a;" print_predicate concl
-
-let call q =
- let f = Filename.temp_file "coq_dp" ".cvc" in
- let c = open_out f in
- let fmt = formatter_of_out_channel c in
- fprintf fmt "@[%a@]@." print_query q;
- close_out c;
- ignore (Sys.command (sprintf "cat %s" f));
- let cmd =
- sprintf "timeout 10 cvcl < %s > out 2>&1 && grep -q -w Valid out" f
- in
- prerr_endline cmd; flush stderr;
- let out = Sys.command cmd in
- if out = 0 then Valid else if out = 1 then Invalid else Timeout
- (* TODO: effacer le fichier f et le fichier out *)
-
-
diff --git a/contrib/dp/dp_cvcl.mli b/contrib/dp/dp_cvcl.mli
deleted file mode 100644
index 03b6d347..00000000
--- a/contrib/dp/dp_cvcl.mli
+++ /dev/null
@@ -1,4 +0,0 @@
-
-open Fol
-
-val call : query -> prover_answer
diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml
new file mode 100644
index 00000000..70439a97
--- /dev/null
+++ b/contrib/dp/dp_gappa.ml
@@ -0,0 +1,445 @@
+
+open Format
+open Util
+open Pp
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Names
+open Nameops
+open Termops
+open Coqlib
+open Hipattern
+open Libnames
+open Declarations
+open Evarutil
+
+let debug = ref false
+
+(* 1. gappa syntax trees and output *)
+
+module Constant = struct
+
+ open Bigint
+
+ type t = { mantissa : bigint; base : int; exp : bigint }
+
+ let create (b, m, e) =
+ { mantissa = m; base = b; exp = e }
+
+ let of_int x =
+ { mantissa = x; base = 1; exp = zero }
+
+ let print fmt x = match x.base with
+ | 1 -> fprintf fmt "%s" (to_string x.mantissa)
+ | 2 -> fprintf fmt "%sb%s" (to_string x.mantissa) (to_string x.exp)
+ | 10 -> fprintf fmt "%se%s" (to_string x.mantissa) (to_string x.exp)
+ | _ -> assert false
+
+end
+
+type binop = Bminus | Bplus | Bmult | Bdiv
+
+type unop = Usqrt | Uabs | Uopp
+
+type rounding_mode = string
+
+type term =
+ | Tconst of Constant.t
+ | Tvar of string
+ | Tbinop of binop * term * term
+ | Tunop of unop * term
+ | Tround of rounding_mode * term
+
+type pred =
+ | Pin of term * Constant.t * Constant.t
+
+let rec print_term fmt = function
+ | Tconst c -> Constant.print fmt c
+ | Tvar s -> pp_print_string fmt s
+ | Tbinop (op, t1, t2) ->
+ let op = match op with
+ | Bplus -> "+" | Bminus -> "-" | Bmult -> "*" | Bdiv -> "/"
+ in
+ fprintf fmt "(%a %s %a)" print_term t1 op print_term t2
+ | Tunop (Uabs, t) ->
+ fprintf fmt "|%a|" print_term t
+ | Tunop (Uopp | Usqrt as op, t) ->
+ let s = match op with
+ | Uopp -> "-" | Usqrt -> "sqrt" | _ -> assert false
+ in
+ fprintf fmt "(%s(%a))" s print_term t
+ | Tround (m, t) ->
+ fprintf fmt "(%s(%a))" m print_term t
+
+let print_pred fmt = function
+ | Pin (t, c1, c2) ->
+ fprintf fmt "%a in [%a, %a]"
+ print_term t Constant.print c1 Constant.print c2
+
+let temp_file f = if !debug then f else Filename.temp_file f ".v"
+let remove_file f = if not !debug then try Sys.remove f with _ -> ()
+
+let read_gappa_proof f =
+ let buf = Buffer.create 1024 in
+ Buffer.add_char buf '(';
+ let cin = open_in f in
+ let rec skip_space () =
+ let c = input_char cin in if c = ' ' then skip_space () else c
+ in
+ while input_char cin <> '=' do () done;
+ try
+ while true do
+ let c = skip_space () in
+ if c = ':' then raise Exit;
+ Buffer.add_char buf c;
+ let s = input_line cin in
+ Buffer.add_string buf s;
+ Buffer.add_char buf '\n';
+ done;
+ assert false
+ with Exit ->
+ close_in cin;
+ remove_file f;
+ Buffer.add_char buf ')';
+ Buffer.contents buf
+
+exception GappaFailed
+exception GappaProofFailed
+
+let patch_gappa_proof fin fout =
+ let cin = open_in fin in
+ let cout = open_out fout in
+ let fmt = formatter_of_out_channel cout in
+ let last = ref "" in
+ let defs = ref "" in
+ try
+ while true do
+ let s = input_line cin in
+ if s = "Qed." then
+ fprintf fmt "Defined.@\n"
+ else begin
+ begin
+ try Scanf.sscanf s "Lemma %s "
+ (fun n -> defs := n ^ " " ^ !defs; last := n)
+ with Scanf.Scan_failure _ ->
+ try Scanf.sscanf s "Definition %s "
+ (fun n -> defs := n ^ " " ^ !defs)
+ with Scanf.Scan_failure _ ->
+ ()
+ end;
+ fprintf fmt "%s@\n" s
+ end
+ done
+ with End_of_file ->
+ close_in cin;
+ fprintf fmt "Definition proof := Eval cbv delta [%s] in %s.@." !defs !last;
+ close_out cout
+
+let call_gappa hl p =
+ let gappa_in = temp_file "gappa_input" in
+ let c = open_out gappa_in in
+ let fmt = formatter_of_out_channel c in
+ fprintf fmt "@[{ ";
+ List.iter (fun h -> fprintf fmt "%a ->@ " print_pred h) hl;
+ fprintf fmt "%a }@]@." print_pred p;
+ close_out c;
+ let gappa_out = temp_file "gappa_output" in
+ let cmd = sprintf "gappa -Bcoq < %s > %s 2> /dev/null" gappa_in gappa_out in
+ let out = Sys.command cmd in
+ if out <> 0 then raise GappaFailed;
+ remove_file gappa_in;
+ let gappa_out2 = temp_file "gappa2" in
+ patch_gappa_proof gappa_out gappa_out2;
+ remove_file gappa_out;
+ let cmd = sprintf "%s/coqc %s" Coq_config.bindir gappa_out2 in
+ let out = Sys.command cmd in
+ if out <> 0 then raise GappaProofFailed;
+ let gappa_out3 = temp_file "gappa3" in
+ let c = open_out gappa_out3 in
+ let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in
+ Printf.fprintf c
+ "Require \"%s\". Set Printing Depth 9999999. Print %s.proof."
+ (Filename.chop_suffix gappa_out2 ".v") gappa2;
+ close_out c;
+ let lambda = temp_file "gappa_lambda" in
+ let cmd = sprintf "%s/coqc %s > %s" Coq_config.bindir gappa_out3 lambda in
+ let out = Sys.command cmd in
+ if out <> 0 then raise GappaProofFailed;
+ remove_file gappa_out2; remove_file gappa_out3;
+ remove_file (gappa_out2 ^ "o"); remove_file (gappa_out3 ^ "o");
+ read_gappa_proof lambda
+
+(* 2. coq -> gappa translation *)
+
+exception NotGappa
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+let coq_modules =
+ init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
+ @ [["Coq"; "ZArith"; "BinInt"];
+ ["Coq"; "Reals"; "Rdefinitions"];
+ ["Coq"; "Reals"; "Raxioms";];
+ ["Coq"; "Reals"; "Rbasic_fun";];
+ ["Coq"; "Reals"; "R_sqrt";];
+ ["Coq"; "Reals"; "Rfunctions";];
+ ["Gappa"; "Gappa_tactic";];
+ ["Gappa"; "Gappa_fixed";];
+ ["Gappa"; "Gappa_float";];
+ ["Gappa"; "Gappa_round_def";];
+ ["Gappa"; "Gappa_pred_bnd";];
+ ["Gappa"; "Gappa_definitions";];
+ ]
+
+let constant = gen_constant_in_modules "gappa" coq_modules
+
+let coq_refl_equal = lazy (constant "refl_equal")
+let coq_Rle = lazy (constant "Rle")
+let coq_R = lazy (constant "R")
+(*
+let coq_Rplus = lazy (constant "Rplus")
+let coq_Rminus = lazy (constant "Rminus")
+let coq_Rmult = lazy (constant "Rmult")
+let coq_Rdiv = lazy (constant "Rdiv")
+let coq_powerRZ = lazy (constant "powerRZ")
+let coq_R1 = lazy (constant "R1")
+let coq_Ropp = lazy (constant "Ropp")
+let coq_Rabs = lazy (constant "Rabs")
+let coq_sqrt = lazy (constant "sqrt")
+*)
+
+let coq_convert = lazy (constant "convert")
+let coq_reUnknown = lazy (constant "reUnknown")
+let coq_reFloat2 = lazy (constant "reFloat2")
+let coq_reFloat10 = lazy (constant "reFloat10")
+let coq_reInteger = lazy (constant "reInteger")
+let coq_reBinary = lazy (constant "reBinary")
+let coq_reUnary = lazy (constant "reUnary")
+let coq_reRound = lazy (constant "reRound")
+let coq_roundDN = lazy (constant "roundDN")
+let coq_roundUP = lazy (constant "roundUP")
+let coq_roundNE = lazy (constant "roundNE")
+let coq_roundZR = lazy (constant "roundZR")
+let coq_rounding_fixed = lazy (constant "rounding_fixed")
+let coq_rounding_float = lazy (constant "rounding_float")
+let coq_boAdd = lazy (constant "boAdd")
+let coq_boSub = lazy (constant "boSub")
+let coq_boMul = lazy (constant "boMul")
+let coq_boDiv = lazy (constant "boDiv")
+let coq_uoAbs = lazy (constant "uoAbs")
+let coq_uoNeg = lazy (constant "uoNeg")
+let coq_uoSqrt = lazy (constant "uoSqrt")
+let coq_subset = lazy (constant "subset")
+let coq_makepairF = lazy (constant "makepairF")
+
+let coq_true = lazy (constant "true")
+let coq_false = lazy (constant "false")
+
+let coq_Z0 = lazy (constant "Z0")
+let coq_Zpos = lazy (constant "Zpos")
+let coq_Zneg = lazy (constant "Zneg")
+let coq_xH = lazy (constant "xH")
+let coq_xI = lazy (constant "xI")
+let coq_xO = lazy (constant "xO")
+let coq_IZR = lazy (constant "IZR")
+
+(* translates a closed Coq term p:positive into a FOL term of type int *)
+let rec tr_positive p = match kind_of_term p with
+ | Term.Construct _ when p = Lazy.force coq_xH ->
+ 1
+ | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
+ 2 * (tr_positive a) + 1
+ | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
+ 2 * (tr_positive a)
+ | Term.Cast (p, _, _) ->
+ tr_positive p
+ | _ ->
+ raise NotGappa
+
+(* translates a closed Coq term t:Z into a term of type int *)
+let rec tr_arith_constant t = match kind_of_term t with
+ | Term.Construct _ when t = Lazy.force coq_Z0 -> 0
+ | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_positive a
+ | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - (tr_positive a)
+ | Term.Cast (t, _, _) -> tr_arith_constant t
+ | _ -> raise NotGappa
+
+(* translates a closed Coq term p:positive into a FOL term of type bigint *)
+let rec tr_bigpositive p = match kind_of_term p with
+ | Term.Construct _ when p = Lazy.force coq_xH ->
+ Bigint.one
+ | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
+ Bigint.add_1 (Bigint.mult_2 (tr_bigpositive a))
+ | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
+ (Bigint.mult_2 (tr_bigpositive a))
+ | Term.Cast (p, _, _) ->
+ tr_bigpositive p
+ | _ ->
+ raise NotGappa
+
+(* translates a closed Coq term t:Z into a term of type bigint *)
+let rec tr_arith_bigconstant t = match kind_of_term t with
+ | Term.Construct _ when t = Lazy.force coq_Z0 -> Bigint.zero
+ | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_bigpositive a
+ | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
+ Bigint.neg (tr_bigpositive a)
+ | Term.Cast (t, _, _) -> tr_arith_bigconstant t
+ | _ -> raise NotGappa
+
+let decomp c =
+ let c, args = decompose_app c in
+ kind_of_term c, args
+
+let tr_bool c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_true -> true
+ | c, [] when c = Lazy.force coq_false -> false
+ | _ -> raise NotGappa
+
+let tr_float b m e =
+ (b, tr_arith_bigconstant m, tr_arith_bigconstant e)
+
+let tr_binop c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_boAdd -> Bplus
+ | c, [] when c = Lazy.force coq_boSub -> Bminus
+ | c, [] when c = Lazy.force coq_boMul -> Bmult
+ | c, [] when c = Lazy.force coq_boDiv -> Bdiv
+ | _ -> assert false
+
+let tr_unop c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_uoNeg -> Uopp
+ | c, [] when c = Lazy.force coq_uoSqrt -> Usqrt
+ | c, [] when c = Lazy.force coq_uoAbs -> Uabs
+ | _ -> raise NotGappa
+
+let tr_var c = match decomp c with
+ | Var x, [] -> string_of_id x
+ | _ -> assert false
+
+let tr_mode c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_roundDN -> "dn"
+ | c, [] when c = Lazy.force coq_roundNE -> "ne"
+ | c, [] when c = Lazy.force coq_roundUP -> "up"
+ | c, [] when c = Lazy.force coq_roundZR -> "zr"
+ | _ -> raise NotGappa
+
+let tr_rounding_mode c = match decompose_app c with
+ | c, [a;b] when c = Lazy.force coq_rounding_fixed ->
+ let a = tr_mode a in
+ let b = tr_arith_constant b in
+ sprintf "fixed<%d,%s>" b a
+ | c, [a;p;e] when c = Lazy.force coq_rounding_float ->
+ let a = tr_mode a in
+ let p = tr_positive p in
+ let e = tr_arith_constant e in
+ sprintf "float<%d,%d,%s>" p (-e) a
+ | _ ->
+ raise NotGappa
+
+(* REexpr -> term *)
+let rec tr_term c0 =
+ let c, args = decompose_app c0 in
+ match kind_of_term c, args with
+ | _, [a] when c = Lazy.force coq_reUnknown ->
+ Tvar (tr_var a)
+ | _, [a; b] when c = Lazy.force coq_reFloat2 ->
+ Tconst (Constant.create (tr_float 2 a b))
+ | _, [a; b] when c = Lazy.force coq_reFloat10 ->
+ Tconst (Constant.create (tr_float 10 a b))
+ | _, [a] when c = Lazy.force coq_reInteger ->
+ Tconst (Constant.create (1, tr_arith_bigconstant a, Bigint.zero))
+ | _, [op;a;b] when c = Lazy.force coq_reBinary ->
+ Tbinop (tr_binop op, tr_term a, tr_term b)
+ | _, [op;a] when c = Lazy.force coq_reUnary ->
+ Tunop (tr_unop op, tr_term a)
+ | _, [op;a] when c = Lazy.force coq_reRound ->
+ Tround (tr_rounding_mode op, tr_term a)
+ | _ ->
+ msgnl (str "tr_term: " ++ Printer.pr_constr c0);
+ assert false
+
+let tr_rle c =
+ let c, args = decompose_app c in
+ match kind_of_term c, args with
+ | _, [a;b] when c = Lazy.force coq_Rle ->
+ begin match decompose_app a, decompose_app b with
+ | (ac, [at]), (bc, [bt])
+ when ac = Lazy.force coq_convert && bc = Lazy.force coq_convert ->
+ at, bt
+ | _ ->
+ raise NotGappa
+ end
+ | _ ->
+ raise NotGappa
+
+let tr_pred c =
+ let c, args = decompose_app c in
+ match kind_of_term c, args with
+ | _, [a;b] when c = build_coq_and () ->
+ begin match tr_rle a, tr_rle b with
+ | (c1, t1), (t2, c2) when t1 = t2 ->
+ begin match tr_term c1, tr_term c2 with
+ | Tconst c1, Tconst c2 ->
+ Pin (tr_term t1, c1, c2)
+ | _ ->
+ raise NotGappa
+ end
+ | _ ->
+ raise NotGappa
+ end
+ | _ ->
+ raise NotGappa
+
+let is_R c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_R -> true
+ | _ -> false
+
+let tr_hyps =
+ List.fold_left
+ (fun acc (_,h) -> try tr_pred h :: acc with NotGappa -> acc) []
+
+let constr_of_string gl s =
+ let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
+ Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
+
+let var_name = function
+ | Name id ->
+ let s = string_of_id id in
+ let s = String.sub s 1 (String.length s - 1) in
+ mkVar (id_of_string s)
+ | Anonymous ->
+ assert false
+
+let build_proof_term c0 =
+ let bl,c = decompose_lam c0 in
+ List.fold_right
+ (fun (x,t) pf ->
+ mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |]))
+ bl c0
+
+let gappa_internal gl =
+ try
+ let c = tr_pred (pf_concl gl) in
+ let s = call_gappa (tr_hyps (pf_hyps_types gl)) c in
+ let pf = constr_of_string gl s in
+ let pf = build_proof_term pf in
+ Tacticals.tclTHEN (Tacmach.refine_no_check pf) Tactics.assumption gl
+ with
+ | NotGappa -> error "not a gappa goal"
+ | GappaFailed -> error "gappa failed"
+ | GappaProofFailed -> error "incorrect gappa proof term"
+
+let gappa_prepare =
+ let id = Ident (dummy_loc, id_of_string "gappa_prepare") in
+ lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id)))
+
+let gappa gl =
+ Coqlib.check_required_library ["Gappa"; "Gappa_tactic"];
+ Tacticals.tclTHEN (Lazy.force gappa_prepare) gappa_internal gl
+
+(*
+Local Variables:
+compile-command: "make -C ../.. bin/coqc.opt bin/coqide.opt"
+End:
+*)
+
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
deleted file mode 100644
index d5376b8d..00000000
--- a/contrib/dp/dp_simplify.ml
+++ /dev/null
@@ -1,117 +0,0 @@
-
-open Format
-open Fol
-
-let is_simplify_ident s =
- let is_simplify_char = function
- | 'a'..'z' | 'A'..'Z' | '0'..'9' -> true
- | _ -> false
- in
- try
- String.iter (fun c -> if not (is_simplify_char c) then raise Exit) s; true
- with Exit ->
- false
-
-let ident fmt s =
- if is_simplify_ident s then fprintf fmt "%s" s else fprintf fmt "|%s|" s
-
-let rec print_list sep print fmt = function
- | [] -> ()
- | [x] -> print fmt x
- | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-
-let space fmt () = fprintf fmt "@ "
-let comma fmt () = fprintf fmt ",@ "
-
-let rec print_term fmt = function
- | Cst n ->
- fprintf fmt "%d" n
- | Plus (a, b) ->
- fprintf fmt "@[(+@ %a@ %a)@]" print_term a print_term b
- | Moins (a, b) ->
- fprintf fmt "@[(-@ %a@ %a)@]" print_term a print_term b
- | Mult (a, b) ->
- fprintf fmt "@[(*@ %a@ %a)@]" print_term a print_term b
- | Div (a, b) ->
- fprintf fmt "@[(/@ %a@ %a)@]" print_term a print_term b
- | App (id, []) ->
- fprintf fmt "%a" ident id
- | App (id, tl) ->
- fprintf fmt "@[(%a@ %a)@]" ident id print_terms tl
-
-and print_terms fmt tl =
- print_list space print_term fmt tl
-
-let rec print_predicate fmt p =
- let pp = print_predicate in
- match p with
- | True ->
- fprintf fmt "TRUE"
- | False ->
- fprintf fmt "FALSE"
- | Fatom (Eq (a, b)) ->
- fprintf fmt "@[(EQ %a@ %a)@]" print_term a print_term b
- | Fatom (Le (a, b)) ->
- fprintf fmt "@[(<= %a@ %a)@]" print_term a print_term b
- | Fatom (Lt (a, b))->
- fprintf fmt "@[(< %a@ %a)@]" print_term a print_term b
- | Fatom (Ge (a, b)) ->
- fprintf fmt "@[(>= %a@ %a)@]" print_term a print_term b
- | Fatom (Gt (a, b)) ->
- fprintf fmt "@[(> %a@ %a)@]" print_term a print_term b
- | Fatom (Pred (id, tl)) ->
- fprintf fmt "@[(EQ (%a@ %a) |@@true|)@]" ident id print_terms tl
- | Imp (a, b) ->
- fprintf fmt "@[(IMPLIES@ %a@ %a)@]" pp a pp b
- | And (a, b) ->
- fprintf fmt "@[(AND@ %a@ %a)@]" pp a pp b
- | Or (a, b) ->
- fprintf fmt "@[(OR@ %a@ %a)@]" pp a pp b
- | Not a ->
- fprintf fmt "@[(NOT@ %a)@]" pp a
- | Forall (id, _, p) ->
- fprintf fmt "@[(FORALL (%a)@ %a)@]" ident id pp p
- | Exists (id, _, p) ->
- fprintf fmt "@[(EXISTS (%a)@ %a)@]" ident id pp p
-
-(**
-let rec string_list l = match l with
- [] -> ""
- | [e] -> e
- | e::l' -> e ^ " " ^ (string_list l')
-**)
-
-let print_query fmt (decls,concl) =
- let print_decl = function
- | DeclVar (id, [], t) ->
- fprintf fmt "@[;; %s : %s@]@\n" id t
- | DeclVar (id, l, t) ->
- fprintf fmt "@[;; %s : %a -> %s@]@\n"
- id (print_list comma pp_print_string) l t
- | DeclPred (id, []) ->
- fprintf fmt "@[;; %s : BOOLEAN @]@\n" id
- | DeclPred (id, l) ->
- fprintf fmt "@[;; %s : %a -> BOOLEAN@]@\n"
- id (print_list comma pp_print_string) l
- | DeclType id ->
- fprintf fmt "@[;; %s : TYPE@]@\n" id
- | Assert (id, f) ->
- fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f
- in
- List.iter print_decl decls;
- fprintf fmt "%a@." print_predicate concl
-
-let call q =
- let f = Filename.temp_file "coq_dp" ".sx" in
- let c = open_out f in
- let fmt = formatter_of_out_channel c in
- fprintf fmt "@[%a@]@." print_query q;
- close_out c;
- ignore (Sys.command (sprintf "cat %s" f));
- let cmd =
- sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" f
- in
- prerr_endline cmd; flush stderr;
- let out = Sys.command cmd in
- if out = 0 then Valid else if out = 1 then Invalid else Timeout
- (* TODO: effacer le fichier f et le fichier out *)
diff --git a/contrib/dp/dp_simplify.mli b/contrib/dp/dp_simplify.mli
deleted file mode 100644
index 03b6d347..00000000
--- a/contrib/dp/dp_simplify.mli
+++ /dev/null
@@ -1,4 +0,0 @@
-
-open Fol
-
-val call : query -> prover_answer
diff --git a/contrib/dp/dp_sorts.ml b/contrib/dp/dp_sorts.ml
deleted file mode 100644
index 7dbdfa56..00000000
--- a/contrib/dp/dp_sorts.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-
-open Fol
-
-let term_has_sort x s = Fatom (Pred ("%sort_" ^ s, [x]))
-
-let has_sort x s = term_has_sort (App (x, [])) s
-
-let rec form = function
- | True | False | Fatom _ as f -> f
- | Imp (f1, f2) -> Imp (form f1, form f2)
- | And (f1, f2) -> And (form f1, form f2)
- | Or (f1, f2) -> Or (form f1, form f2)
- | Not f -> Not (form f)
- | Forall (x, ("INT" as t), f) -> Forall (x, t, form f)
- | Forall (x, t, f) -> Forall (x, t, Imp (has_sort x t, form f))
- | Exists (x, ("INT" as t), f) -> Exists (x, t, form f)
- | Exists (x, t, f) -> Exists (x, t, Imp (has_sort x t, form f))
-
-let sort_ax = let r = ref 0 in fun () -> incr r; "sort_ax_" ^ string_of_int !r
-
-let hyp acc = function
- | Assert (id, f) ->
- (Assert (id, form f)) :: acc
- | DeclVar (id, _, "INT") as d ->
- d :: acc
- | DeclVar (id, [], t) as d ->
- (Assert (sort_ax (), has_sort id t)) :: d :: acc
- | DeclVar (id, l, t) as d ->
- let n = ref 0 in
- let xi =
- List.fold_left
- (fun l t -> incr n; ("x" ^ string_of_int !n, t) :: l) [] l
- in
- let f =
- List.fold_left
- (fun f (x,t) -> if t = "INT" then f else Imp (has_sort x t, f))
- (term_has_sort
- (App (id, List.rev_map (fun (x,_) -> App (x,[])) xi)) t)
- xi
- in
- let f = List.fold_left (fun f (x,t) -> Forall (x, t, f)) f xi in
- (Assert (sort_ax (), f)) :: d :: acc
- | DeclPred _ as d ->
- d :: acc
- | DeclType t as d ->
- (DeclPred ("%sort_" ^ t, [t])) :: d :: acc
-
-let query (hyps, f) =
- let hyps' = List.fold_left hyp [] hyps in
- List.rev hyps', form f
-
diff --git a/contrib/dp/dp_sorts.mli b/contrib/dp/dp_sorts.mli
deleted file mode 100644
index 9e74f997..00000000
--- a/contrib/dp/dp_sorts.mli
+++ /dev/null
@@ -1,4 +0,0 @@
-
-open Fol
-
-val query : query -> query
diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml
index e1ddb039..e24049ad 100644
--- a/contrib/dp/dp_why.ml
+++ b/contrib/dp/dp_why.ml
@@ -4,6 +4,18 @@
open Format
open Fol
+type proof =
+ | Immediate of Term.constr
+ | Fun_def of string * (string * typ) list * typ * term
+
+let proofs = Hashtbl.create 97
+let proof_name =
+ let r = ref 0 in fun () -> incr r; "dp_axiom__" ^ string_of_int !r
+
+let add_proof pr = let n = proof_name () in Hashtbl.add proofs n pr; n
+
+let find_proof = Hashtbl.find proofs
+
let rec print_list sep print fmt = function
| [] -> ()
| [x] -> print fmt x
diff --git a/contrib/dp/dp_why.mli b/contrib/dp/dp_why.mli
new file mode 100644
index 00000000..b38a3d37
--- /dev/null
+++ b/contrib/dp/dp_why.mli
@@ -0,0 +1,17 @@
+
+open Fol
+
+(* generation of the Why file *)
+
+val output_file : string -> query -> unit
+
+(* table to translate the proofs back to Coq (used in dp_zenon) *)
+
+type proof =
+ | Immediate of Term.constr
+ | Fun_def of string * (string * typ) list * typ * term
+
+val add_proof : proof -> string
+val find_proof : string -> proof
+
+
diff --git a/contrib/dp/dp_zenon.ml b/contrib/dp/dp_zenon.ml
deleted file mode 100644
index 57b0a44f..00000000
--- a/contrib/dp/dp_zenon.ml
+++ /dev/null
@@ -1,103 +0,0 @@
-
-open Format
-open Fol
-
-let rec print_list sep print fmt = function
- | [] -> ()
- | [x] -> print fmt x
- | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-
-let space fmt () = fprintf fmt "@ "
-
-let rec print_term fmt = function
- | Cst n ->
- fprintf fmt "%d" n
- | Plus (a, b) ->
- fprintf fmt "@[(+@ %a@ %a)@]" print_term a print_term b
- | Moins (a, b) ->
- fprintf fmt "@[(-@ %a@ %a)@]" print_term a print_term b
- | Mult (a, b) ->
- fprintf fmt "@[(*@ %a@ %a)@]" print_term a print_term b
- | Div (a, b) ->
- fprintf fmt "@[(/@ %a@ %a)@]" print_term a print_term b
- | App (id, []) ->
- fprintf fmt "%s" id
- | App (id, tl) ->
- fprintf fmt "@[(%s@ %a)@]" id print_terms tl
-
-and print_terms fmt tl =
- print_list space print_term fmt tl
-
-let rec print_predicate fmt p =
- let pp = print_predicate in
- match p with
- | True ->
- fprintf fmt "True"
- | False ->
- fprintf fmt "False"
- | Fatom (Eq (a, b)) ->
- fprintf fmt "@[(= %a@ %a)@]" print_term a print_term b
- | Fatom (Le (a, b)) ->
- fprintf fmt "@[(<= %a@ %a)@]" print_term a print_term b
- | Fatom (Lt (a, b))->
- fprintf fmt "@[(< %a@ %a)@]" print_term a print_term b
- | Fatom (Ge (a, b)) ->
- fprintf fmt "@[(>= %a@ %a)@]" print_term a print_term b
- | Fatom (Gt (a, b)) ->
- fprintf fmt "@[(> %a@ %a)@]" print_term a print_term b
- | Fatom (Pred (id, tl)) ->
- fprintf fmt "@[(%s@ %a)@]" id print_terms tl
- | Imp (a, b) ->
- fprintf fmt "@[(=>@ %a@ %a)@]" pp a pp b
- | And (a, b) ->
- fprintf fmt "@[(/\\@ %a@ %a)@]" pp a pp b
- | Or (a, b) ->
- fprintf fmt "@[(\\/@ %a@ %a)@]" pp a pp b
- | Not a ->
- fprintf fmt "@[(-.@ %a)@]" pp a
- | Forall (id, t, p) ->
- fprintf fmt "@[(A. ((%s \"%s\")@ %a))@]" id t pp p
- | Exists (id, t, p) ->
- fprintf fmt "@[(E. ((%s \"%s\")@ %a))@]" id t pp p
-
-let rec string_of_type_list = function
- | [] -> ""
- | e :: l' -> e ^ " -> " ^ (string_of_type_list l')
-
-let print_query fmt (decls,concl) =
- let print_decl = function
- | DeclVar (id, [], t) ->
- fprintf fmt "@[;; %s: %s@]@\n" id t
- | DeclVar (id, l, t) ->
- fprintf fmt "@[;; %s: %s%s@]@\n"
- id (string_of_type_list l) t
- | DeclPred (id, l) ->
- fprintf fmt "@[;; %s: %sBOOLEAN@]@\n"
- id (string_of_type_list l)
- | DeclType id ->
- fprintf fmt "@[;; %s: TYPE@]@\n" id
- | Assert (id, f) ->
- fprintf fmt "@[\"%s\" %a@]@\n" id print_predicate f
- in
- List.iter print_decl decls;
- fprintf fmt "$goal %a@." print_predicate concl
-
-let call q =
- let f = Filename.temp_file "coq_dp" ".znn" in
- let c = open_out f in
- let fmt = formatter_of_out_channel c in
- fprintf fmt "@[%a@]@." print_query q;
- close_out c;
- ignore (Sys.command (sprintf "cat %s" f));
- let cmd =
- sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" f
- in
- prerr_endline cmd; flush stderr;
- let out = Sys.command cmd in
- if out = 0 then Valid
- else if out = 1 then Invalid
- else if out = 137 then Timeout
- else Util.anomaly "malformed Zenon input file"
- (* TODO: effacer le fichier f et le fichier out *)
-
-
diff --git a/contrib/dp/dp_zenon.mli b/contrib/dp/dp_zenon.mli
index 03b6d347..0a727d1f 100644
--- a/contrib/dp/dp_zenon.mli
+++ b/contrib/dp/dp_zenon.mli
@@ -1,4 +1,7 @@
open Fol
-val call : query -> prover_answer
+val set_debug : bool -> unit
+
+val proof_from_file : string -> Proof_type.tactic
+
diff --git a/contrib/dp/dp_zenon.mll b/contrib/dp/dp_zenon.mll
new file mode 100644
index 00000000..2fc2a5f4
--- /dev/null
+++ b/contrib/dp/dp_zenon.mll
@@ -0,0 +1,181 @@
+
+{
+
+ open Lexing
+ open Pp
+ open Util
+ open Names
+ open Tacmach
+ open Dp_why
+ open Tactics
+ open Tacticals
+
+ let debug = ref false
+ let set_debug b = debug := b
+
+ let buf = Buffer.create 1024
+
+ let string_of_global env ref =
+ Libnames.string_of_qualid (Nametab.shortest_qualid_of_global env ref)
+
+ let axioms = ref []
+
+ (* we cannot interpret the terms as we read them (since some lemmas
+ may need other lemmas to be already interpreted) *)
+ type lemma = { l_id : string; l_type : string; l_proof : string }
+ type zenon_proof = lemma list * string
+
+}
+
+let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9' '\'']+
+let space = [' ' '\t' '\r']
+
+rule start = parse
+| "(* BEGIN-PROOF *)" "\n" { scan lexbuf }
+| _ { start lexbuf }
+| eof { anomaly "malformed Zenon proof term" }
+
+(* here we read the lemmas and the main proof term;
+ meanwhile we maintain the set of axioms that were used *)
+
+and scan = parse
+| "Let" space (ident as id) space* ":"
+ { let t = read_coq_term lexbuf in
+ let p = read_lemma_proof lexbuf in
+ let l,pr = scan lexbuf in
+ { l_id = id; l_type = t; l_proof = p } :: l, pr }
+| "Definition theorem:"
+ { let t = read_main_proof lexbuf in [], t }
+| _ | eof
+ { anomaly "malformed Zenon proof term" }
+
+and read_coq_term = parse
+| "." "\n"
+ { let s = Buffer.contents buf in Buffer.clear buf; s }
+| "coq__" (ident as id) (* a Why keyword renamed *)
+ { Buffer.add_string buf id; read_coq_term lexbuf }
+| ("dp_axiom__" ['0'-'9']+) as id
+ { axioms := id :: !axioms; Buffer.add_string buf id; read_coq_term lexbuf }
+| _ as c
+ { Buffer.add_char buf c; read_coq_term lexbuf }
+| eof
+ { anomaly "malformed Zenon proof term" }
+
+and read_lemma_proof = parse
+| "Proof" space
+ { read_coq_term lexbuf }
+| _ | eof
+ { anomaly "malformed Zenon proof term" }
+
+(* skip the main proof statement and then read its term *)
+and read_main_proof = parse
+| ":=" "\n"
+ { read_coq_term lexbuf }
+| _
+ { read_main_proof lexbuf }
+| eof
+ { anomaly "malformed Zenon proof term" }
+
+
+{
+
+ let read_zenon_proof f =
+ Buffer.clear buf;
+ let c = open_in f in
+ let lb = from_channel c in
+ let p = start lb in
+ close_in c;
+ if not !debug then begin try Sys.remove f with _ -> () end;
+ p
+
+ let constr_of_string gl s =
+ let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
+ Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
+
+ (* we are lazy here: we build strings containing Coq terms using a *)
+ (* pretty-printer Fol -> Coq *)
+ module Coq = struct
+ open Format
+ open Fol
+
+ let rec print_list sep print fmt = function
+ | [] -> ()
+ | [x] -> print fmt x
+ | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
+
+ let space fmt () = fprintf fmt "@ "
+ let comma fmt () = fprintf fmt ",@ "
+
+ let rec print_typ fmt = function
+ | Tvar x -> fprintf fmt "%s" x
+ | Tid ("int", []) -> fprintf fmt "Z"
+ | Tid (x, []) -> fprintf fmt "%s" x
+ | Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t
+ | Tid (x,tl) ->
+ fprintf fmt "(%s %a)" x (print_list comma print_typ) tl
+
+ let rec print_term fmt = function
+ | Cst n ->
+ fprintf fmt "%d" n
+ | Plus (a, b) ->
+ fprintf fmt "@[(Zplus %a %a)@]" print_term a print_term b
+ | Moins (a, b) ->
+ fprintf fmt "@[(Zminus %a %a)@]" print_term a print_term b
+ | Mult (a, b) ->
+ fprintf fmt "@[(Zmult %a %a)@]" print_term a print_term b
+ | Div (a, b) ->
+ fprintf fmt "@[(Zdiv %a %a)@]" print_term a print_term b
+ | App (id, []) ->
+ fprintf fmt "%s" id
+ | App (id, tl) ->
+ fprintf fmt "@[(%s %a)@]" id print_terms tl
+
+ and print_terms fmt tl =
+ print_list space print_term fmt tl
+
+ (* builds the text for "forall vars, f vars = t" *)
+ let fun_def_axiom f vars t =
+ let binder fmt (x,t) = fprintf fmt "(%s: %a)" x print_typ t in
+ fprintf str_formatter
+ "@[(forall %a, %s %a = %a)@]@."
+ (print_list space binder) vars f
+ (print_list space (fun fmt (x,_) -> pp_print_string fmt x)) vars
+ print_term t;
+ flush_str_formatter ()
+
+ end
+
+ let prove_axiom id = match Dp_why.find_proof id with
+ | Immediate t ->
+ exact_check t
+ | Fun_def (f, vars, ty, t) ->
+ tclTHENS
+ (fun gl ->
+ let s = Coq.fun_def_axiom f vars t in
+ if !debug then Format.eprintf "axiom fun def = %s@." s;
+ let c = constr_of_string gl s in
+ assert_tac true (Name (id_of_string id)) c gl)
+ [tclTHEN intros reflexivity; tclIDTAC]
+
+ let exact_string s gl =
+ let c = constr_of_string gl s in
+ exact_check c gl
+
+ let interp_zenon_proof (ll,p) =
+ let interp_lemma l gl =
+ let ty = constr_of_string gl l.l_type in
+ tclTHENS
+ (assert_tac true (Name (id_of_string l.l_id)) ty)
+ [exact_string l.l_proof; tclIDTAC]
+ gl
+ in
+ tclTHEN (tclMAP interp_lemma ll) (exact_string p)
+
+ let proof_from_file f =
+ axioms := [];
+ msgnl (str "proof_from_file " ++ str f);
+ let zp = read_zenon_proof f in
+ msgnl (str "proof term is " ++ str (snd zp));
+ tclTHEN (tclMAP prove_axiom !axioms) (interp_zenon_proof zp)
+
+}
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
index a85469cc..b94bd3e3 100644
--- a/contrib/dp/fol.mli
+++ b/contrib/dp/fol.mli
@@ -45,4 +45,11 @@ type query = decl list * form
(* prover result *)
-type prover_answer = Valid | Invalid | DontKnow | Timeout
+type prover_answer =
+ | Valid of string option
+ | Invalid
+ | DontKnow
+ | Timeout
+ | NoAnswer
+ | Failure of string
+
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index eb7fb73b..99bcf477 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_dp.ml4 7165 2005-06-24 12:56:46Z coq $ *)
+(* $Id: g_dp.ml4 10924 2008-05-13 14:01:11Z filliatr $ *)
open Dp
@@ -16,6 +16,14 @@ TACTIC EXTEND Simplify
[ "simplify" ] -> [ simplify ]
END
+TACTIC EXTEND Ergo
+ [ "ergo" ] -> [ ergo ]
+END
+
+TACTIC EXTEND Yices
+ [ "yices" ] -> [ yices ]
+END
+
TACTIC EXTEND CVCLite
[ "cvcl" ] -> [ cvc_lite ]
END
@@ -28,6 +36,18 @@ TACTIC EXTEND Zenon
[ "zenon" ] -> [ zenon ]
END
+TACTIC EXTEND Gwhy
+ [ "gwhy" ] -> [ gwhy ]
+END
+
+TACTIC EXTEND Gappa_internal
+ [ "gappa_internal" ] -> [ Dp_gappa.gappa_internal ]
+END
+
+TACTIC EXTEND Gappa
+ [ "gappa" ] -> [ Dp_gappa.gappa ]
+END
+
(* should be part of basic tactics syntax *)
TACTIC EXTEND admit
[ "admit" ] -> [ Tactics.admit_as_an_axiom ]
@@ -36,3 +56,24 @@ END
VERNAC COMMAND EXTEND Dp_hint
[ "Dp_hint" ne_global_list(l) ] -> [ dp_hint l ]
END
+
+VERNAC COMMAND EXTEND Dp_timeout
+| [ "Dp_timeout" natural(n) ] -> [ dp_timeout n ]
+END
+
+VERNAC COMMAND EXTEND Dp_prelude
+| [ "Dp_prelude" string_list(l) ] -> [ dp_prelude l ]
+END
+
+VERNAC COMMAND EXTEND Dp_predefined
+| [ "Dp_predefined" global(g) "=>" string(s) ] -> [ dp_predefined g s ]
+END
+
+VERNAC COMMAND EXTEND Dp_debug
+| [ "Dp_debug" ] -> [ dp_debug true; Dp_zenon.set_debug true ]
+END
+
+VERNAC COMMAND EXTEND Dp_trace
+| [ "Dp_trace" ] -> [ dp_trace true ]
+END
+
diff --git a/contrib/dp/test2.v b/contrib/dp/test2.v
index 4e933a3c..3e4c0f6d 100644
--- a/contrib/dp/test2.v
+++ b/contrib/dp/test2.v
@@ -5,6 +5,10 @@ Require Import List.
Open Scope list_scope.
Open Scope Z_scope.
+Dp_debug.
+Dp_timeout 3.
+Require Export zenon.
+
Definition neg (z:Z) : Z := match z with
| Z0 => Z0
| Zpos p => Zneg p
@@ -18,9 +22,7 @@ Open Scope nat_scope.
Print plus.
Goal forall x, x+0=x.
- induction x.
- zenon.
- zenon.
+ induction x; ergo.
(* simplify resoud le premier, pas le second *)
Admitted.
diff --git a/contrib/dp/test_gappa.v b/contrib/dp/test_gappa.v
new file mode 100644
index 00000000..eb65a59d
--- /dev/null
+++ b/contrib/dp/test_gappa.v
@@ -0,0 +1,91 @@
+Require Export Gappa_tactic.
+Require Export Reals.
+
+Open Scope Z_scope.
+Open Scope R_scope.
+
+Lemma test_base10 :
+ forall x y:R,
+ 0 <= x <= 4 ->
+ 0 <= x * (24 * powerRZ 10 (-1)) <= 10.
+Proof.
+ gappa.
+Qed.
+
+(*
+@rnd = float< ieee_32, zr >;
+a = rnd(a_); b = rnd(b_);
+{ a in [3.2,3.3] /\ b in [1.4,1.9] ->
+ rnd(a - b) - (a - b) in [0,0] }
+*)
+
+Definition rnd := gappa_rounding (rounding_float roundZR 43 (120)).
+
+Lemma test_float3 :
+ forall a_ b_ a b : R,
+ a = rnd a_ ->
+ b = rnd b_ ->
+ 52 / 16 <= a <= 53 / 16 ->
+ 22 / 16 <= b <= 30 / 16 ->
+ 0 <= rnd (a - b) - (a - b) <= 0.
+Proof.
+ unfold rnd.
+ gappa.
+Qed.
+
+Lemma test_float2 :
+ forall x y:R,
+ 0 <= x <= 1 ->
+ 0 <= y <= 1 ->
+ 0 <= gappa_rounding (rounding_float roundNE 53 (1074)) (x+y) <= 2.
+Proof.
+ gappa.
+Qed.
+
+Lemma test_float1 :
+ forall x y:R,
+ 0 <= gappa_rounding (rounding_fixed roundDN (0)) x -
+ gappa_rounding (rounding_fixed roundDN (0)) y <= 0 ->
+ Rabs (x - y) <= 1.
+Proof.
+ gappa.
+Qed.
+
+Lemma test1 :
+ forall x y:R,
+ 0 <= x <= 1 ->
+ 0 <= -y <= 1 ->
+ 0 <= x * (-y) <= 1.
+Proof.
+ gappa.
+Qed.
+
+Lemma test2 :
+ forall x y:R,
+ 3/4 <= x <= 3 ->
+ 0 <= sqrt x <= 1775 * (powerRZ 2 (-10)).
+Proof.
+ gappa.
+Qed.
+
+Lemma test3 :
+ forall x y z:R,
+ 0 <= x - y <= 3 ->
+ -2 <= y - z <= 4 ->
+ -2 <= x - z <= 7.
+Proof.
+ gappa.
+Qed.
+
+Lemma test4 :
+ forall x1 x2 y1 y2 : R,
+ 1 <= Rabs y1 <= 1000 ->
+ 1 <= Rabs y2 <= 1000 ->
+ - powerRZ 2 (-53) <= (x1 - y1) / y1 <= powerRZ 2 (-53) ->
+ - powerRZ 2 (-53) <= (x2 - y2) / y2 <= powerRZ 2 (-53) ->
+ - powerRZ 2 (-51) <= (x1 * x2 - y1 * y2) / (y1 * y2) <= powerRZ 2 (-51).
+Proof.
+ gappa.
+Qed.
+
+
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index 52a57a0c..a6d4f2e1 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -2,48 +2,115 @@
Require Import ZArith.
Require Import Classical.
+Dp_debug.
+Dp_timeout 3.
+
+(* module renamings *)
+
+Module M.
+ Parameter t : Set.
+End M.
+
+Lemma test_module_0 : forall x:M.t, x=x.
+ergo.
+Qed.
+
+Module N := M.
+
+Lemma test_module_renaming_0 : forall x:N.t, x=x.
+ergo.
+Qed.
+
+Dp_predefined M.t => "int".
+
+Lemma test_module_renaming_1 : forall x:N.t, x=x.
+ergo.
+Qed.
+
+(* Coq lists *)
+
+Require Export List.
+
+Lemma test_pol_0 : forall l:list nat, l=l.
+ergo.
+Qed.
+
+Parameter nlist: list nat -> Prop.
+
+Lemma poly_1 : forall l, nlist l -> True.
+intros.
+simplify.
+Qed.
+
+(* user lists *)
+
+Inductive list (A:Set) : Set :=
+| nil : list A
+| cons: forall a:A, list A -> list A.
+
+Fixpoint app (A:Set) (l m:list A) {struct l} : list A :=
+match l with
+| nil => m
+| cons a l1 => cons A a (app A l1 m)
+end.
+
+Lemma entail: (nil Z) = app Z (nil Z) (nil Z) -> True.
+intros; ergo.
+Qed.
+
+(* polymorphism *)
+Require Import List.
+
+Inductive mylist (A:Set) : Set :=
+ mynil : mylist A
+| mycons : forall a:A, mylist A -> mylist A.
+
+Parameter my_nlist: mylist nat -> Prop.
+
+ Goal forall l, my_nlist l -> True.
+ intros.
+ simplify.
+Qed.
+
(* First example with the 0 and the equality translated *)
Goal 0 = 0.
-zenon.
+simplify.
Qed.
-
(* Examples in the Propositional Calculus
and theory of equality *)
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 *)
Open Scope Z_scope.
Goal 1 + 1 = 2.
-simplify.
+yices.
Qed.
@@ -57,14 +124,12 @@ Qed.
Goal (forall (x y : Z), x = y) -> 0=1.
try zenon.
-simplify.
+ergo.
Qed.
Goal forall (x: nat), (x + 0 = x)%nat.
-induction x0.
-zenon.
-zenon.
+induction x0; ergo.
Qed.
@@ -106,7 +171,7 @@ Inductive even : Z -> Prop :=
unlike CVC Lite *)
Goal even 4.
-cvcl.
+ergo.
Qed.
@@ -115,8 +180,7 @@ Definition skip_z (z : Z) (n : nat) := n.
Definition skip_z1 := skip_z.
Goal forall (z : Z) (n : nat), skip_z z n = skip_z1 z n.
-
-zenon.
+yices.
Qed.
@@ -133,8 +197,7 @@ Dp_hint add_S.
unlike zenon *)
Goal forall n : nat, add n 0 = n.
-
-induction n ; zenon.
+induction n ; yices.
Qed.
@@ -144,8 +207,8 @@ Definition pred (n : nat) : nat := match n with
end.
Goal forall n : nat, n <> 0%nat -> pred (S n) <> 0%nat.
-
-zenon.
+yices.
+(*zenon.*)
Qed.
@@ -157,7 +220,7 @@ end.
Goal forall n : nat, plus n 0%nat = n.
-induction n; zenon.
+induction n; ergo.
Qed.
@@ -173,8 +236,11 @@ with odd_b (n : nat) : bool := match n with
end.
Goal even_b (S (S O)) = true.
-
+ergo.
+(*
+simplify.
zenon.
+*)
Qed.
@@ -184,7 +250,8 @@ 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.
-zenon.
+yices.
+(*zenon.*)
Qed.
@@ -194,7 +261,8 @@ Qed.
Parameter poly_f : forall A:Set, A->A.
Goal forall x:nat, poly_f nat x = poly_f nat x.
-zenon.
+ergo.
+(*zenon.*)
Qed.
diff --git a/contrib/dp/zenon.v b/contrib/dp/zenon.v
new file mode 100644
index 00000000..4ad00a11
--- /dev/null
+++ b/contrib/dp/zenon.v
@@ -0,0 +1,94 @@
+(* Copyright 2004 INRIA *)
+(* $Id: zenon.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+
+Require Export Classical.
+
+Lemma zenon_nottrue :
+ (~True -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_noteq : forall (T : Type) (t : T),
+ ((t <> t) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_and : forall P Q : Prop,
+ (P -> Q -> False) -> (P /\ Q -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_or : forall P Q : Prop,
+ (P -> False) -> (Q -> False) -> (P \/ Q -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_imply : forall P Q : Prop,
+ (~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_equiv : forall P Q : Prop,
+ (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notand : forall P Q : Prop,
+ (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notor : forall P Q : Prop,
+ (~P -> ~Q -> False) -> (~(P \/ Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notimply : forall P Q : Prop,
+ (P -> ~Q -> False) -> (~(P -> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notequiv : forall P Q : Prop,
+ (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
+ (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
+ ((P t) -> False) -> ((forall x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
+ (~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
+ (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
+Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.
+
+Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
+Proof. auto. Qed.
+
+Lemma zenon_equal_step :
+ forall (S T : Type) (fa fb : S -> T) (a b : S),
+ (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
+Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.
+
+Lemma zenon_pnotp : forall P Q : Prop,
+ (P = Q) -> (P -> ~Q -> False).
+Proof. intros P Q Ha. rewrite Ha. auto. Qed.
+
+Lemma zenon_notequal : forall (T : Type) (a b : T),
+ (a = b) -> (a <> b -> False).
+Proof. auto. Qed.
+
+Ltac zenon_intro id :=
+ intro id || let nid := fresh in (intro nid; clear nid)
+.
+
+Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
+Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
+Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
+Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
+Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
+Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
+Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
+Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
+Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
+Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.
+
+Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
+Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.