Permalink
Browse files

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
  • Loading branch information...
1 parent 8d70a84 commit 033fed4d6788be791bb1c980f3cddc10827d6318 letouzey committed Mar 13, 2013
@@ -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
@@ -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 " ++
@@ -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
@@ -423,15 +423,15 @@ 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) ->
begin
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
@@ -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)
;;
@@ -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 *)
@@ -82,18 +82,18 @@ 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 =
try
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 ;
@@ -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 *)
@@ -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;
@@ -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
@@ -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
@@ -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
@@ -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
@@ -50,7 +50,7 @@ let rec get_extension f = function
let basename_noext filename =
let fn = Filename.basename filename in
- try Filename.chop_extension fn with _ -> fn
+ try Filename.chop_extension fn with Invalid_argument _ -> fn
(** ML Files specified on the command line. In the entries:
- the first string is the basename of the file, without extension nor

0 comments on commit 033fed4

Please sign in to comment.