From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- plugins/micromega/certificate.ml | 7 ++++--- plugins/micromega/coq_micromega.ml | 24 +++++++++++++++--------- plugins/micromega/csdpcert.ml | 6 +++--- plugins/micromega/mfourier.ml | 3 ++- plugins/micromega/mutils.ml | 12 +++++++----- plugins/micromega/persistent_cache.ml | 10 +++++----- 6 files changed, 36 insertions(+), 26 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 25579a87..a5b0da9c 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -331,7 +331,7 @@ let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = | Inr _ -> None | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) (* should not use rats_to_ints *) - with x -> + with x when Errors.noncritical x -> if debug then (Printf.printf "raw certificate %s" (Printexc.to_string x); flush stdout) ; @@ -377,8 +377,9 @@ let linear_prover n_spec l = let linear_prover n_spec l = - try linear_prover n_spec l with - x -> (print_string (Printexc.to_string x); None) + try linear_prover n_spec l + with x when x <> Sys.Break -> + (print_string (Printexc.to_string x); None) let linear_prover_with_cert spec l = match linear_prover spec l with diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 2020447f..ff08aeb3 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -937,7 +937,8 @@ struct let (expr,env) = parse_expr env args.(0) in let power = (parse_exp expr args.(1)) in (power , env) - with _ -> (* if the exponent is a variable *) + with e when e <> Sys.Break -> + (* if the exponent is a variable *) let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) end | Ukn s -> @@ -1112,8 +1113,12 @@ struct let parse_formula parse_atom env tg term = - let parse_atom env tg t = try let (at,env) = parse_atom env t in - (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in + let parse_atom env tg t = + try + let (at,env) = parse_atom env t in + (A(at,tg,t), env,Tag.next tg) + with e when e <> Sys.Break -> (X(t),env,tg) + in let rec xparse_formula env tg term = match kind_of_term term with @@ -1189,7 +1194,8 @@ let same_proof sg cl1 cl2 = let rec xsame_proof sg = match sg with | [] -> true - | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false) + | n::sg -> + (try List.nth cl1 n = List.nth cl2 n with e when e <> Sys.Break -> false) && (xsame_proof sg ) in xsame_proof sg @@ -1253,7 +1259,7 @@ let btree_of_array typ a = let btree_of_array typ a = try btree_of_array typ a - with x -> + with x when x <> Sys.Break -> failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x)) let dump_varmap typ env = @@ -1322,7 +1328,7 @@ let rec parse_hyps parse_arith env tg hyps = try let (c,env,tg) = parse_formula parse_arith env tg t in ((i,c)::lhyps, env,tg) - with _ -> (lhyps,env,tg) + with e when e <> Sys.Break -> (lhyps,env,tg) (*(if debug then Printf.printf "parse_arith : %s\n" x);*) @@ -1466,7 +1472,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = (pp_ml_list prover.pp_f) (List.map fst new_cl) ; flush stdout end ; *) - let res = try prover.compact prf remap with x -> + let res = try prover.compact prf remap with x when x <> Sys.Break -> if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; (* This should not happen -- this is the recovery plan... *) match prover.prover (List.map fst new_cl) with @@ -2031,13 +2037,13 @@ let xlia gl = try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ linear_Z ] gl - with z -> (*Printexc.print_backtrace stdout ;*) raise z + with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let xnlia gl = try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ nlinear_Z ] gl - with z -> (*Printexc.print_backtrace stdout ;*) raise z + with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index dfda5984..0f26575c 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -150,7 +150,7 @@ let real_nonlinear_prover d l = S (Some proof) with | Sos_lib.TooDeep -> S None - | x -> F (Printexc.to_string x) + | x when x <> Sys.Break -> F (Printexc.to_string x) (* This is somewhat buggy, over Z, strict inequality vanish... *) let pure_sos l = @@ -174,7 +174,7 @@ let pure_sos l = S (Some proof) with (* | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *) - | x -> (* May be that could be refined *) S None + | x when x <> Sys.Break -> (* May be that could be refined *) S None @@ -203,7 +203,7 @@ let main () = Marshal.to_channel chan (cert:csdp_certificate) [] ; flush chan ; exit 0 - with x -> (Printf.fprintf chan "error %s" (Printexc.to_string x) ; exit 1) + with any -> (Printf.fprintf chan "error %s" (Printexc.to_string any) ; exit 1) ;; diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index d9201722..6effa4c4 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -728,7 +728,8 @@ struct try Some (bound_of_variable IMap.empty fresh s.sys) with - x -> Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None + x when x <> Sys.Break -> + Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None let find_point cstrs = diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index ccbf0406..3129e54d 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -29,10 +29,10 @@ let finally f rst = try let res = f () in rst () ; res - with x -> + with reraise -> (try rst () - with _ -> raise x - ); raise x + with any -> raise reraise + ); raise reraise let map_option f x = match x with @@ -431,14 +431,16 @@ let command exe_path args vl = | Unix.WEXITED 0 -> let inch = Unix.in_channel_of_descr stdout_read in begin try Marshal.from_channel inch - with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) + with x when x <> Sys.Break -> + failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) end | Unix.WEXITED i -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) | Unix.WSTOPPED i -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) (* Cleanup *) (fun () -> - List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write]) + List.iter (fun x -> try Unix.close x with e when e <> Sys.Break -> ()) + [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write]) (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index cb7a9280..6d1a2927 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -82,10 +82,10 @@ let finally f rst = try let res = f () in rst () ; res - with x -> + with reraise -> (try rst () - with _ -> raise x - ); raise x + with any -> raise reraise + ); raise reraise let read_key_elem inch = @@ -93,7 +93,7 @@ let read_key_elem inch = Some (Marshal.from_channel inch) with | End_of_file -> None - | _ -> raise InvalidTableFormat + | e when e <> Sys.Break -> raise InvalidTableFormat (** In win32, it seems that we should unlock the exact zone that has been locked, and not the whole file *) @@ -151,7 +151,7 @@ let open_in f = Table.iter (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl; flush outch ; - with _ -> () ) + with e when e <> Sys.Break -> () ) ; unlock out ; { outch = outch ; -- cgit v1.2.3