new csdp cache + improved error message

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

8 files changed, 95 insertions, 38 deletions

diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 5b89579c8..88b53583d 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -456,6 +456,41 @@ Proof.
   simpl.   apply  addon.(SORrm).(morph0).
 Qed.
 
+Fixpoint ge_bool (n m  : nat) : bool :=
+ match n with 
+   | O   => match m with 
+            |  O => true
+            | S _ => false
+          end
+   | S n  => match m with 
+               | O => true
+               | S m => ge_bool n m 
+             end
+   end.
+
+Lemma ge_bool_cases : forall n m, (if ge_bool n m then n >= m else n < m)%nat.
+Proof.
+  induction n ; simpl.
+  destruct m ; simpl.
+  constructor.
+  omega.
+  destruct m.
+  constructor.
+  omega.
+  generalize (IHn m).
+  destruct (ge_bool n m) ; omega.
+Qed.
+
+
+Fixpoint xhyps_of_psatz (base:nat) (acc : list nat) (prf : Psatz)  : list nat :=
+  match prf with 
+    | PsatzC _ | PsatzZ | PsatzSquare _ => acc
+    | PsatzMulC _ prf => xhyps_of_psatz base acc prf
+    | PsatzAdd e1 e2 | PsatzMulE e1 e2 => xhyps_of_psatz base (xhyps_of_psatz base acc e2) e1
+    | PsatzIn n => if ge_bool n base then (n::acc) else acc
+  end.
+
+
 (* roughly speaking, normalise_pexpr_correct is a proof of
   forall env p, eval_pexpr env p == eval_pol env (normalise_pexpr p) *)
 
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index a23671fde..42e0acb58 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -8,7 +8,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                           *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -322,3 +322,6 @@ Set Implicit Arguments.
 
 End S.
 
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 65ea366fd..212478720 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -1081,6 +1081,25 @@ Proof.
   apply ZChecker_sound.
 Qed.
 
+Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof)  : list nat :=
+  match pt with
+    | DoneProof => acc
+    | RatProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
+    | CutProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
+    | EnumProof c1 c2 l => 
+      let acc := xhyps_of_psatz base (xhyps_of_psatz base acc c2) c1 in
+        List.fold_left (xhyps_of_pt (S base)) l acc
+  end.
+
+Definition hyps_of_pt (pt : ZArithProof) : list nat := xhyps_of_pt 0 nil pt.
+
+
+(*Lemma hyps_of_pt_correct : forall pt l, *)
+
+
+
+
+
 
 Open Scope Z_scope.
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 286e866fd..acef98e78 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1322,8 +1322,8 @@ let lift_ratproof  prover l =
   | None -> None
   | Some c -> Some (Mc.RatProof( c,Mc.DoneProof))
 
-type csdpcert = Sos.positivstellensatz option
-type micromega_polys = (Mc.q Mc.pol * Mc.op1) list
+type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list
+type csdp_certificate = S of Sos.positivstellensatz option | F of string
 type provername = string * int option
 
 open Persistent_cache
@@ -1336,14 +1336,19 @@ end)
 
 let csdp_cache = "csdp.cache" 
 
-let really_call_csdpcert : provername -> micromega_polys -> csdpcert =
+let really_call_csdpcert : provername -> micromega_polys -> Sos.positivstellensatz option  =
   fun provername poly -> 
 
   let cmdname =
     List.fold_left Filename.concat (Envars.coqlib ())
       ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
 
-    command cmdname [| cmdname |] (provername,poly) 
+    match command cmdname [| cmdname |] (provername,poly) with
+      | None -> failwith "unix error"
+      | Some res -> 
+	  match res with
+	    | F str -> failwith str
+	    | S res -> res
 
 
 
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index 3bc81c576..96b369acf 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -20,6 +20,11 @@ module Mc = Micromega
 module Ml2C = Mutils.CamlToCoq
 module C2Ml = Mutils.CoqToCaml
 
+type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list
+type csdp_certificate = S of Sos.positivstellensatz option | F of string
+type provername = string * int option
+
+
 let debug = false
 
 module M =
@@ -135,10 +140,10 @@ let real_nonlinear_prover d l =
 
   let proof = list_fold_right_elements 
    (fun s t -> Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) in
-   Some proof
+   S (Some proof)
  with 
-  | Sos.TooDeep -> None
-
+  | Sos.TooDeep -> S None
+  |    x        ->   F (Printexc.to_string x)
 
 (* This is somewhat buggy, over Z, strict inequality vanish... *)
 let pure_sos  l =
