diff options
-rw-r--r-- | tools/coqdep.ml | 8 | ||||
-rw-r--r-- | tools/coqdep_common.ml | 37 | ||||
-rw-r--r-- | tools/coqdep_common.mli | 2 |
3 files changed, 27 insertions, 20 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index ec8e983ec..99b6c7e06 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -36,14 +36,6 @@ let warning_mult suf iter = in iter check -let add_coqlib_known recur phys_dir log_dir f = - match get_extension f [".vo"] with - | (basename,".vo") -> - let name = log_dir@[basename] in - let paths = if recur then suffixes name else [name] in - List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths - | _ -> () - let sort () = let seen = Hashtbl.create 97 in let rec loop file = diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 0868c9e11..d88455852 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -138,24 +138,31 @@ let get_prefix p l = in drop_prefix_rec (p, l) -exception Found of string - -let search_v_known ?from s = match from with -| None -> fst (Hashtbl.find vKnown s) +let search_table (type r) is_root table ?from s = match from with +| None -> Hashtbl.find table s | Some from -> - let iter logpath (phys_dir, root) = - if root then match get_prefix from logpath with + let module M = struct exception Found of r end in + let iter logpath binding = + if is_root binding then match get_prefix from logpath with | None -> () | Some rem -> match get_prefix (List.rev s) (List.rev rem) with | None -> () - | Some _ -> raise (Found phys_dir) + | Some _ -> raise (M.Found binding) in - try Hashtbl.iter iter vKnown; raise Not_found - with Found s -> s + try Hashtbl.iter iter table; raise Not_found + with M.Found s -> s let search_v_known ?from s = - try Some (search_v_known ?from s) with Not_found -> None + let is_root (_, root) = root in + try + let (phys_dir, _) = search_table is_root vKnown ?from s in + Some phys_dir + with Not_found -> None + +let is_in_coqlib ?from s = + let is_root _ = true in + try search_table is_root coqlibKnown ?from s; true with Not_found -> false let clash_v = ref ([]: (string list * string list) list) @@ -353,7 +360,7 @@ let rec traite_fichier_Coq suffixe verbose f = let file_str = safe_assoc from verbose f str in printf " %s%s" (canonize file_str) suffixe with Not_found -> - if verbose && not (Hashtbl.mem coqlibKnown str) then + if verbose && not (is_in_coqlib ?from str) then warning_module_notfound f str end) strl | Declare sl -> @@ -466,6 +473,14 @@ let add_caml_known phys_dir _ f = | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () +let add_coqlib_known recur phys_dir log_dir f = + match get_extension f [".vo"] with + | (basename,".vo") -> + let name = log_dir@[basename] in + let paths = if recur then suffixes name else [name] in + List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths + | _ -> () + let add_known recur phys_dir log_dir f = match get_extension f [".v";".vo"] with | (basename,".v") -> diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 23619d1e6..5e5c4740c 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -32,7 +32,6 @@ val search_mli_known : string -> dir option val add_mllib_known : string -> dir -> string -> unit val search_mllib_known : string -> dir option val search_v_known : ?from:string list -> string list -> string option -val coqlibKnown : (string list, unit) Hashtbl.t val file_name : string -> string option -> string val escape : string -> string val canonize : string -> string @@ -40,6 +39,7 @@ val mL_dependencies : unit -> unit val coq_dependencies : unit -> unit val suffixes : 'a list -> 'a list list val add_known : bool -> string -> string list -> string -> unit +val add_coqlib_known : bool -> string -> string list -> string -> unit val add_caml_known : string -> string list -> string -> unit val add_directory : bool -> |