Moved the Loadpath part of Library to its own file, and documented

the interface.

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

6 files changed, 203 insertions, 115 deletions

diff --git a/library/library.ml b/library/library.ml
index edb86bc4c..dc0981497 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -17,99 +17,6 @@ open Safe_typing
 open Libobject
 open Lib
 
-(*************************************************************************)
-(*s Load path. Mapping from physical to logical paths etc.*)
-
-type logical_path = DirPath.t
-
-let load_paths = ref ([] : (CUnix.physical_path * logical_path * bool) list)
-
-let get_load_paths () = List.map pi1 !load_paths
-
-let find_logical_path phys_dir =
-  let phys_dir = CUnix.canonical_path_name phys_dir in
-  let filter (p, _, _) = String.equal p phys_dir in
-  let paths = List.filter filter !load_paths in
-  match paths with
-  | [_,dir,_] -> dir
-  | [] -> Nameops.default_root_prefix
-  | l -> anomaly (str "Two logical paths are associated to" ++ spc () ++ str phys_dir)
-
-let is_in_load_paths phys_dir =
-  let dir = CUnix.canonical_path_name phys_dir in
-  let lp = get_load_paths () in
-  let check_p = fun p -> (String.compare dir p) == 0 in
-    List.exists check_p lp
-
-let remove_load_path dir =
-  load_paths := List.filter (fun (p,_,_) -> not (String.equal p dir)) !load_paths
-
-let add_load_path isroot (phys_path,coq_path) =
-  let phys_path = CUnix.canonical_path_name phys_path in
-  let filter (p, _, _) = String.equal p phys_path in
-    match List.filter filter !load_paths with
-      | [_,dir,_] ->
-	  if not (DirPath.equal coq_path dir)
-            (* If this is not the default -I . to coqtop *)
-            && not
-            (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name)
-		&& DirPath.equal coq_path (Nameops.default_root_prefix))
-	  then
-	    begin
-              (* Assume the user is concerned by library naming *)
-	      if not (DirPath.equal dir Nameops.default_root_prefix) then
-		Flags.if_warn msg_warning
-		  (str phys_path ++ strbrk " was previously bound to " ++
-		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
-		   pr_dirpath coq_path);
-	      remove_load_path phys_path;
-	      load_paths := (phys_path,coq_path,isroot) :: !load_paths;
-	    end
-      | [] ->
-	  load_paths := (phys_path,coq_path,isroot) :: !load_paths;
-      | _ -> anomaly (str "Two logical paths are associated to" ++ spc () ++ str phys_path)
-
-let extend_path_with_dirpath p dir =
-  List.fold_left Filename.concat p
-    (List.rev_map Id.to_string (DirPath.repr 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 DirPath.is_empty d1 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
     number, and before the digest). *)
@@ -330,7 +237,7 @@ type library_location = LibLoaded | LibInPath
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
-  let loadpath = root_paths_matching_dir_path pref in
+  let loadpath = Loadpath.expand_root_path pref in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
   try
     let name = (Id.to_string base)^".vo" in
@@ -347,7 +254,7 @@ let locate_qualified_library warn qid =
   try
     (* Search library in loadpath *)
     let dir, base = repr_qualid qid in
-    let loadpath = loadpaths_matching_dir_path dir in
+    let loadpath = Loadpath.expand_path dir in
     let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
     let name = Id.to_string base ^ ".vo" in
     let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
@@ -480,7 +387,7 @@ let rec_intern_by_filename_only id f =
 
 let rec_intern_library_from_file idopt f =
   (* A name is specified, we have to check it contains library id *)
-  let paths = get_load_paths () in
+  let paths = Loadpath.get_paths () in
   let _, f =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
   rec_intern_by_filename_only idopt f
@@ -609,10 +516,15 @@ let check_coq_overwriting p id =
       ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
 
 let start_library f =
