Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un chemin Unix à un chemin Coq

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

8 files changed, 58 insertions, 38 deletions

diff --git a/lib/system.ml b/lib/system.ml
index f6da6f866..f571b4638 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -11,14 +11,14 @@ open Unix
 type load_path_entry = {
   directory : string;
   root_dir : string;
-  relative_subdir : string }
+  relative_subdir : string list }
 
 type load_path = load_path_entry list
 
 let exists_dir dir =
   try let _ = opendir dir in true with Unix_error _ -> false
 
-let all_subdirs root =
+let all_subdirs root alias =
   let l = ref [] in
   let add f rel = 
     l := { directory = f; root_dir = root; relative_subdir = rel } :: !l 
@@ -31,7 +31,7 @@ let all_subdirs root =
 	if f <> "." && f <> ".." && (not Coq_config.local or (f <> "CVS")) then
 	  let file = Filename.concat dir f in
 	  if (stat file).st_kind = S_DIR then begin
-	    let newrel = Filename.concat rel f in
+	    let newrel = rel@[f] in
 	    add file newrel;
 	    traverse file newrel
 	  end
@@ -41,8 +41,12 @@ let all_subdirs root =
   in
   if exists_dir root then
    begin
-     add root "";
-     traverse root ""
+     let alias = match alias with 
+       | Some a -> a
+       | None -> [Filename.basename root]
+     in
+     add root alias;
+     traverse root alias
    end ;
   List.rev !l
 
@@ -74,7 +78,7 @@ let find_file_in_path paths name =
   let globname = glob name in
   if not (Filename.is_relative globname) then
     let root = Filename.dirname globname in
-    { directory = root; root_dir = root; relative_subdir = "" }, globname
+    { directory = root; root_dir = root; relative_subdir = [] }, globname
   else 
     try 
       search_in_path paths name
diff --git a/lib/system.mli b/lib/system.mli
index 18dae1915..eb0783052 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,11 +8,11 @@
 type load_path_entry = {
   directory : string;
   root_dir : string;
-  relative_subdir : string }
+  relative_subdir : string list }
 
 type load_path = load_path_entry list
 
-val all_subdirs : string -> load_path
+val all_subdirs : unix_path:string -> string list option -> load_path
 val is_in_path : load_path -> string -> bool
 val where_in_path : load_path -> string -> load_path_entry * string
 
diff --git a/library/library.ml b/library/library.ml
index cd99b603e..abdce3482 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -17,14 +17,19 @@ let get_load_path () = !load_path
 
 let add_load_path_entry lpe = load_path := lpe :: !load_path
 
-let add_path dir = 
-  add_load_path_entry { directory = dir; root_dir = dir; relative_subdir = "" }
+let add_path dir coq_dirpath = 
+  if coq_dirpath = [] then anomaly "add_path: empty path in library";
+  Nametab.push_library_root (List.hd coq_dirpath);
+  add_load_path_entry
+    { directory = dir; root_dir = dir; relative_subdir = coq_dirpath }
 
 let remove_path dir =
   load_path := List.filter (fun lpe -> lpe.directory <> dir) !load_path
 
-let rec_add_path dir = 
-  load_path := (all_subdirs dir) @ !load_path
+let rec_add_path dir coq_dirpath =
+  if coq_dirpath = [] then anomaly "add_path: empty path in library";
+  Nametab.push_library_root (List.hd coq_dirpath);
+  load_path := (all_subdirs dir (Some coq_dirpath)) @ !load_path
 
 (*s Modules on disk contain the following informations (after the magic 
     number, and before the digest). *)
@@ -159,8 +164,7 @@ let rec load_module_from s f =
     List.iter (load_mandatory_module s) m.module_deps;
     Global.import m.module_compiled_env;
     load_objects m.module_declarations;
-    let dir = parse_loadpath lpe.relative_subdir in
-    let sp = Names.make_path dir (id_of_string s) CCI in
+    let sp = Names.make_path lpe.relative_subdir (id_of_string s) CCI in
     Nametab.push_module sp m.module_nametab;
     modules_table := Stringmap.add s m !modules_table;
     m
diff --git a/library/library.mli b/library/library.mli
index 4ff27b4cd..4d4a2d19b 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -58,6 +58,6 @@ val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit
 (*s Global load path *)
 val get_load_path : unit -> System.load_path
 val add_load_path_entry : System.load_path_entry -> unit
