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/extraction/extract_env.ml | 18 +++++++++++------- plugins/extraction/extraction.ml | 4 ++-- plugins/extraction/haskell.ml | 4 +++- plugins/extraction/mlutil.ml | 4 ++-- plugins/extraction/ocaml.ml | 5 +++-- plugins/extraction/table.ml | 6 +++--- 6 files changed, 24 insertions(+), 17 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 6aa47eff..b7ee3c1a 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -397,8 +397,10 @@ let mono_filename f = in let id = if lang () <> Haskell then default_id - else try id_of_string (Filename.basename f) - with _ -> error "Extraction: provided filename is not a valid identifier" + else + try id_of_string (Filename.basename f) + with e when Errors.noncritical e -> + error "Extraction: provided filename is not a valid identifier" in Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id @@ -473,8 +475,8 @@ let print_structure_to_file (fn,si,mo) dry struc = msg_with ft (d.preamble mo opened unsafe_needs); msg_with ft (d.pp_struct struc); Option.iter close_out cout; - with e -> - Option.iter close_out cout; raise e + with reraise -> + Option.iter close_out cout; raise reraise end; if not dry then Option.iter info_file fn; (* Now, let's print the signature *) @@ -487,8 +489,8 @@ let print_structure_to_file (fn,si,mo) dry struc = msg_with ft (d.sig_preamble mo opened unsafe_needs); msg_with ft (d.pp_sig (signature_of_structure struc)); close_out cout; - with e -> - close_out cout; raise e + with reraise -> + close_out cout; raise reraise end; info_file si) (if dry then None else si); @@ -527,7 +529,9 @@ let rec locate_ref = function | r::l -> let q = snd (qualid_of_reference r) in let mpo = try Some (Nametab.locate_module q) with Not_found -> None - and ro = try Some (Smartlocate.global_with_alias r) with _ -> None + and ro = + try Some (Smartlocate.global_with_alias r) + with e when Errors.noncritical e -> None in match mpo, ro with | None, None -> Nametab.error_global_not_found q diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0a17453c..e5357336 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -149,7 +149,7 @@ let rec handle_exn r n fn_name = function (fun i -> assert ((0 < i) && (i <= n)); MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i))) - with _ -> MLexn s) + with e when Errors.noncritical e -> MLexn s) | a -> ast_map (handle_exn r n fn_name) a (*S Management of type variable contexts. *) @@ -683,7 +683,7 @@ and extract_cst_app env mle mlt kn args = let l,l' = list_chop (projection_arity (ConstRef kn)) mla in if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla - with _ -> mla + with e when Errors.noncritical e -> mla in (* For strict languages, purely logical signatures with at least one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 6c78b533..b6fc5ac8 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -81,7 +81,9 @@ let kn_sig = let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false - | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) + | Tvar i -> + (try pr_id (List.nth vl (pred i)) + with e when Errors.noncritical e -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r | Tglob (IndRef(kn,0),l) when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" -> diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a38b303f..d0bf387a 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -879,7 +879,7 @@ let is_program_branch = function (try ignore (int_of_string (String.sub s n (String.length s - n))); String.sub s 0 n = br - with _ -> false) + with e when Errors.noncritical e -> false) | Tmp _ | Dummy -> false let expand_linear_let o id e = @@ -1312,7 +1312,7 @@ let inline_test r t = let c = match r with ConstRef c -> c | _ -> assert false in let has_body = try constant_has_body (Global.lookup_constant c) - with _ -> false + with e when Errors.noncritical e -> false in has_body && (let t1 = eta_red t in diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 289b2a1d..4e8d8145 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -119,7 +119,8 @@ let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ | Taxiom -> assert false | Tvar i -> (try pp_tvar (List.nth vl (pred i)) - with _ -> (str "'a" ++ int i)) + with e when Errors.noncritical e -> + (str "'a" ++ int i)) | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r @@ -188,7 +189,7 @@ let rec pp_expr par env args = let args = list_skipn (projection_arity r) args in let record = List.hd args in pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) - with _ -> apply (pp_global Term r)) + with e when Errors.noncritical e -> apply (pp_global Term r)) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index e0a6e843..497ddf03 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -255,7 +255,7 @@ let safe_basename_of_global r = let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) - with _ -> string_of_id (safe_basename_of_global r) + with e when Errors.noncritical e -> string_of_id (safe_basename_of_global r) let safe_pr_global r = str (string_of_global r) @@ -263,7 +263,7 @@ let safe_pr_global r = str (string_of_global r) let safe_pr_long_global r = try Printer.pr_global r - with _ -> match r with + with e when Errors.noncritical e -> match r with | ConstRef kn -> let mp,_,l = repr_con kn in str ((string_of_mp mp)^"."^(string_of_label l)) @@ -452,7 +452,7 @@ let my_bool_option name initval = (*s Extraction AccessOpaque *) -let access_opaque = my_bool_option "AccessOpaque" false +let access_opaque = my_bool_option "AccessOpaque" true (*s Extraction AutoInline *) -- cgit v1.2.3