-  let paths = get_load_paths () in
-  let _,longf =
+  let paths = Loadpath.get_paths () in
+  let _, longf =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
-  let ldir0 = find_logical_path (Filename.dirname longf) in
+  let ldir0 =
+    try
+      let lp = Loadpath.find_load_path (Filename.dirname longf) in
+      Loadpath.logical lp
+    with Not_found -> Nameops.default_root_prefix
+  in
   let id = Id.of_string (Filename.basename f) in
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
@@ -661,7 +573,9 @@ let save_library_to dir f =
     System.marshal_out ch table;
     close_out ch;
     if not !Flags.no_native_compiler then begin
-    let lp = List.map CUnix.string_of_physical_path (get_load_paths ()) in
+    let lp = Loadpath.get_load_paths () in
+    let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in
+    let lp = List.map map_path lp in
     let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
     match Nativelibrary.compile_library dir ast lp fn with
       | 0 -> ()
@@ -686,6 +600,8 @@ let mem s =
 		 (CObj.size_kb m.library_objects)))
 
 let get_load_paths_str () =
-  List.map CUnix.string_of_physical_path (get_load_paths ())
+  let lp = Loadpath.get_load_paths () in
+  let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in
+  List.map map_path lp
 
 let _ = Nativelib.get_load_paths := get_load_paths_str
diff --git a/library/library.mli b/library/library.mli
index 11253087a..22b94e521 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -58,18 +58,6 @@ val overwrite_library_filenames : string -> unit
 (** {6 Hook for the xml exportation of libraries } *)
 val set_xml_require : (DirPath.t -> unit) -> unit
 
