Using maps and sets instead of lists in coqdep.

The quadratic behaviour of list searching probably appears with small
enough samples. With the advent of usable libraries in Coq, and thus many
possible dependencies, better be safe than sorry.

1 files changed, 35 insertions, 23 deletions

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index d88455852..8e2159745 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