Lissage de la gestion des chemins de chargement de fichiers :

- Option -R fait maintenant des Import à tous les niveaux de la
  hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche.
- Option -I rend maintenant possible l'accès aux sous-répertoires via
  les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il
  rend récursivement visibles les noms non qualifiés.
- Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir.
- Ajout option -exclude-dir pour exclure certains sous-répertoires de
  la descente récursive de -R.
- Amélioration message de localisation pour fichiers venant d'un "state".
- Adaptation du checker (et ajout du test check_coq_overwriting qui
  semblait involontairement oublié dans l'option -R).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 81 insertions, 38 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index dfa0fb82d..04ab34baa 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -89,6 +89,8 @@ let drop_dirpath_prefix d1 d2 =
   let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in
     make_dirpath (List.rev d)
 
+let append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1)
+
 (* To know how qualified a name should be to be understood in the current env*)
 let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
 
diff --git a/library/libnames.mli b/library/libnames.mli
index fe5033d73..890a442e3 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -59,6 +59,7 @@ val chop_dirpath : int -> dir_path -> dir_path * dir_path
 val drop_dirpath_prefix : dir_path -> dir_path -> dir_path
 val extract_dirpath_prefix : int -> dir_path -> dir_path
 val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+val append_dirpath : dir_path -> dir_path -> dir_path
 
 module Dirset : Set.S with type elt = dir_path
 module Dirmap : Map.S with type key = dir_path
diff --git a/library/library.ml b/library/library.ml
index 272f01f7d..b17be690a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -24,9 +24,9 @@ open Nametab
 
 type logical_path = dir_path
 
-let load_paths = ref ([],[] : System.physical_path list * logical_path list)
+let load_paths = ref ([] : (System.physical_path * logical_path * bool) list)
 
-let get_load_paths () = fst !load_paths
+let get_load_paths () = List.map pi1 !load_paths
 
 (* Hints to partially detects if two paths refer to the same repertory *)
 let rec remove_path_dot p = 
@@ -56,12 +56,12 @@ let canonical_path_name p =
     (* We give up to find a canonical name and just simplify it... *)
     strip_path p
 
-let find_logical_path phys_dir = 
+let find_logical_path phys_dir =
   let phys_dir = canonical_path_name phys_dir in
-  match list_filter2 (fun p d -> p = phys_dir) !load_paths with
-  | _,[dir] -> dir
-  | _,[] -> Nameops.default_root_prefix
-  | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
+  match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with
+  | [_,dir,_] -> dir
+  | [] -> Nameops.default_root_prefix
+  | l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
 let is_in_load_paths phys_dir =
   let dir = canonical_path_name phys_dir in
@@ -70,12 +70,12 @@ let is_in_load_paths phys_dir =
     List.exists check_p lp 
 
 let remove_load_path dir =
-  load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
+  load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
 
-let add_load_path (phys_path,coq_path) =
+let add_load_path isroot (phys_path,coq_path) =
   let phys_path = canonical_path_name phys_path in
-    match list_filter2 (fun p d -> p = phys_path) !load_paths with
-      | _,[dir] ->
+    match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
+      | [_,dir,_] ->
 	  if coq_path <> dir 
             (* If this is not the default -I . to coqtop *)
             && not
@@ -90,18 +90,54 @@ let add_load_path (phys_path,coq_path) =
 		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
 		   pr_dirpath coq_path);
 	      remove_load_path phys_path;
-	      load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+	      load_paths := (phys_path,coq_path,isroot) :: !load_paths;
 	    end
-      | _,[] ->
-	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+      | [] ->
+	  load_paths := (phys_path,coq_path,isroot) :: !load_paths;
       | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
 let physical_paths (dp,lp) = dp
 