-(** {6 ... } *)
-(** Global load paths: a load path is a physical path in the file
-    system; to each load path is associated a Coq [DirPath.t] (the "logical"
-    path of the physical path) *)
-
-val get_load_paths : unit -> CUnix.physical_path list
-val get_full_load_paths : unit -> (CUnix.physical_path * DirPath.t) list
-val add_load_path : bool -> CUnix.physical_path * DirPath.t -> unit
-val remove_load_path : CUnix.physical_path -> unit
-val find_logical_path : CUnix.physical_path -> DirPath.t
-val is_in_load_paths : CUnix.physical_path -> bool
-
 (** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir
 exception LibNotFound
diff --git a/library/library.mllib b/library/library.mllib
index 2d03f14cb..2568bcc18 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -7,6 +7,7 @@ Nametab
 Global
 Lib
 Declaremods
+Loadpath
 Library
 States
 Kindops
diff --git a/library/loadpath.ml b/library/loadpath.ml
new file mode 100644
index 000000000..44b53c09a
--- /dev/null
+++ b/library/loadpath.ml
@@ -0,0 +1,129 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Errors
+open Names
+open Libnames
+
+(** Load paths. Mapping from physical to logical paths. *)
+
+type t = {
+  path_physical : CUnix.physical_path;
+  path_logical : DirPath.t;
+  path_is_root : bool;
+}
+
+let logical p = p.path_logical
+
+let physical p = p.path_physical
+
+let load_paths = ref ([] : t list)
+
+let get_load_paths () = !load_paths
+
+let get_paths () = List.map physical !load_paths
+
+let anomaly_too_many_paths path =
+  anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
+
+let find_load_path phys_dir =
+  let phys_dir = CUnix.canonical_path_name phys_dir in
+  let filter p = String.equal p.path_physical phys_dir in
+  let paths = List.filter filter !load_paths in
+  match paths with
+  | [] -> raise Not_found
+  | [p] -> p
+  | _ -> anomaly_too_many_paths phys_dir
+
+let is_in_load_paths phys_dir =
+  let dir = CUnix.canonical_path_name phys_dir in
+  let lp = get_load_paths () in
+  let check_p p = String.equal dir p.path_physical in
+  List.exists check_p lp
+
+let remove_load_path dir =
+  let filter p = not (String.equal p.path_physical dir) in
+  load_paths := List.filter filter !load_paths
+
+let add_load_path phys_path isroot coq_path =
+  let phys_path = CUnix.canonical_path_name phys_path in
+  let filter p = String.equal p.path_physical phys_path in
+  let binding = {
+    path_logical = coq_path;
+    path_physical = phys_path;
+    path_is_root = isroot;
+  } in
+  match List.filter filter !load_paths with
+  | [] ->
+    load_paths := binding :: !load_paths;
+  | [p] ->
+    let dir = p.path_logical in
+    if not (DirPath.equal coq_path dir)
+      (* If this is not the default -I . to coqtop *)
+      && not
+      (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name)
+          && DirPath.equal coq_path (Nameops.default_root_prefix))
+    then
+      begin
+        (* Assume the user is concerned by library naming *)
+        if not (DirPath.equal dir Nameops.default_root_prefix) then
+          Flags.if_warn msg_warning
+            (str phys_path ++ strbrk " was previously bound to " ++
+              pr_dirpath dir ++ strbrk "; it is remapped to " ++
+              pr_dirpath coq_path);
+        remove_load_path phys_path;
+        load_paths := binding :: !load_paths;
+      end
+  | _ -> anomaly_too_many_paths phys_path
+
+let extend_path_with_dirpath p dir =
+  List.fold_left Filename.concat p
+    (List.rev_map Id.to_string (DirPath.repr dir))
+
+let expand_root_path dir =
+  let rec aux = function
+  | [] -> []
+  | p :: l ->
+    if p.path_is_root && is_dirpath_prefix_of p.path_logical dir then
+      let suffix = drop_dirpath_prefix p.path_logical dir in
+      extend_path_with_dirpath p.path_physical suffix :: aux l
+    else 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 DirPath.is_empty d1 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 expand p dir =
+  let ph = extend_path_with_dirpath p.path_physical dir in
+  let log = append_dirpath p.path_logical dir in
+  (ph, log)
+
+let expand_path dir =
+  let rec aux = function
+  | [] -> []
+  | p :: l ->
+    if p.path_is_root then
+      let inters = intersections p.path_logical dir in
+      List.map (expand p) inters @ aux l
+    else
+      expand p dir :: aux l in
+  aux !load_paths
diff --git a/library/loadpath.mli b/library/loadpath.mli
new file mode 100644
index 000000000..8928542a6
--- /dev/null
+++ b/library/loadpath.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+
+(** * Load paths.
+
+  A load path is a physical path in the file system; to each load path is
+  associated a Coq [DirPath.t] (the "logical" path of the physical path).
+
+*)
+
+type t
+(** Type of loadpath bindings. *)
+
+val physical : t -> CUnix.physical_path
+(** Get the physical path (filesystem location) of a loadpath. *)
+
+val logical : t -> DirPath.t
+(** Get the logical path (Coq module hierarchy) of a loadpath. *)
+
+val get_load_paths : unit -> t list
+(** Get the current loadpath association. *)
+
+val get_paths : unit -> CUnix.physical_path list
+(** Same as [get_load_paths] but only get the physical part. *)
+
+val add_load_path : CUnix.physical_path -> bool -> DirPath.t -> unit
+(** [add_load_path root phys log] adds the binding [phys := log] to the current
+    loadpaths. The [root] flag indicates whether this loadpath has to be treated
+    as a root one. *)
+
+val remove_load_path : CUnix.physical_path -> unit
+(** Remove the current logical path binding associated to a given physical path,
+    if any. *)
+
+val find_load_path : CUnix.physical_path -> t
+(** Get the binding associated to a physical path. Raises [Not_found] if there
+    is none. *)
+
+val is_in_load_paths : CUnix.physical_path -> bool
+(** Whether a physical path is currently bound. *)
+
+val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
+(** Given a relative logical path, associate the list of absolute physical and
+    logical paths which are possible expansions of it. *)
+
+val expand_root_path : DirPath.t -> CUnix.physical_path list
+(** As [expand_path] but restricts to root loadpaths. *)
diff --git a/library/states.ml b/library/states.ml
index 906ebdacc..9d15dfc6c 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -28,8 +28,8 @@ let (extern_state,intern_state) =
     raw_extern s (freeze())),
   (fun s ->
     let s = ensure_suffix s in
-    unfreeze
-      (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
+    let paths = Loadpath.get_paths () in
+    unfreeze (with_magic_number_check (raw_intern paths) s);
     Library.overwrite_library_filenames s)
 
 (* Rollback. *)