From 033fed4d6788be791bb1c980f3cddc10827d6318 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 13 Mar 2013 00:00:59 +0000 Subject: Restrict (try...with...) to avoid catching critical exn (part 15) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/indfun_common.ml | 43 +++++++++++++++++++---------------- plugins/funind/invfun.ml | 8 +++++-- plugins/funind/merge.ml | 4 ++-- plugins/funind/recdef.ml | 9 ++++---- plugins/micromega/csdpcert.ml | 6 ++--- plugins/micromega/mutils.ml | 32 +++++++++++++++++--------- plugins/micromega/persistent_cache.ml | 10 ++++---- plugins/nsatz/nsatz.ml4 | 2 +- plugins/nsatz/utile.ml | 7 +++--- plugins/omega/coq_omega.ml | 5 ++-- plugins/romega/const_omega.ml | 4 ++-- plugins/xml/cic2acic.ml | 2 +- plugins/xml/xmlcommand.ml | 2 +- 13 files changed, 77 insertions(+), 57 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 56660cd69..4d1cefe5a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -335,17 +335,25 @@ let discharge_Function (_,finfos) = } open Term + +let pr_ocst c = + Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) + let pr_info f_info = - str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ - str "function_constant_type := " ++ - (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++ - str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++ - str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++ - str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++ - str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++ - str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++ - str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++ - str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + str "function_constant := " ++ + Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ + str "function_constant_type := " ++ + (try + Printer.pr_lconstr + (Global.type_of_global (ConstRef f_info.function_constant)) + with e when Errors.noncritical e -> mt ()) ++ fnl () ++ + str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ + str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ + str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++ + str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ + str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ + str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ + str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = let l = Cmap.fold (fun k v acc -> v::acc) tb [] in @@ -486,22 +494,17 @@ exception Building_graph of exn exception Defining_principle of exn exception ToShow of exn -let init_constant dir s = - try - Coqlib.gen_constant "Function" dir s - with e -> raise (ToShow e) - let jmeq () = try - (Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq") - with e -> raise (ToShow e) + Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; + Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq" + with e when Errors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq_refl" - with e -> raise (ToShow e) + Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl" + with e when Errors.noncritical e -> raise (ToShow e) let h_intros l = tclMAP h_intro l diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index bb775d40a..16b1881f4 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -60,9 +60,13 @@ let observe strm = let do_observe_tac s tac g = - let goal = begin try (Printer.pr_goal g) with _ -> assert false end in + let goal = + try Printer.pr_goal g + with e when Errors.noncritical e -> assert false + in try - let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v + let v = tac g in + msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with reraise -> let e = Cerrors.process_vernac_interp_error reraise in msgnl (str "observation "++ s++str " raised exception " ++ diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 97512dd84..bf5eba63a 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -786,10 +786,10 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let params1 = try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) - with _ -> [] in + with e when Errors.noncritical e -> [] in let params2 = try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) - with _ -> [] in + with e when Errors.noncritical e -> [] in let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8a4cdc3c7..597233d01 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -423,7 +423,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info - with _ -> + with e when Errors.noncritical e -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) end | Lambda(n,t,b) -> @@ -431,7 +431,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info - with _ -> + with e when Errors.noncritical e -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) end | Case(ci,t,a,l) -> @@ -1240,8 +1240,9 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let name = match goal_name with | Some s -> s | None -> - try (add_suffix current_proof_name "_subproof") - with _ -> anomaly (Pp.str "open_new_goal with an unamed theorem") + try add_suffix current_proof_name "_subproof" + with e when Errors.noncritical e -> + anomaly (Pp.str "open_new_goal with an unamed theorem") in let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index f848591cc..6fd79f16b 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -148,7 +148,7 @@ let real_nonlinear_prover d l = S (Some proof) with | Sos_lib.TooDeep -> S None - | x -> F (Printexc.to_string x) + | any -> F (Printexc.to_string any) (* This is somewhat buggy, over Z, strict inequality vanish... *) let pure_sos l = @@ -172,7 +172,7 @@ let pure_sos l = S (Some proof) with (* | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *) - | x -> (* May be that could be refined *) S None + | any -> (* May be that could be refined *) S None @@ -201,7 +201,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/mutils.ml b/plugins/micromega/mutils.ml index 43cad05e9..0b98696c9 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 @@ -429,16 +429,26 @@ let command exe_path args vl = (fun () -> match status with | 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)) - 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)) + let inch = Unix.in_channel_of_descr stdout_read in + begin + try Marshal.from_channel inch + with any -> + failwith + (Printf.sprintf "command \"%s\" exited %s" exe_path + (Printexc.to_string any)) + 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 any -> ()) + [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 cb7a9280d..39a1b82b0 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 Errors.noncritical e -> 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 Errors.noncritical e -> () ) ; unlock out ; { outch = outch ; diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 7b42fc5ba..e31eba4e0 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -54,7 +54,7 @@ module BigInt = struct let to_int x = int_of_big_int x let hash x = try (int_of_big_int x) - with _-> 1 + with Failure _ -> 1 let puis = power_big_int_positive_int (* a et b positifs, résultat positif *) diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index d647b14ed..638242462 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -51,7 +51,7 @@ let facteurs_liste div constant lp = if not (constant r) then l1:=r::(!l1) else p_dans_lmin:=true) - with _ -> ()) + with e when Errors.noncritical e -> ()) lmin; if !p_dans_lmin then factor lmin lp1 @@ -62,7 +62,8 @@ let facteurs_liste div constant lp = List.iter (fun q -> try (let r = div q p in if not (constant r) then l1:=r::(!l1)) - with _ -> lmin1:=q::(!lmin1)) + with e when Errors.noncritical e -> + lmin1:=q::(!lmin1)) lmin; factor (List.rev (p::(!lmin1))) !l1) (* au moins un q de lmin divise p non trivialement *) @@ -92,7 +93,7 @@ let factorise_tableau div zero c f l1 = li:=j::(!li); r:=rr; done) - with _ -> ()) + with e when Errors.noncritical e -> ()) l1; res.(i)<-(!r,!li)) f; diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index c4961654d..f98aba0a8 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -874,7 +874,7 @@ let rec transform p t = try let v,th,_ = find_constr t' in [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - with _ -> + with e when Errors.noncritical e -> let v = new_identifier_var () and th = new_identifier () in hide_constr t' v th isnat; @@ -913,7 +913,8 @@ let rec transform p t = | _ -> default false t end | Kapp((Zpos|Zneg|Z0),_) -> - (try ([],Oz(recognize_number t)) with _ -> default false t) + (try ([],Oz(recognize_number t)) + with e when Errors.noncritical e -> default false t) | Kvar s -> [],Oatom s | Kapp(Zopp,[t]) -> let tac,t' = transform (P_APP 1 :: p) t in diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index d23a07ba6..75fe49bcf 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -334,7 +334,7 @@ let parse_term t = | Kapp("Z.succ",[t]) -> Tsucc t | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (try Tnum (recognize t) with _ -> Tother) + (try Tnum (recognize t) with e when Errors.noncritical e -> Tother) | _ -> Tother with e when Logic.catchable_exception e -> Tother @@ -356,6 +356,6 @@ let is_scalar t = | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true | _ -> false in - try aux t with _ -> false + try aux t with e when Errors.noncritical e -> false end diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 5f4add47a..98c485dba 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -351,7 +351,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids if computeinnertypes then try Acic.CicHash.find terms_to_types tt -with _ -> +with e when Errors.noncritical e -> (*CSC: Warning: it really happens, for example in Ring_theory!!! *) Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false else diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 4d9541ebc..a34d4a682 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -81,7 +81,7 @@ let rec join_dirs cwd = | he::tail -> (try Unix.mkdir cwd 0o775 - with _ -> () (* Let's ignore the errors on mkdir *) + with e when Errors.noncritical e -> () (* ignore the errors on mkdir *) ) ; let newcwd = cwd ^ "/" ^ he in join_dirs newcwd tail -- cgit v1.2.3