diff options
-rw-r--r-- | library/nametab.mli | 6 | ||||
-rw-r--r-- | plugins/extraction/extract_env.ml | 10 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 4 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 12 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 4 |
5 files changed, 19 insertions, 17 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index d561735fd..43c174f1b 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -151,13 +151,15 @@ val path_of_tactic : ltac_constant -> full_path val dirpath_of_global : global_reference -> DirPath.t val basename_of_global : global_reference -> Id.t -(** Printing of global references using names as short as possible *) +(** Printing of global references using names as short as possible. + @raise Not_found when the reference is not in the global tables. *) val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds (** The [shortest_qualid] functions given an object with [user_name] Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and - Coq.A.B.x that denotes the same object. *) + Coq.A.B.x that denotes the same object. + @raise Not_found for unknown objects. *) val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index ae60259e9..358fe2d01 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -402,8 +402,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 UserError _ -> + error "Extraction: provided filename is not a valid identifier" in Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id @@ -541,7 +543,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 Not_found | UserError _ -> 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 035f8e3bb..3ec9038c6 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -144,11 +144,11 @@ let sign_with_implicits r s nb_params = let rec handle_exn r n fn_name = function | MLexn s -> - (try Scanf.sscanf s "UNBOUND %d" + (try Scanf.sscanf s "UNBOUND %d%!" (fun i -> assert ((0 < i) && (i <= n)); MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i))) - with _ -> MLexn s) + with Scanf.Scan_failure _ | End_of_file -> MLexn s) | a -> ast_map (handle_exn r n fn_name) a (*S Management of type variable contexts. *) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 4407c6798..659ee4ec4 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -856,15 +856,11 @@ let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false Unfolding them leads to more natural code (and more dummy removal) *) let is_program_branch = function + | Tmp _ | Dummy -> false | Id id -> let s = Id.to_string id in - let br = "program_branch_" in - let n = String.length br in - (try - ignore (int_of_string (String.sub s n (String.length s - n))); - String.sub s 0 n = br - with _ -> false) - | Tmp _ | Dummy -> false + try Scanf.sscanf s "program_branch_%d%!" (fun _ -> true) + with Scanf.Scan_failure _ | End_of_file -> false let expand_linear_let o id e = o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e @@ -1297,7 +1293,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 Not_found -> false in has_body && (let t1 = eta_red t in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 17303d80c..b35b5fc5e 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 Id.Set.empty r) - with _ -> Id.to_string (safe_basename_of_global r) + with Not_found -> Id.to_string (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 Not_found -> match r with | ConstRef kn -> let mp,_,l = repr_con kn in str ((string_of_mp mp)^"."^(Label.to_string l)) |