From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- tools/coqdep_common.ml | 155 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 103 insertions(+), 52 deletions(-) (limited to 'tools/coqdep_common.ml') diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 2e6a15ce..c1111375 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -17,6 +17,11 @@ open Unix options (see for instance [option_natdynlk] below). *) +module StrSet = Set.Make(String) + +module StrList = struct type t = string list let compare = compare end +module StrListMap = Map.Make(StrList) + let stderr = Pervasives.stderr let stdout = Pervasives.stdout @@ -26,8 +31,8 @@ let option_natdynlk = ref true let option_boot = ref false let option_mldep = ref None -let norec_dirs = ref ([] : string list) -let norec_dirnames = ref ["CVS"; "_darcs"] +let norec_dirs = ref StrSet.empty +let norec_dirnames = ref (List.fold_right StrSet.add ["CVS"; "_darcs"] StrSet.empty) let suffixe = ref ".vo" @@ -86,18 +91,18 @@ let vAccu = ref ([] : (string * string) list) let addQueue q v = q := v :: !q -let safe_hash_add cmp clq q (k,v) = +let safe_hash_add cmp clq q (k, (v, b)) = try - let v2 = Hashtbl.find q k in + let (v2, _) = Hashtbl.find q k in if not (cmp v v2) then - let rec add_clash = function - (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl - | cl::cltl -> cl::add_clash cltl - | [] -> [(k,[v;v2])] in - clq := add_clash !clq; + let nv = + try v :: StrListMap.find k !clq + with Not_found -> [v; v2] + in + clq := StrListMap.add k nv !clq; (* overwrite previous bindings, as coqc does *) - Hashtbl.add q k v - with Not_found -> Hashtbl.add q k v + Hashtbl.add q k (v, b) + with Not_found -> Hashtbl.add q k (v, b) (** Files found in the loadpaths. For the ML files, the string is the basename without extension. @@ -126,20 +131,53 @@ let add_mli_known, iter_mli_known, search_mli_known = mkknown () let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () -let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t) +let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t) +(** The associated boolean is true if this is a root path. *) let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t) -let clash_v = ref ([]: (string list * string list) list) +let get_prefix p l = + let rec drop_prefix_rec = function + | (h1::tp, h2::tl) when h1 = h2 -> drop_prefix_rec (tp,tl) + | ([], tl) -> Some tl + | _ -> None + in + drop_prefix_rec (p, l) + +let search_table (type r) is_root table ?from s = match from with +| None -> Hashtbl.find table s +| Some from -> + 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 (M.Found binding) + in + try Hashtbl.iter iter table; raise Not_found + with M.Found s -> s + +let search_v_known ?from s = + 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 (StrListMap.empty : string list StrListMap.t) let error_cannot_parse s (i,j) = Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; exit 1 let warning_module_notfound f s = - eprintf "*** Warning: in file %s, library " f; - eprintf "%s.v is required and has not been found in the loadpath!\n" - (String.concat "." s); - flush stderr + eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!" + f (String.concat "." s) let warning_notfound f s = eprintf "*** Warning: in file %s, the file " f; @@ -152,7 +190,7 @@ let warning_declare f s = flush stderr let warning_clash file dir = - match List.assoc dir !clash_v with + match StrListMap.find dir !clash_v with (f1::f2::fl) -> let f = Filename.basename f1 in let d1 = Filename.dirname f1 in @@ -165,9 +203,11 @@ let warning_clash file dir = eprintf "%s and %s; used the latter)\n" d2 d1 | _ -> assert false -let safe_assoc verbose file k = - if verbose && List.mem_assoc k !clash_v then warning_clash file k; - Hashtbl.find vKnown k +let safe_assoc from verbose file k = + if verbose && StrListMap.mem k !clash_v then warning_clash file k; + match search_v_known ?from k with + | None -> raise Not_found + | Some path -> path let absolute_dir dir = let current = Sys.getcwd () in @@ -222,16 +262,16 @@ let autotraite_fichier_ML md ext = try let chan = open_in (md ^ ext) in let buf = Lexing.from_channel chan in - let deja_vu = ref [md] in + let deja_vu = ref (StrSet.singleton md) in let a_faire = ref "" in let a_faire_opt = ref "" in begin try while true do let (Use_module str) = caml_action buf in - if List.mem str !deja_vu then + if StrSet.mem str !deja_vu then () else begin - addQueue deja_vu str; + deja_vu := StrSet.add str !deja_vu; let byte,opt = depend_ML str in a_faire := !a_faire ^ byte; a_faire_opt := !a_faire_opt ^ opt @@ -307,38 +347,39 @@ let canonize f = | (f,_) :: _ -> escape f | _ -> escape f +module VData = struct + type t = string list option * string list + let compare = Pervasives.compare +end + +module VCache = Set.Make(VData) + let rec traite_fichier_Coq suffixe verbose f = try let chan = open_in f in let buf = Lexing.from_channel chan in - let deja_vu_v = ref ([]: string list list) - and deja_vu_ml = ref ([] : string list) in + let deja_vu_v = ref VCache.empty in + let deja_vu_ml = ref StrSet.empty in try while true do let tok = coq_action buf in match tok with - | Require strl -> + | Require (from, strl) -> List.iter (fun str -> - if not (List.mem str !deja_vu_v) then begin - addQueue deja_vu_v str; + if not (VCache.mem (from, str) !deja_vu_v) then begin + deja_vu_v := VCache.add (from, str) !deja_vu_v; try - let file_str = safe_assoc verbose f str in + 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 + let str = + match from with + | None -> str + | Some pth -> pth @ str + in warning_module_notfound f str end) strl - | RequireString s -> - let str = Filename.basename s in - if not (List.mem [str] !deja_vu_v) then begin - addQueue deja_vu_v [str]; - try - let file_str = Hashtbl.find vKnown [str] in - printf " %s%s" (canonize file_str) suffixe - with Not_found -> - if not (Hashtbl.mem coqlibKnown [str]) then - warning_notfound f s - end | Declare sl -> let declare suff dir s = let base = file_name s dir in @@ -347,8 +388,8 @@ let rec traite_fichier_Coq suffixe verbose f = in let decl str = let s = basename_noext str in - if not (List.mem s !deja_vu_ml) then begin - addQueue deja_vu_ml s; + if not (StrSet.mem s !deja_vu_ml) then begin + deja_vu_ml := StrSet.add s !deja_vu_ml; match search_mllib_known s with | Some mldir -> declare ".cma" mldir s | None -> @@ -362,10 +403,10 @@ let rec traite_fichier_Coq suffixe verbose f = in List.iter decl sl | Load str -> let str = Filename.basename str in - if not (List.mem [str] !deja_vu_v) then begin - addQueue deja_vu_v [str]; + if not (VCache.mem (None, [str]) !deja_vu_v) then begin + deja_vu_v := VCache.add (None, [str]) !deja_vu_v; try - let file_str = Hashtbl.find vKnown [str] in + let (file_str, _) = Hashtbl.find vKnown [str] in let canon = canonize file_str in printf " %s.v" canon; traite_fichier_Coq suffixe true (canon ^ ".v") @@ -449,14 +490,24 @@ 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") -> let name = log_dir@[basename] in let file = phys_dir//basename in - let paths = if recur then suffixes name else [name] in - List.iter - (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths + let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in + if recur then + let paths = List.tl (suffixes name) in + let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in + List.iter iter paths | (basename,".vo") when not(!option_boot) -> let name = log_dir@[basename] in let paths = if recur then suffixes name else [name] in @@ -477,9 +528,9 @@ let rec add_directory recur add_file phys_dir log_dir = let phys_f = if phys_dir = "." then f else phys_dir//f in match try (stat phys_f).st_kind with _ -> S_BLK with | S_DIR when recur -> - if List.mem f !norec_dirnames then () + if StrSet.mem f !norec_dirnames then () else - if List.mem phys_f !norec_dirs then () + if StrSet.mem phys_f !norec_dirs then () else add_directory recur add_file phys_f (log_dir@[f]) | S_REG -> add_file phys_dir log_dir f -- cgit v1.2.3