aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tools/coqdep.ml25
-rw-r--r--tools/coqdep_boot.ml2
-rw-r--r--tools/coqdep_common.ml58
-rw-r--r--tools/coqdep_common.mli6
4 files changed, 56 insertions, 35 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 99b6c7e06f..110d306022 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -289,14 +289,21 @@ struct
module DAG = DAG(struct type t = string let compare = compare end)
(** TODO: we should share this code with Coqdep_common *)
+module VData = struct
+ type t = string list option * string list
+ let compare = Pervasives.compare
+end
+
+module VCache = Set.Make(VData)
+
let treat_coq_file chan =
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
let mark_v_done from acc str =
- let seen = List.mem (from, str) !deja_vu_v in
+ let seen = VCache.mem (from, str) !deja_vu_v in
if not seen then
- let () = addQueue deja_vu_v (from, str) in
+ let () = deja_vu_v := VCache.add (from, str) !deja_vu_v in
match search_v_known ?from str with
| None -> acc
| Some file_str -> (canonize file_str, !suffixe) :: acc
@@ -318,8 +325,8 @@ let treat_coq_file chan =
in
let decl acc str =
let s = basename_noext str in
- if not (List.mem s !deja_vu_ml) then
- let () = addQueue deja_vu_ml s in
+ if not (StrSet.mem s !deja_vu_ml) then
+ let () = deja_vu_ml := StrSet.add s !deja_vu_ml in
match search_mllib_known s with
| Some mldir -> (declare ".cma" mldir s) :: acc
| None ->
@@ -331,9 +338,9 @@ let treat_coq_file chan =
List.fold_left decl acc sl
| Load str ->
let str = Filename.basename str in
- let seen = List.mem (None, [str]) !deja_vu_v in
+ let seen = VCache.mem (None, [str]) !deja_vu_v in
if not seen then
- let () = addQueue deja_vu_v (None, [str]) in
+ let () = deja_vu_v := VCache.add (None, [str]) !deja_vu_v in
match search_v_known [str] with
| None -> acc
| Some file_str -> (canonize file_str, ".v") :: acc
@@ -448,7 +455,7 @@ let rec parse = function
| "-R" :: ([] | [_]) -> usage ()
| "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
| "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
- | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll
+ | "-exclude-dir" :: r :: ll -> norec_dirnames := StrSet.add r !norec_dirnames; parse ll
| "-exclude-dir" :: [] -> usage ()
| "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
| "-coqlib" :: [] -> usage ()
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index bc3435a644..2d5fd36a63 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -25,7 +25,7 @@ let rec parse = function
(* To solve conflict (e.g. same filename in kernel and checker)
we allow to state an explicit order *)
add_caml_dir r;
- norec_dirs:=r::!norec_dirs;
+ norec_dirs := StrSet.add r !norec_dirs;
parse ll
| f :: ll -> treat_file None f; parse ll
| [] -> ()
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
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 5e5c4740c6..d610a0558d 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -6,13 +6,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+module StrSet : Set.S with type elt = string
+
val option_c : bool ref
val option_noglob : bool ref
val option_boot : bool ref
val option_natdynlk : bool ref
val option_mldep : string option ref
-val norec_dirs : string list ref
-val norec_dirnames : string list ref
+val norec_dirs : StrSet.t ref
+val norec_dirnames : StrSet.t ref
val suffixe : string ref
type dir = string option
val ( // ) : string -> string -> string
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:19:15 +0000