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

1 files changed, 129 insertions, 0 deletions

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