Imported Upstream version 8.5~beta3+dfsg

1 files changed, 29 insertions, 35 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2e0cce6e..110d3060 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 =
@@ -55,13 +47,13 @@ let sort () =
       try
 	while true do
 	  match coq_action lb with
-	    | Require sl ->
+	    | Require (from, sl) ->
 		List.iter
 		  (fun s ->
-		    try loop (Hashtbl.find vKnown s)
-		    with Not_found -> ())
+                    match search_v_known ?from s with
+                    | None -> ()
+                    | Some f -> loop f)
 		sl
-	    | RequireString s -> loop s
 	    | _ -> ()
 	done
       with Fin_fichier ->
@@ -297,18 +289,24 @@ 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 list)
-  and deja_vu_ml = ref ([] : string list) in
-  let mark_v_done acc str =
-    let seen = List.mem str !deja_vu_v 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 = VCache.mem (from, str) !deja_vu_v in
     if not seen then
-      let () = addQueue deja_vu_v str in
-      try
-        let file_str = Hashtbl.find vKnown str in
-        (canonize file_str, !suffixe) :: acc
-      with Not_found -> acc
+      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
     else acc
   in
   let rec loop acc =
@@ -317,11 +315,8 @@ let treat_coq_file chan =
     | None -> acc
     | Some action ->
       let acc = match action with
-      | Require strl ->
-        List.fold_left mark_v_done acc strl
-      | RequireString s ->
-        let str = Filename.basename s in
-        mark_v_done acc [str]
+      | Require (from, strl) ->
+        List.fold_left (fun accu v -> mark_v_done from accu v) acc strl
       | Declare sl ->
         let declare suff dir s =
           let base = file_name s dir in
@@ -330,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 ->
@@ -343,13 +338,12 @@ let treat_coq_file chan =
         List.fold_left decl acc sl
       | Load str ->
         let str = Filename.basename str in
-        let seen = List.mem [str] !deja_vu_v in
+        let seen = VCache.mem (None, [str]) !deja_vu_v in
         if not seen then
-          let () = addQueue deja_vu_v [str] in
-          try
-            let file_str = Hashtbl.find vKnown [str] in
-            (canonize file_str, ".v") :: acc
-          with Not_found -> acc
+          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
         else acc
       | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *)
       in
@@ -461,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 ()