-val add_path : string -> unit
-val rec_add_path : string -> unit
+val add_path : unix_path:string -> coq_root:dir_path -> unit
+val rec_add_path : unix_path:string -> coq_root:dir_path -> unit
 val remove_path : string -> unit
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7262362ec..b50d3af4b 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -40,20 +40,23 @@ let load_rcfile() =
   else 
     if Options.is_verbose() then mSGNL [< 'sTR"Skipping rcfile loading." >]
 
+let add_ml_include s =
+  Mltop.dir_ml_dir s
+
 (* Puts dir in the path of ML and in the LoadPath *)
-let add_include s =
+let add_include s alias =
   Mltop.dir_ml_dir s;
-  Library.add_path s
+  Library.add_path s alias
 
-let add_rec_include s = 
-  let subdirs = all_subdirs s in
+let add_rec_include s alias = 
+  let subdirs = all_subdirs s (Some alias) in
   List.iter (fun lpe -> Mltop.dir_ml_dir lpe.directory) subdirs;
   List.iter Library.add_load_path_entry subdirs
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
-let push_include s = includes := (s,false) :: !includes
-let push_rec_include s = includes := (s,true) :: !includes
+let push_include (s, alias) = includes := (s,alias,false) :: !includes
+let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
 
 (* Because find puts "./" and the loadpath is not nicely pretty-printed *)
 let hm2 s = 
@@ -67,22 +70,23 @@ let init_load_path () =
   if Coq_config.local then begin
     (* local use (no installation) *)
     List.iter 
-      (fun s -> add_include (Filename.concat Coq_config.coqtop s))
+      (fun s -> add_include (Filename.concat Coq_config.coqtop s) ["Coq"])
       ["states"; "dev"];
-    add_rec_include (Filename.concat Coq_config.coqtop "theories");
-    add_include (Filename.concat Coq_config.coqtop "tactics");
-    add_rec_include (Filename.concat Coq_config.coqtop "contrib");
+    add_rec_include (Filename.concat Coq_config.coqtop "theories") ["Coq"];
+    add_include (Filename.concat Coq_config.coqtop "tactics") ["Coq"];
+    add_rec_include (Filename.concat Coq_config.coqtop "contrib") ["Coq"];
   end else begin
     (* default load path; variable COQLIB overrides the default library *)
     let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
-    add_rec_include coqlib
+    add_rec_include coqlib ["Coq"]
   end;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
-  add_include camlp4;
-  add_include ".";
+  add_ml_include camlp4;
+  add_include "." ["Scratch"];
   (* additional loadpath, given with -I -include -R options *)
   List.iter 
-    (fun (s,reci) -> if reci then add_rec_include s else add_include s)
+    (fun (s,alias,reci) ->
+       if reci then add_rec_include s alias else add_include s alias)
     (List.rev !includes);
   includes := []
 
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 7baa825be..86b2c9b64 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -11,7 +11,7 @@ val set_rcuser : string -> unit
 val no_load_rc : unit -> unit
 val load_rcfile : unit -> unit
 
-val push_include : string -> unit
-val push_rec_include : string -> unit
+val push_include : string * Names.dir_path -> unit
+val push_rec_include : string * Names.dir_path -> unit
 
 val init_load_path : unit -> unit
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 0c81359cb..e1ed88193 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -36,7 +36,7 @@ open Vernacinterp
 let coq_mlpath_copy = ref []
 let keep_copy_mlpath s = 
   let dir = glob s in
-  let lpe = { directory = dir; root_dir = dir; relative_subdir = "" } in
+  let lpe = { directory = dir; root_dir = dir; relative_subdir = [] } in
   coq_mlpath_copy := lpe :: !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
@@ -125,7 +125,7 @@ let dir_ml_dir s =
 
 (* For Rec Add ML Path *)
 let rdir_ml_dir dir = 
-  List.iter (fun lpe -> dir_ml_dir lpe.directory) (all_subdirs dir)
+  List.iter (fun lpe -> dir_ml_dir lpe.directory) (all_subdirs dir None)
 
 (* convertit un nom quelconque en nom de fichier ou de module *) 
 let mod_of_name name =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3e34733f5..427792147 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -165,7 +165,11 @@ let _ =
 let _ = 
   add "ADDPATH"
     (function 
-       | [VARG_STRING dir] -> (fun () -> add_path dir)
+       | [VARG_STRING dir] ->
+	   let alias = Filename.basename dir in
+	   if alias = "" then
+	     error ("Cannot map "^dir^" to a root of Coq library");
+	   (fun () -> add_path dir [alias])
        | _ -> bad_vernac_args "ADDPATH")
 
 (* For compatibility *)
@@ -178,7 +182,11 @@ let _ =
 let _ = 
   add "RECADDPATH"
     (function 
-       | [VARG_STRING dir] -> (fun () -> rec_add_path dir)
+       | [VARG_STRING dir] ->
+	   let alias = Filename.basename dir in
+	   if alias = "" then
+	     error ("Cannot map "^dir^" to a root of Coq library");
+	   (fun () -> rec_add_path dir [alias])
        | _ -> bad_vernac_args "RECADDPATH")
 
 (* For compatibility *)
@@ -284,9 +292,9 @@ let _ =
     (function 
        | [VARG_IDENTIFIER id] ->
 	   let s = string_of_id id in
-	   let {relative_subdir = dir},_ = 
+	   let lpe,_ = 
 	     System.find_file_in_path (Library.get_load_path ()) (s^".v") in
-	   fun () -> Lib.start_module ((parse_loadpath dir)@[s])
+	   fun () -> Lib.start_module (lpe.relative_subdir @ [s])
        | _ -> bad_vernac_args "BeginModule")
 
 let _ =