Nicer code concerning dirpaths and modpath around Lib

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

5 files changed, 66 insertions, 90 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 8d332b7df..dae585d5a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -764,7 +764,7 @@ let declare_one_include interp_modast (me_ast,annot) =
   let env = Global.env() in
   let me,kind = interp_modast env ModAny me_ast in
   let is_mod = (kind == Module) in
-  let cur_mp = fst (Lib.current_prefix ()) in
+  let cur_mp = Lib.current_mp () in
   let inl = inl2intopt annot in
   let mbids,aobjs = get_module_sobjs is_mod env inl me in
   let subst_self =
diff --git a/library/lib.ml b/library/lib.ml
index 159ac2d6d..e8b56de70 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -104,15 +104,13 @@ let library_dp () =
    module path and relative section path *)
 let path_prefix = ref initial_prefix
 
-let sections_depth () =
-  List.length (Names.DirPath.repr (snd (snd !path_prefix)))
-
-let sections_are_opened () =
-  match Names.DirPath.repr (snd (snd !path_prefix)) with
-      [] -> false
-    | _ -> true
-
 let cwd () = fst !path_prefix
+let current_prefix () = snd !path_prefix
+let current_mp () = fst (snd !path_prefix)
+let current_sections () = snd (snd !path_prefix)
+
+let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
+let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
 
 let cwd_except_section () =
   Libnames.pop_dirpath_n (sections_depth ()) (cwd ())
@@ -123,26 +121,14 @@ let current_dirpath sec =
 
 let make_path id = Libnames.make_path (cwd ()) id
 
-let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id
-
-let path_of_include () =
-  let dir = Names.DirPath.repr (cwd ()) in
-  let new_dir = List.tl dir in
-  let id = List.hd dir in
-    Libnames.make_path (Names.DirPath.make new_dir) id
-
-let current_prefix () = snd !path_prefix
+let make_path_except_section id =
+  Libnames.make_path (cwd_except_section ()) id
 
 let make_kn id =
   let mp,dir = current_prefix () in
-    Names.make_kn mp dir (Names.Label.of_id id)
+  Names.make_kn mp dir (Names.Label.of_id id)
 
-let make_con id =
-  let mp,dir = current_prefix () in
-    Names.make_con mp dir (Names.Label.of_id id)
-
-
-let make_oname id = make_path id, make_kn id
+let make_oname id = Libnames.make_oname !path_prefix id
 
 let recalc_path_prefix () =
   let rec recalc = function
@@ -156,7 +142,7 @@ let recalc_path_prefix () =
 
 let pop_path_prefix () =
   let dir,(mp,sec) = !path_prefix in
-    path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec))
+  path_prefix := pop_dirpath dir, (mp, pop_dirpath sec)
 
 let find_entry_p p =
   let rec find = function
@@ -219,8 +205,7 @@ let add_anonymous_entry node =
   add_entry (make_oname (anonymous_id ())) node
 
 let add_leaf id obj =
