contrib/dp

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

17 files changed, 368 insertions, 427 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index af684e6e9..412786e1f 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -25,8 +25,12 @@ open Coqlib
 open Hipattern
 open Libnames
 open Declarations
+open Dp_why
 
 let debug = ref false
+let set_debug b = debug := b
+let timeout = ref 10
+let set_timeout n = timeout := n
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 let coq_modules =
@@ -52,6 +56,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
@@ -374,7 +379,7 @@ and axiomatize_body env r id d = match r with
 		     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|])) -> 
@@ -401,21 +406,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
@@ -581,6 +586,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)
@@ -639,14 +646,18 @@ let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ())
 let sprintf = Format.sprintf
 
 let call_simplify fwhy =
-  if Sys.command (sprintf "why --simplify %s" fwhy) <> 0 then
-    anomaly ("call to why --simplify " ^ fwhy ^ " failed; please report");
+  let cmd = sprintf "why --no-prelude --simplify %s" fwhy in
+  if Sys.command cmd <> 0 then
+    anomaly ("call to " ^ cmd ^ " failed; please report");
   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
 
@@ -655,28 +666,34 @@ let call_zenon fwhy =
   if Sys.command cmd <> 0 then
     anomaly ("call to " ^ cmd ^ " failed; please report");
   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
-  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)
+    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];
-  r
+  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_cvcl fwhy =
   if Sys.command (sprintf "why --cvcl %s" fwhy) <> 0 then
     anomaly ("call to why --cvcl " ^ fwhy ^ " failed; please report");
   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
 
@@ -689,7 +706,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 
@@ -698,7 +716,7 @@ 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
@@ -719,7 +737,8 @@ let dp prover gl =
   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 _ -> Tactics.admit_as_an_axiom gl
       | Invalid -> error "Invalid"
       | DontKnow -> error "Don't know"
       | Timeout -> error "Timeout"
@@ -742,7 +761,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 ->
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index 3dad469c6..841c38873 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -8,5 +8,7 @@ val harvey : tactic
 val zenon : tactic
 
 val dp_hint : reference list -> unit
+val set_timeout : int -> unit
+val set_debug : bool -> unit
 
 
diff --git a/contrib/dp/dp_cvcl.ml b/contrib/dp/dp_cvcl.ml
deleted file mode 100644
index 05d430812..000000000
--- 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 03b6d3475..000000000
--- 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_simplify.ml b/contrib/dp/dp_simplify.ml
deleted file mode 100644
index d5376b8df..000000000
--- 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 03b6d3475..000000000
--- 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 7dbdfa561..000000000
--- 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 9e74f9973..000000000
--- 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 e1ddb039b..e24049ad6 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 000000000..b38a3d376
--- /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 57b0a44fc..000000000
--- 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 03b6d3475..0a727d1f1 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 000000000..2fc2a5f4e
--- /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 a85469cc6..5347a86f2 100644
--- a/contrib/dp/fol.mli
+++ b/contrib/dp/fol.mli
@@ -45,4 +45,4 @@ type query = decl list * form
 
 (* prover result *)
 
-type prover_answer = Valid | Invalid | DontKnow | Timeout
+type prover_answer = Valid of string option | Invalid | DontKnow | Timeout
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 7adc6f382..afbd59224 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -36,3 +36,12 @@ 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) ] -> [ set_timeout n ]
+END
+
+VERNAC COMMAND EXTEND Dp_debug
+| [ "Dp_debug" ] -> [ set_debug true; Dp_zenon.set_debug true ]
+END
+
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index 52a57a0cb..26cb2823c 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -57,7 +57,6 @@ Qed.
 
 Goal (forall (x y : Z), x = y) -> 0=1.
 try zenon.
-simplify.
 Qed.
 
 Goal forall (x: nat), (x + 0 = x)%nat.
@@ -133,8 +132,7 @@ Dp_hint add_S.
    unlike zenon *)
 
 Goal forall n : nat, add n 0 = n.
-
-induction n ; zenon.
+induction n ; simplify.
 Qed.
 
 
diff --git a/contrib/dp/zenon.v b/contrib/dp/zenon.v
new file mode 100644
index 000000000..2ef943675
--- /dev/null
+++ b/contrib/dp/zenon.v
@@ -0,0 +1,94 @@
+(*  Copyright 2004 INRIA  *)
+(*  $Id: zenon.v,v 1.6 2006-02-16 09:22:46 doligez Exp $  *)
+
+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.