@@ -159,15 +164,11 @@ let pure_sos  l =
   let proof = Sum(Axiom_lt i, pos) in
 (*  let s,proof' = scale_certificate proof in
   let cert  = snd (cert_of_pos proof') in *)
-   Some proof
+    S (Some proof)
  with
-  | Not_found -> (* This is no strict inequality *) None
-  |  x        -> None
-
+  | Not_found -> (* This is no strict inequality *) F "pure_sos cannot solve this goal"
+  |  x        -> F (Printf.sprintf "pure_sos : %s"  (Printexc.to_string x))
 
-type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list
-type csdp_certificate = Sos.positivstellensatz option
-type provername = string * int option
 
 
 let run_prover prover pb = 
@@ -178,10 +179,10 @@ let run_prover prover pb =
 
 
 let main () =
-  let (prover,poly) = (input_value stdin : provername * micromega_polys) in
-  let cert = run_prover prover poly in
-  output_value stdout (cert:csdp_certificate);
-  exit 0;;
+    let (prover,poly) = (input_value stdin : provername * micromega_polys) in
+    let cert = run_prover prover poly in
+      output_value stdout (cert:csdp_certificate);
+      exit 0 ;;
 
 let _ = main () in ()
 
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 72b2a70b6..a568f4157 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -357,14 +357,14 @@ let command exe_path args vl =
   and (stdout_read,stdout_write) = Unix.pipe ()
   and (stderr_read,stderr_write) = Unix.pipe () in
 
-  (* Creating channels from dile descr *)
+  (* Creating channels from file descr *)
   let outch = Unix.out_channel_of_descr stdin_write in
   let inch  = Unix.in_channel_of_descr  stdout_read in 
 
   (* Create the process *)
   let pid = Unix.create_process exe_path args stdin_read stdout_write stderr_write in
 
-  (* Write the data on the stdin of the future process *)
+  (* Write the data on the stdin of the created process *)
     Marshal.to_channel outch vl [Marshal.No_sharing] ; 
     flush outch ;
     
@@ -374,7 +374,8 @@ let command exe_path args vl =
   (* Recover the result *)
     let res = 
       match status with
-	| Unix.WEXITED 0 -> Marshal.from_channel inch 
+	| Unix.WEXITED 0 -> 
+	    Some (Marshal.from_channel inch)
 	| _         -> None in
      
     (* Cleanup  *)
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index cbacc48e4..87c9d1bbe 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -25,7 +25,9 @@ module type PHashtable =
 
 
     val open_in : string -> 'a t
-    (** [open_in f] rebuilds a table from the records stored in file [f] *)
+    (** [open_in f] rebuilds a table from the records stored in file [f].
+	As marshaling is not type-safe, it migth segault.
+    *)
 
     val find : 'a t -> key -> 'a
     (** find has the specification of Hashtable.find *)
@@ -42,7 +44,7 @@ module type PHashtable =
 
     val memo : string -> (key -> 'a) -> (key -> 'a)
       (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
-	  Note that the cache is just loaded when needed *)
+	  Note that the cache will only be loaded when the function is used for the first time *)
 
   end
 
@@ -89,16 +91,6 @@ let finally f rst =
     ); raise x
 
 
-(** [from_file f] returns a hashtable by parsing records from file [f].
-    Elements of the file are marshelled pairs of Caml structures.
-    (To ensure portability across platforms, closures are not allowed.)
-
-    Raises Sys_error if the file cannot be open
-    Raises InvalidTableFormat if the file does not conform to the format
-    i.e, Marshal.from_channel fails
-*)
-
-
 let read_key_elem inch =
   try
     Some (Marshal.from_channel inch)
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index ee9fa35f1..c75648af2 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -1125,6 +1125,7 @@ let file_of_string filename s =
 
 
 exception CsdpInfeasible
+exception CsdpNotFound
 
 let run_csdp dbg string_problem =
   let input_file = Filename.temp_file "sos" ".dat-s" in
@@ -1136,8 +1137,7 @@ let run_csdp dbg string_problem =
   let rv = Sys.command("cd "^temp_path^"; csdp "^input_file^" "^output_file^
                        (if dbg then "" else "> /dev/null")) in
     if rv = 1 or rv = 2 then raise CsdpInfeasible; 
-  if rv = 127 then
-     (print_string "csdp not found, exiting..."; exit 1);
+  if rv = 127 then raise CsdpNotFound ;
   if rv <> 0 & rv <> 3 (* reduced accuracy *) then
      failwith("csdp: error "^string_of_int rv);
   let string_result = string_of_file output_file in
@@ -1474,8 +1474,9 @@ let sdpa_of_blockproblem comment nblocks blocksizes obj mats =
 let csdp_blocks nblocks blocksizes obj mats =
   let string_problem = sdpa_of_blockproblem "" nblocks blocksizes obj mats in
   try parse_csdpoutput (run_csdp !debugging string_problem)
-  with CsdpInfeasible -> failwith "csdp: Problem is infeasible"
-
+  with 
+    | CsdpInfeasible -> failwith "csdp: Problem is infeasible"
+   
 (* ------------------------------------------------------------------------- *)
 (* 3D versions of matrix operations to consider blocks separately.           *)
 (* ------------------------------------------------------------------------- *)