Imported Upstream version 8.5~beta3+dfsg

1 files changed, 103 insertions, 52 deletions

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