-let load_paths_of_dir_path dir =
-  fst (list_filter2 (fun p d -> d = dir) !load_paths)
-    
-let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
+let extend_path_with_dirpath p dir =
+  List.fold_left Filename.concat p 
+    (List.map string_of_id (List.rev (repr_dirpath dir)))
+
+let root_paths_matching_dir_path dir =
+  let rec aux = function
+  | [] -> []
+  | (p,d,true) :: l when is_dirpath_prefix_of d dir ->
+      let suffix = drop_dirpath_prefix d dir in
+      extend_path_with_dirpath p suffix :: aux l
+  | _ :: l -> aux l in
+  aux !load_paths
+
+(* Root p is bound to A.B.C.D and we require file C.D.E.F *)
+(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *)
+
+(* Root p is bound to A.B.C.C and we require file C.C.E.F *)
+(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *)
+
+let intersections d1 d2 =
+  let rec aux d1 =
+    if d1 = empty_dirpath then [d2] else
+      let rest = aux (snd (chop_dirpath 1 d1)) in
+      if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
+      else rest in
+  aux d1
+
+let loadpaths_matching_dir_path dir =
+  let rec aux = function
+  | [] -> []
+  | (p,d,true) :: l ->
+      let inters = intersections d dir in
+      List.map (fun tl -> (extend_path_with_dirpath p tl,append_dirpath d tl))
+	inters @
+	aux l
+  | (p,d,_) :: l ->
+      (extend_path_with_dirpath p dir,append_dirpath d dir) :: aux l in
+  aux !load_paths
+
+let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths
 
 (************************************************************************)
 (*s Modules on disk contain the following informations (after the magic 
@@ -196,6 +232,12 @@ let library_full_filename dir =
   try LibraryFilenameMap.find dir !libraries_filename_table
   with Not_found -> "<unavailable filename>"
 
+let overwrite_library_filenames f =
+  let f =
+    if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in
+  LibraryMap.iter (fun dir _ -> register_library_filename dir f)
+    !libraries_table
+
 let library_is_loaded dir =
   try let _ = find_library dir in true
   with Not_found -> false
@@ -334,11 +376,11 @@ type library_location = LibLoaded | LibInPath
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
-  let loadpath = load_paths_of_dir_path pref in
+  let loadpath = root_paths_matching_dir_path pref in
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = (string_of_id base)^".vo" in
-    let _, file = System.where_in_path loadpath name in
+    let _, file = System.where_in_path false loadpath name in
     (dir, file)
   with Not_found ->
   (* Last chance, removed from the file system but still in memory *)
@@ -347,20 +389,15 @@ let locate_absolute_library dir =
   else
     raise LibNotFound
 
-let locate_qualified_library qid =
+let locate_qualified_library warn qid =
   try
     (* Search library in loadpath *)
-    let dir, base = repr_qualid qid in 
-    let loadpath =
-      if repr_dirpath dir = [] then get_load_paths ()
-      else 
-        (* we assume dir is an absolute dirpath *)
-	load_paths_of_dir_path dir
-    in
+    let dir, base = repr_qualid qid in
+    let loadpath = loadpaths_matching_dir_path dir in
     if loadpath = [] then raise LibUnmappedDir;
-    let name =  (string_of_id base)^".vo" in
-    let path, file = System.where_in_path loadpath name in
-    let dir = extend_dirpath (find_logical_path path) base in
+    let name = string_of_id base ^ ".vo" in
+    let lpath, file = System.where_in_path warn (List.map fst loadpath) name in
+    let dir = extend_dirpath (List.assoc lpath loadpath) base in
     (* Look if loaded *)
     if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
     (* Otherwise, look for it in the file system *)
@@ -386,7 +423,7 @@ let try_locate_absolute_library dir =
 
 let try_locate_qualified_library (loc,qid) =
   try
-    let (_,dir,f) = locate_qualified_library qid in
+    let (_,dir,f) = locate_qualified_library true qid in
     dir,f
   with e -> 
     explain_locate_library_error qid e
@@ -586,8 +623,7 @@ let import_module export (loc,qid) =
 (*s Initializing the compilation of a library. *)
 
 let start_library f = 
-  let _,longf = 
-    System.find_file_in_path (get_load_paths ()) (f^".v") in
+  let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
   let id = id_of_string (Filename.basename f) in
   let ldir = extend_dirpath ldir0 id in
diff --git a/library/library.mli b/library/library.mli
index 1e2197409..d7cef3243 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -52,6 +52,9 @@ val opened_libraries : unit -> dir_path list
   (* - Return the full filename of a loaded library. *)
 val library_full_filename : dir_path -> string
 
+  (* - Overwrite the filename of all libraries (used when restoring a state) *)
+val overwrite_library_filenames : string -> unit
+
 (*s Hook for the xml exportation of libraries *)
 val set_xml_require : (dir_path -> unit) -> unit
 
@@ -61,11 +64,10 @@ val set_xml_require : (dir_path -> unit) -> unit
 
 val get_load_paths : unit -> System.physical_path list
 val get_full_load_paths : unit -> (System.physical_path * dir_path) list
-val add_load_path : System.physical_path * dir_path -> unit
+val add_load_path : bool -> System.physical_path * dir_path -> unit
 val remove_load_path : System.physical_path -> unit
 val find_logical_path : System.physical_path -> dir_path
 val is_in_load_paths : System.physical_path -> bool
-val load_paths_of_dir_path : dir_path -> System.physical_path list
 
 (*s Locate a library in the load paths *)
 exception LibUnmappedDir
@@ -73,7 +75,7 @@ exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
-  qualid -> library_location * dir_path * System.physical_path
+  bool -> qualid -> library_location * dir_path * System.physical_path
 
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds
diff --git a/library/states.ml b/library/states.ml
index dcb4111ed..7c3953151 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -24,7 +24,9 @@ let state_magic_number = 19764
 let (extern_state,intern_state) =
   let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
   (fun s -> raw_extern s (freeze())),
-  (fun s -> unfreeze (raw_intern (Library.get_load_paths ()) s))
+  (fun s ->
+    unfreeze (raw_intern (Library.get_load_paths ()) s);
+    Library.overwrite_library_filenames s)
 
 (* Rollback. *)