Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins

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

7 files changed, 66 insertions, 63 deletions

diff --git a/library/declare.ml b/library/declare.ml
index c2ac0ce45..1c034190e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -43,24 +43,28 @@ let depth_of_strength = function
 
 let restrict_path n sp =
   let dir, s, k = repr_path sp in
-  let dir' = list_lastn n dir in
-  Names.make_path dir' s k
+  let dir' = list_lastn n (repr_dirpath dir) in
+  Names.make_path (make_dirpath dir') s k
 
 let make_strength_0 () = 
   let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
   if depth > 0 then DischargeAt (cwd, depth) else NeverDischarge
 
+let extract_dirpath_prefix n dir =
+  let dir = repr_dirpath dir in
+  make_dirpath (list_firstn (List.length dir -n) dir)
+
 let make_strength_1 () =
   let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
-  if depth > 1 then DischargeAt (list_firstn (List.length cwd -1) cwd, depth-1)
+  if depth > 1 then DischargeAt (extract_dirpath_prefix 1 cwd, depth-1)
   else NeverDischarge
 
 let make_strength_2 () =
   let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
-  if depth > 2 then DischargeAt (list_firstn (List.length cwd -2) cwd, depth-2)
+  if depth > 2 then DischargeAt (extract_dirpath_prefix 2 cwd, depth-2)
   else NeverDischarge
 
 
@@ -450,10 +454,10 @@ let is_section_variable = function
 
 let is_global id =
   try 
-    let osp = Nametab.locate (make_qualid [] id) in
+    let osp = Nametab.locate (make_short_qualid id) in
     (* Compatibilité V6.3: Les variables de section ne sont pas globales
     not (is_section_variable osp) && *)
-    list_prefix_of (dirpath_of_global osp) (Lib.cwd())
+    is_dirpath_prefix_of (dirpath_of_global osp) (Lib.cwd())
   with Not_found -> 
     false
 
diff --git a/library/global.ml b/library/global.ml
index 1f509bcde..b55f741dd 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -78,9 +78,9 @@ let qualid_of_global ref =
     if (try Nametab.locate qid = ref with Not_found -> false) then qid
     else match dir with
       | [] -> Nametab.qualid_of_sp sp
-      | a::l -> find_visible l (a::qdir)
+      | a::l -> find_visible l (add_dirpath_prefix a qdir)
   in
-  find_visible (List.rev (dirpath sp)) []
+  find_visible (rev_repr_dirpath (dirpath sp)) (make_dirpath [])
 
 let string_of_global ref = Nametab.string_of_qualid (qualid_of_global ref)
 
diff --git a/library/lib.ml b/library/lib.ml
index c6ebfa000..e85e834ec 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -17,9 +17,9 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of dir_path
-  | OpenedSection of module_ident * Summary.frozen
+  | OpenedSection of dir_path * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
-  | ClosedSection of bool * module_ident * library_segment
+  | ClosedSection of bool * dir_path * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -36,9 +36,7 @@ and library_segment = library_entry list
 
 let lib_stk = ref ([] : (section_path * node) list)
 
-let default_module_name = id_of_string "Top"
-let default_module = make_dirpath [default_module_name]
-let init_toplevel_root () = Nametab.push_library_root default_module_name
+let init_toplevel_root () = Nametab.push_library_root default_module
 
 let module_name = ref None
 let path_prefix = ref (default_module : dir_path)
@@ -48,23 +46,19 @@ let module_sp () =
 
 let recalc_path_prefix () =
   let rec recalc = function
-    | (sp, OpenedSection (modid,_)) :: _ -> (dirpath sp)@[modid]
+    | (sp, OpenedSection (dir,_)) :: _ -> dir
     | _::l -> recalc l
     | [] -> module_sp ()
   in
   path_prefix := recalc !lib_stk
 
-let pop_path_prefix () =
-  let rec pop = function
-    | [] -> assert false
-    | [_] -> []
-    | s::l -> s :: (pop l)
-  in
-  path_prefix := pop !path_prefix
+let pop_path_prefix () = path_prefix := fst (split_dirpath !path_prefix)
 
 let make_path id k = Names.make_path !path_prefix id k
 
-let sections_depth () = List.length !path_prefix - List.length (module_sp ())
+let sections_depth () =
+  List.length (rev_repr_dirpath !path_prefix)
+  - List.length (rev_repr_dirpath (module_sp ()))
 
 let cwd () = !path_prefix
 
@@ -122,11 +116,11 @@ let contents_after = function
 (* Sections. *)
 
 let open_section id =
-  let dir = !path_prefix @ [id] in
+  let dir = extend_dirpath !path_prefix id in
   let sp = make_path id OBJ in
   if Nametab.exists_section dir then
     errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
-  add_entry sp (OpenedSection (id, freeze_summaries()));
+  add_entry sp (OpenedSection (dir, freeze_summaries()));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_section dir;
   path_prefix := dir;
@@ -145,7 +139,7 @@ let start_module s =
   if !path_prefix <> default_module then
     error "some sections are already opened";
   module_name := Some s;
-  (match split_dirpath s with [],id -> Nametab.push_library_root id | _ -> ());
+  Nametab.push_library_root s;
   Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
   path_prefix := s
@@ -179,10 +173,12 @@ let export_segment seg =
   clean [] seg
 
 let close_section export id =
-  let sp,fs = 
+  let sp,dir,fs = 
     try match find_entry_p is_opened_section with
-      | sp,OpenedSection (id',fs) -> 
-	  if id<>id' then error "this is not the last opened section"; (sp,fs)
+      | sp,OpenedSection (dir,fs) -> 
+	  if id<>snd(split_dirpath dir) then
+	    error "this is not the last opened section";
+	  (sp,dir,fs)
       | _ -> assert false
     with Not_found ->
       error "no opened section"
@@ -191,8 +187,8 @@ let close_section export id =
   lib_stk := before;
   let after' = export_segment after in
   pop_path_prefix ();
-  add_entry (make_path id OBJ) (ClosedSection (export, id, after'));
-  (sp,after,fs)
+  add_entry (make_path id OBJ) (ClosedSection (export, dir, after'));
+  (dir,after,fs)
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
@@ -252,7 +248,7 @@ let init () =
   lib_stk := [];
   add_frozen_state ();
   module_name := None;
-  path_prefix := [];
+  path_prefix := make_dirpath [];
   init_summaries()
 
 (* Initial state. *)
diff --git a/library/lib.mli b/library/lib.mli
index 0421f0812..faf80428a 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -21,8 +21,8 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of dir_path
-  | OpenedSection of module_ident * Summary.frozen
-  | ClosedSection of bool * module_ident * library_segment
+  | OpenedSection of dir_path * Summary.frozen
+  | ClosedSection of bool * dir_path * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -50,7 +50,7 @@ val contents_after : section_path option -> library_segment
 
 val open_section : identifier -> section_path
 val close_section : 
-  export:bool -> identifier -> section_path * library_segment * Summary.frozen
+  export:bool -> identifier -> dir_path * library_segment * Summary.frozen
 val sections_are_opened : unit -> bool
 
 val make_path : identifier -> path_kind -> section_path
diff --git a/library/library.ml b/library/library.ml
index df5d588bd..46c6b8b50 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -145,7 +145,8 @@ let module_is_loaded dir =
   try let _ = CompUnitmap.find dir !modules_table in true
   with Not_found -> false
 
-let module_is_opened s = (find_module [id_of_string s]).module_opened
+let module_is_opened s =
+  (find_module (make_dirpath [id_of_string s])).module_opened
 
 let loaded_modules () =
   CompUnitmap.fold (fun s _ l -> s :: l) !modules_table []
@@ -183,8 +184,8 @@ let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
     | _,OpenedSection _ -> assert false
-    | sp,ClosedSection (export,s,seg) ->
-	push_section (wd_of_sp sp);
+    | sp,ClosedSection (export,dir,seg) ->
+	push_section dir;
 	if export then iter seg
     | _,(FrozenState _ | Module _) -> ()
   and iter seg =
@@ -263,9 +264,7 @@ let rec load_module = function
 	  [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
 	  pr_dirpath md.md_name; 'sPC; 'sTR "and not module"; 'sPC;
 	  pr_dirpath dir >];
-      (match split_dirpath dir with
-	| [], id -> Nametab.push_library_root id
-	| _ -> ());
+      Nametab.push_library_root dir;
       compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
       (md, digest) in
     intern_module digest f md
@@ -317,7 +316,7 @@ let locate_qualified_library qid =
   try
     let dir, base = repr_qualid qid in 
     let loadpath =
-      if dir = [] then get_load_path ()
+      if is_empty_dirpath dir then get_load_path ()
       else 
         (* we assume dir is an absolute dirpath *)
 	load_path_of_logical_path dir
@@ -325,7 +324,7 @@ let locate_qualified_library qid =
     if loadpath = [] then raise LibUnmappedDir;
     let name =  (string_of_id base)^".vo" in
     let path, file = System.where_in_path loadpath name in
-    (LibInPath, find_logical_path path@[base], file)
+    (LibInPath, extend_dirpath (find_logical_path path) base, file)
   with Not_found -> raise LibNotFound
 
 let try_locate_qualified_library qid =
@@ -365,9 +364,7 @@ let locate_by_filename_only id f =
        m.module_filename);
     (LibLoaded, md.md_name, m.module_filename)
   with Not_found ->
-    (match split_dirpath md.md_name with
-      | [], id -> Nametab.push_library_root id
-      | _ -> ());
+    Nametab.push_library_root md.md_name;
     compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
     (LibInPath, md.md_name, f)
 
@@ -375,7 +372,7 @@ let locate_module qid = function
   | Some f ->
       (* A name is specified, we have to check it contains module id *)
       let prefix, id = repr_qualid qid in
-      assert (prefix = []);
+      assert (is_empty_dirpath prefix);
       let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
       locate_by_filename_only (Some id) f
   | None ->
diff --git a/library/nametab.ml b/library/nametab.ml
index f09787866..309841796 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,14 +18,16 @@ type qualid = dir_path * identifier
 let make_qualid p id = (p,id)
 let repr_qualid q = q
 
-let string_of_qualid (l,id) =
-  let dir = if l = [] then "" else string_of_dirpath l ^ "." in
-  dir ^ string_of_id id
+let empty_dirpath = make_dirpath []
+let make_short_qualid id = (empty_dirpath,id)
+
+let string_of_qualid (l,id) = string_of_path (make_path l id CCI)
+
 let pr_qualid p = pr_str (string_of_qualid p)
 
 let qualid_of_sp sp = make_qualid (dirpath sp) (basename sp)
 let qualid_of_dirpath dir = 
-  let a,l = list_sep_last (repr_qualid dir) in
+  let (l,a) = split_dirpath dir in
   make_qualid l a
 
 exception GlobalizationError of qualid
@@ -42,11 +44,13 @@ let error_global_not_found q = raise (GlobalizationError q)
 (*s Roots of the space of absolute names *)
 
 let coq_root = id_of_string "Coq"
-let default_root_prefix = []
+let default_root_prefix = make_dirpath []
 
 (* Obsolète
 let roots = ref []
-let push_library_root s = roots := list_add_set s !roots
+let push_library_root = function
+  | [] -> ()
+  | s::_ -> roots := list_add_set s !roots
 *)
 let push_library_root s = ()
 
@@ -90,6 +94,7 @@ let dirpath_of_extended_ref = function
 (* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *)
 (* We proceed in the reverse way, looking first to [id] *)
 let push_tree extract_dirpath tab visibility dir o =
+  let extract = option_app (fun c -> rev_repr_dirpath (extract_dirpath c)) in
   let rec push level (current,dirmap) = function
     | modid :: path as dir ->
 	let mc = 
@@ -98,7 +103,7 @@ let push_tree extract_dirpath tab visibility dir o =
 	in
 	let this =
           if level >= visibility then
-            if option_app extract_dirpath current = Some dir then
+            if extract current = Some dir then
               (* This is an absolute name, we must keep it otherwise it may
                  become unaccessible forever *)
               current
@@ -107,7 +112,7 @@ let push_tree extract_dirpath tab visibility dir o =
           else current in
 	(this, ModIdmap.add modid (push (level+1) mc path) dirmap)
     | [] -> (Some o,dirmap) in
-  push 0 tab (List.rev dir)
+  push 0 tab (rev_repr_dirpath dir)
 
 let push_idtree extract_dirpath tab n dir id o =
   let modtab =
@@ -149,14 +154,14 @@ let push_syntactic_definition sp =
 
 let push_short_name_syntactic_definition sp =
   let _, s = repr_qualid (qualid_of_sp sp) in
-  push_short_name_ccipath Pervasives.max_int [] s (SyntacticDef sp)
+  push_short_name_ccipath Pervasives.max_int empty_dirpath s (SyntacticDef sp)
 
 (* This is for dischargeable non-cci objects (removed at the end of the
    section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
 
 let push_short_name_object sp =
   let _, s = repr_qualid (qualid_of_sp sp) in
-  push_short_name_objpath 0 [] s sp
+  push_short_name_objpath 0 empty_dirpath s sp
 
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
 
@@ -164,18 +169,18 @@ let push_section fulldir =
   let dir, s = split_dirpath fulldir in
   (* We push all partially qualified name *)
   push_long_names_secpath dir s fulldir;
-  push_long_names_secpath [] s fulldir
+  push_long_names_secpath empty_dirpath s fulldir
 
 (* These are entry points to locate names *)
 let locate_in_tree tab dir =
-  let dir = List.rev dir in
+  let dir = rev_repr_dirpath dir in
   let rec search (current,modidtab) = function
     | modid :: path -> search (ModIdmap.find modid modidtab) path
     | [] -> match current with Some o -> o | _ -> raise Not_found
   in
   search tab dir
 
-let locate_cci qid =
+let locate_cci (qid:qualid) =
   let (dir,id) = repr_qualid qid in
   locate_in_tree (Idmap.find id !the_ccitab) dir
 
@@ -196,7 +201,7 @@ let locate_obj qid =
 let push_loaded_library fulldir =
   let dir, s = split_dirpath fulldir in
   push_long_names_libpath dir s fulldir;
-  push_long_names_libpath [] s fulldir
+  push_long_names_libpath empty_dirpath s fulldir
 
 let locate_loaded_library qid =
   let (dir,id) = repr_qualid qid in
@@ -215,14 +220,14 @@ let locate_constant qid =
     | TrueGlobal (VarRef sp) -> sp
     | _ -> raise Not_found
 
-let sp_of_id _ id = match locate_cci (make_qualid [] id) with
+let sp_of_id _ id = match locate_cci (make_short_qualid id) with
   | TrueGlobal ref -> ref
   | SyntacticDef _ ->
       anomaly ("sp_of_id: "^(string_of_id id)
 	       ^" is not a true global reference but a syntactic definition")
 
 let constant_sp_of_id id =
-  match locate_cci (make_qualid [] id) with
+  match locate_cci (make_short_qualid id) with
     | TrueGlobal (ConstRef sp) -> sp
     | _ -> raise Not_found
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 44e4e6b44..5fb7eb237 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -28,6 +28,7 @@ type qualid
 
 val make_qualid : dir_path -> identifier -> qualid
 val repr_qualid : qualid -> dir_path * identifier
+val make_short_qualid : identifier -> qualid
 
 val string_of_qualid : qualid -> string
 val pr_qualid : qualid -> std_ppcmds
@@ -89,7 +90,7 @@ val coq_root : module_ident
 val default_root_prefix : dir_path
 
 (* This is to declare a new root *)
-val push_library_root : module_ident -> unit
+val push_library_root : dir_path -> unit
 
 (* This turns a "user" absolute name into a global reference;
    especially, constructor/inductive names are turned into internal