diff options
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 58 |
1 files changed, 35 insertions, 23 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index d884558527..8e2159745d 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" @@ -90,11 +95,11 @@ let safe_hash_add cmp clq q (k, (v, b)) = try 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, b) with Not_found -> Hashtbl.add q k (v, b) @@ -164,7 +169,7 @@ 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) +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; @@ -185,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 @@ -199,7 +204,7 @@ let warning_clash file dir = | _ -> assert false let safe_assoc from verbose file k = - if verbose && List.mem_assoc k !clash_v then warning_clash 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 @@ -257,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 @@ -342,20 +347,27 @@ 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 option * 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 (from, strl) -> List.iter (fun str -> - if not (List.mem (from, str) !deja_vu_v) then begin - addQueue deja_vu_v (from, 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 from verbose f str in printf " %s%s" (canonize file_str) suffixe @@ -371,8 +383,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 -> @@ -386,8 +398,8 @@ 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 (None, [str]) !deja_vu_v) then begin - addQueue deja_vu_v (None, [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 canon = canonize file_str in @@ -511,9 +523,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 |