-  let (path, _) = current_prefix () in
-  if Names.ModPath.equal path Names.initial_path then
+  if Names.ModPath.equal (current_mp ()) Names.initial_path then
     error ("No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
@@ -271,16 +256,15 @@ let current_mod_id () =
 
 
 let start_mod is_type export id mp fs =
-  let dir = add_dirpath_suffix (fst !path_prefix) id in
+  let dir = add_dirpath_suffix (cwd ()) id in
   let prefix = dir,(mp,Names.DirPath.empty) in
-  let sp = make_path id in
-  let oname = sp, make_kn id in
   let exists =
-    if is_type then Nametab.exists_cci sp else Nametab.exists_module dir
+    if is_type then Nametab.exists_cci (make_path id)
+    else Nametab.exists_module dir
   in
   if exists then
     errorlabstrm "open_module" (pr_id id ++ str " already exists");
-  add_entry oname (OpenedModule (is_type,export,prefix,fs));
+  add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
   path_prefix := prefix;
   prefix
 
@@ -322,7 +306,7 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
 let start_compilation s mp =
   if !comp_name != None then
     error "compilation unit is already started";
-  if not (Names.DirPath.equal (snd (snd (!path_prefix))) Names.DirPath.empty) then
+  if not (Names.DirPath.is_empty (current_sections ())) then
     error "some sections are already opened";
   let prefix = s, (mp, Names.DirPath.empty) in
   let () = add_anonymous_entry (CompilingLibrary prefix) in
@@ -482,11 +466,10 @@ let open_section id =
   let olddir,(mp,oldsec) = !path_prefix in
   let dir = add_dirpath_suffix olddir id in
   let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
-  let name = make_path id, make_kn id (* this makes little sense however *) in
   if Nametab.exists_section dir then
     errorlabstrm "open_section" (pr_id id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:`No in
-  add_entry name (OpenedSection (prefix, fs));
+  add_entry (make_oname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
   path_prefix := prefix;
@@ -545,42 +528,36 @@ let init () =
 
 (* Misc *)
 
-let mp_of_global ref =
-  match ref with
-    | VarRef id -> fst (current_prefix ())
-    | ConstRef cst -> Names.con_modpath cst
-    | IndRef ind -> Names.ind_modpath ind
-    | ConstructRef constr -> Names.constr_modpath constr
-
-let rec dp_of_mp modp =
-  match modp with
-    | Names.MPfile dp -> dp
-    | Names.MPbound _ -> library_dp ()
-    | Names.MPdot (mp,_) -> dp_of_mp mp
-
-let rec split_mp mp =
-  match mp with
-    | Names.MPfile dp -> dp,  Names.DirPath.empty
-    | Names.MPdot (prfx, lbl) ->
-	let mprec, dprec = split_mp prfx in
-	  mprec, Names.DirPath.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.DirPath.repr dprec))
-    | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in  library_dp(), Names.DirPath.make [id]
-
-let split_modpath mp =
-  let rec aux = function
-    | Names.MPfile dp -> dp, []
-    | Names.MPbound mbid ->
-	library_dp (), [Names.MBId.to_id mbid]
-    | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
-			      (mp', Names.Label.to_id l :: lab)
-  in
-  let (mp, l) = aux mp in
-    mp, l
-
-let library_part ref =
-  match ref with
-    | VarRef id -> library_dp ()
-    | _ -> dp_of_mp (mp_of_global ref)
+let mp_of_global = function
+  |VarRef id -> current_mp ()
+  |ConstRef cst -> Names.con_modpath cst
+  |IndRef ind -> Names.ind_modpath ind
+  |ConstructRef constr -> Names.constr_modpath constr
+
+let rec dp_of_mp = function
+  |Names.MPfile dp -> dp
+  |Names.MPbound _ -> library_dp ()
+  |Names.MPdot (mp,_) -> dp_of_mp mp
+
+let rec split_mp = function
+  |Names.MPfile dp -> dp, Names.DirPath.empty
+  |Names.MPdot (prfx, lbl) ->
+    let mprec, dprec = split_mp prfx in
+    mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl)
+  |Names.MPbound mbid ->
+    let (_,id,dp) = Names.MBId.repr mbid in
+    library_dp (), Names.DirPath.make [id]
+
+let rec split_modpath = function
+  |Names.MPfile dp -> dp, []
+  |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid]
+  |Names.MPdot (mp,l) ->
+    let (dp,ids) = split_modpath mp in
+    (dp, Names.Label.to_id l :: ids)
+
+let library_part = function
+  |VarRef id -> library_dp ()
+  |ref -> dp_of_mp (mp_of_global ref)
 
 let remove_section_part ref =
   let sp = Nametab.path_of_global ref in
@@ -602,12 +579,12 @@ let remove_section_part ref =
 let con_defined_in_sec kn =
   let _,dir,_ = Names.repr_con kn in
   not (Names.DirPath.is_empty dir) &&
-  Names.DirPath.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
+  Names.DirPath.equal (pop_dirpath dir) (current_sections ())
 
 let defined_in_sec kn =
   let _,dir,_ = Names.repr_mind kn in
   not (Names.DirPath.is_empty dir) &&
-  Names.DirPath.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
+  Names.DirPath.equal (pop_dirpath dir) (current_sections ())
 
 let discharge_global = function
   | ConstRef kn when con_defined_in_sec kn ->
diff --git a/library/lib.mli b/library/lib.mli
index 1362fabf8..fa3bd3f48 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -81,12 +81,10 @@ val cwd_except_section : unit -> Names.DirPath.t
 val current_dirpath : bool -> Names.DirPath.t (* false = except sections *)
 val make_path : Names.Id.t -> Libnames.full_path
 val make_path_except_section : Names.Id.t -> Libnames.full_path
-val path_of_include : unit -> Libnames.full_path
 
 (** Kernel-side names *)
-val current_prefix : unit -> Names.module_path * Names.DirPath.t
+val current_mp : unit -> Names.module_path
 val make_kn : Names.Id.t -> Names.kernel_name
-val make_con : Names.Id.t -> Names.constant
 
 (** Are we inside an opened section *)
 val sections_are_opened : unit -> bool
diff --git a/library/libnames.ml b/library/libnames.ml
index bc2406f27..d1bef531a 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -17,33 +17,34 @@ let pr_dirpath sl = (str (DirPath.to_string sl))
 
 (*s Operations on dirpaths *)
 
-(* Pop the last n module idents *)
-let pop_dirpath_n n dir =
-  DirPath.make (List.skipn n (DirPath.repr dir))
+let split_dirpath d = match DirPath.repr d with
+  | id :: l -> DirPath.make l, id
+  | _ -> failwith "split_dirpath"
 
 let pop_dirpath p = match DirPath.repr p with
-  | [] -> anomaly (str "dirpath_prefix: empty dirpath")
   | _::l -> DirPath.make l
+  | [] -> failwith "pop_dirpath"
+
+(* Pop the last n module idents *)
+let pop_dirpath_n n dir = DirPath.make (List.skipn n (DirPath.repr dir))
 
 let is_dirpath_prefix_of d1 d2 =
   List.prefix_of (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
 
 let chop_dirpath n d =
   let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in
-    DirPath.make (List.rev d1), DirPath.make (List.rev d2)
+  DirPath.make (List.rev d1), DirPath.make (List.rev d2)
 
 let drop_dirpath_prefix d1 d2 =
-  let d = Util.List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) in
-    DirPath.make (List.rev d)
+  let d =
+    List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
+  in
+  DirPath.make (List.rev d)
 
 let append_dirpath d1 d2 = DirPath.make (DirPath.repr d2 @ DirPath.repr d1)
 
-(* To know how qualified a name should be to be understood in the current env*)
 let add_dirpath_prefix id d = DirPath.make (DirPath.repr d @ [id])
 
-let split_dirpath d =
-  let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l)
-
 let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p)
 
 (* parsing *)
diff --git a/library/libnames.mli b/library/libnames.mli
index c44fea543..627b8f013 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -18,13 +18,13 @@ val pr_dirpath : DirPath.t -> Pp.std_ppcmds
 val dirpath_of_string : string -> DirPath.t
 val string_of_dirpath : DirPath.t -> string
 
-(** Pop the suffix of a [DirPath.t] *)
+(** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *)
 val pop_dirpath : DirPath.t -> DirPath.t
 
 (** Pop the suffix n times *)
 val pop_dirpath_n : int -> DirPath.t -> DirPath.t
 
-(** Give the immediate prefix and basename of a [DirPath.t] *)
+(** Immediate prefix and basename of a [DirPath.t]. May raise [Failure] *)
 val split_dirpath : DirPath.t -> DirPath.t * Id.t
 
 val add_dirpath_suffix : DirPath.t -> module_ident -> DirPath.t