[lib] [api] Introduce record for `object_prefix`

This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.

10 files changed, 107 insertions, 74 deletions

diff --git a/API/API.mli b/API/API.mli
index 7ec3cbee3..4c1dbeabc 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2070,7 +2070,11 @@ sig
   val basename : full_path -> Names.Id.t
 
   type object_name = full_path * Names.KerName.t
-  type object_prefix = Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t)
+  type object_prefix = {
+    obj_dir : DirPath.t;
+    obj_mp  : ModPath.t;
+    obj_sec : DirPath.t;
+  }
 
   module Dirset : Set.S with type elt = DirPath.t
   module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 707adce30..c69be4f4d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -46,9 +46,9 @@ We changed the type of the following functions:
 
 - `Global.body_of_constant`: same as above.
 
-We renamed the following datatypes:
+We have changed the representation of the following types:
 
-- `Pp.std_ppcmds` -> `Pp.t`
+- `Lib.object_prefix` is now a record instead of a nested tuple.
 
 Some tactics and related functions now support static configurability, e.g.:
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index db83dafef..41e00a41c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -180,16 +180,16 @@ let compute_visibility exists i =
 
 (** Iterate some function [iter_objects] on all components of a module *)
 
-let do_module exists iter_objects i dir mp sobjs kobjs =
-  let prefix = (dir,(mp,DirPath.empty)) in
+let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
+  let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
   let dirinfo = DirModule prefix in
-  consistency_checks exists dir dirinfo;
-  Nametab.push_dir (compute_visibility exists i) dir dirinfo;
-  ModSubstObjs.set mp sobjs;
+  consistency_checks exists obj_dir dirinfo;
+  Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
+  ModSubstObjs.set obj_mp sobjs;
   (* If we're not a functor, let's iter on the internal components *)
   if sobjs_no_functor sobjs then begin
     let objs = expand_sobjs sobjs in
-    ModObjs.set mp (prefix,objs,kobjs);
+    ModObjs.set obj_mp (prefix,objs,kobjs);
     iter_objects (i+1) prefix objs;
     iter_objects (i+1) prefix kobjs
   end
@@ -222,20 +222,20 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!")
 
 let load_keep i ((sp,kn),kobjs) =
   (* Invariant : seg isn't empty *)
-  let dir = dir_of_sp sp and mp = mp_of_kn kn in
-  let prefix = (dir,(mp,DirPath.empty)) in
+  let obj_dir = dir_of_sp sp and obj_mp  = mp_of_kn kn in
+  let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
   let prefix',sobjs,kobjs0 =
-    try ModObjs.get mp
+    try ModObjs.get obj_mp
     with Not_found -> assert false (* a substobjs should already be loaded *)
   in
   assert (eq_op prefix' prefix);
   assert (List.is_empty kobjs0);
-  ModObjs.set mp (prefix,sobjs,kobjs);
+  ModObjs.set obj_mp (prefix,sobjs,kobjs);
   Lib.load_objects i prefix kobjs
 
 let open_keep i ((sp,kn),kobjs) =
-  let dir = dir_of_sp sp and mp = mp_of_kn kn in
-  let prefix = (dir,(mp,DirPath.empty)) in
+  let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
+  let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in
   Lib.open_objects i prefix kobjs
 
 let in_modkeep : Lib.lib_objects -> obj =
@@ -284,9 +284,9 @@ let (in_modtype : substitutive_objects -> obj),
 (** {6 Declaration of substitutive objects for Include} *)
 
 let do_include do_load do_open i ((sp,kn),aobjs) =
-  let dir = Libnames.dirpath sp in
-  let mp = KerName.modpath kn in
-  let prefix = (dir,(mp,DirPath.empty)) in
+  let obj_dir = Libnames.dirpath sp in
+  let obj_mp = KerName.modpath kn in
+  let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in
   let o = expand_aobjs aobjs in
   if do_load then Lib.load_objects i prefix o;
   if do_open then Lib.open_objects i prefix o
@@ -577,7 +577,7 @@ let start_module interp_modast export id args res fs =
   in
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
-  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
+  Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModule prefix);
   mp
 
 let end_module () =
@@ -684,7 +684,7 @@ let start_modtype interp_modast id args mtys fs =
   let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in
   openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
-  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
+  Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix);
   mp
 
 let end_modtype () =
diff --git a/library/lib.ml b/library/lib.ml
index 3dbb16c7b..499e2ae21 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -93,12 +93,16 @@ let segment_of_objects prefix =
    sections, but on the contrary there are many constructions of section
    paths based on the library path. *)
 
-let initial_prefix = default_library,(Names.ModPath.initial,Names.DirPath.empty)
+let initial_prefix = {
+  obj_dir = default_library;
+  obj_mp  = ModPath.initial;
+  obj_sec = DirPath.empty;
+}
 
 type lib_state = {
-  comp_name   : Names.DirPath.t option;
+  comp_name   : DirPath.t option;
   lib_stk     : library_segment;
-  path_prefix : Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t);
+  path_prefix : object_prefix;
 }
 
 let initial_lib_state = {
@@ -115,10 +119,9 @@ let library_dp () =
 (* [path_prefix] is a pair of absolute dirpath and a pair of current
    module path and relative section path *)
 
-let cwd () = fst !lib_state.path_prefix
-let current_prefix () = snd !lib_state.path_prefix
-let current_mp () = fst (snd !lib_state.path_prefix)
-let current_sections () = snd (snd !lib_state.path_prefix)
+let cwd () = !lib_state.path_prefix.obj_dir
+let current_mp () = !lib_state.path_prefix.obj_mp
+let current_sections () = !lib_state.path_prefix.obj_sec
 
 let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
 let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
@@ -136,7 +139,7 @@ let make_path_except_section id =
   Libnames.make_path (cwd_except_section ()) id
 
 let make_kn id =
-  let mp,dir = current_prefix () in
+  let mp, dir = current_mp (), current_sections () in
   Names.KerName.make mp dir (Names.Label.of_id id)
 
 let make_oname id = Libnames.make_oname !lib_state.path_prefix id
@@ -152,8 +155,11 @@ let recalc_path_prefix () =
   lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk }
 
 let pop_path_prefix () =
-  let dir,(mp,sec) = !lib_state.path_prefix in
-  lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)}
+  let op = !lib_state.path_prefix in
+  lib_state := { !lib_state
+                 with path_prefix = { op with obj_dir = pop_dirpath op.obj_dir;
+                                              obj_sec = pop_dirpath op.obj_sec;
+                                    } }
 
 let find_entry_p p =
   let rec find = function
@@ -226,7 +232,7 @@ let add_anonymous_entry node =
   add_entry (make_oname (anonymous_id ())) node
 
 let add_leaf id obj =
-  if Names.ModPath.equal (current_mp ()) Names.ModPath.initial then
+  if ModPath.equal (current_mp ()) ModPath.initial then
     user_err Pp.(str "No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
@@ -278,8 +284,8 @@ let current_mod_id () =
 
 
 let start_mod is_type export id mp fs =
-  let dir = add_dirpath_suffix (cwd ()) id in
-  let prefix = dir,(mp,Names.DirPath.empty) in
+  let dir = add_dirpath_suffix (!lib_state.path_prefix.obj_dir) id in
+  let prefix = { obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
   let exists =
     if is_type then Nametab.exists_cci (make_path id)
     else Nametab.exists_module dir
@@ -328,10 +334,10 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
 let start_compilation s mp =
   if !lib_state.comp_name != None then
     user_err Pp.(str "compilation unit is already started");
-  if not (Names.DirPath.is_empty (current_sections ())) then
+  if not (Names.DirPath.is_empty (!lib_state.path_prefix.obj_sec)) then
     user_err Pp.(str "some sections are already opened");
-  let prefix = s, (mp, Names.DirPath.empty) in
-  let () = add_anonymous_entry (CompilingLibrary prefix) in
+  let prefix = Libnames.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
+  add_anonymous_entry (CompilingLibrary prefix);
   lib_state := { !lib_state with comp_name = Some s;
                                  path_prefix = prefix }
 
@@ -522,15 +528,15 @@ let is_in_section ref =
 (*************)
 (* Sections. *)
 let open_section id =
-  let olddir,(mp,oldsec) = !lib_state.path_prefix in
-  let dir = add_dirpath_suffix olddir id in
-  let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
-  if Nametab.exists_section dir then
+  let opp = !lib_state.path_prefix in
+  let obj_dir = add_dirpath_suffix opp.obj_dir id in
+  let prefix = { obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
+  if Nametab.exists_section obj_dir then
     user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:`No in
   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);
+  Nametab.push_dir (Nametab.Until 1) obj_dir (DirOpenSection prefix);
   lib_state := { !lib_state with path_prefix = prefix };
   add_section ()
 
@@ -556,7 +562,7 @@ let close_section () =
   in
   let (secdecls,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
-  let full_olddir = fst !lib_state.path_prefix in
+  let full_olddir = !lib_state.path_prefix.obj_dir in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
   let newdecls = List.map discharge_item secdecls in
@@ -596,10 +602,10 @@ let init () =
 (* Misc *)
 
 let mp_of_global = function
-  |VarRef id -> current_mp ()
-  |ConstRef cst -> Names.Constant.modpath cst
-  |IndRef ind -> Names.ind_modpath ind
-  |ConstructRef constr -> Names.constr_modpath constr
+  | VarRef id -> !lib_state.path_prefix.obj_mp
+  | ConstRef cst -> Names.Constant.modpath cst
+  | IndRef ind -> Names.ind_modpath ind
+  | ConstructRef constr -> Names.constr_modpath constr
 
 let rec dp_of_mp = function
   |Names.MPfile dp -> dp
diff --git a/library/libnames.ml b/library/libnames.ml
index 81878e72f..a471d8396 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -156,10 +156,15 @@ let qualid_of_dirpath dir =
 
 type object_name = full_path * KerName.t
 
-type object_prefix = DirPath.t * (ModPath.t * DirPath.t)
+type object_prefix = {
+  obj_dir : DirPath.t;
+  obj_mp  : ModPath.t;
+  obj_sec : DirPath.t;
+}
 
-let make_oname (dirpath,(mp,dir)) id =
-  make_path dirpath id, KerName.make mp dir (Label.of_id id)
+(* let make_oname (dirpath,(mp,dir)) id = *)
+let make_oname { obj_dir; obj_mp; obj_sec } id =
+  make_path obj_dir id, KerName.make obj_mp obj_sec (Label.of_id id)
 
 (* to this type are mapped DirPath.t's in the nametab *)
 type global_dir_reference =
@@ -170,10 +175,10 @@ type global_dir_reference =
   | DirClosedSection of DirPath.t
       (* this won't last long I hope! *)
 
-let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
-  DirPath.equal d1 d2 &&
-  DirPath.equal p1 p2 &&
-  ModPath.equal mp1 mp2
+let eq_op op1 op2 =
+  DirPath.equal op1.obj_dir op2.obj_dir &&
+  DirPath.equal op1.obj_sec op2.obj_sec &&
+  ModPath.equal op1.obj_mp  op2.obj_mp
 
 let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
diff --git a/library/libnames.mli b/library/libnames.mli
index ed01163ee..71f542240 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -94,7 +94,25 @@ val qualid_of_ident : Id.t -> qualid
 
 type object_name = full_path * KerName.t
 
-type object_prefix = DirPath.t * (ModPath.t * DirPath.t)
+(** Object prefix morally contains the "prefix" naming of an object to
+   be stored by [library], where [obj_dir] is the "absolute" path,
+   [obj_mp] is the current "module" prefix and [obj_sec] is the
+   "section" prefix.
+
+    Thus, for an object living inside [Module A. Section B.] the
+   prefix would be:
+
+    [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ]
+
+    Note that both [obj_dir] and [obj_sec] are "paths" that is to say,
+   as opposed to [obj_mp] which is a single module name.
+
+ *)
+type object_prefix = {
+  obj_dir : DirPath.t;
+  obj_mp  : ModPath.t;
+  obj_sec : DirPath.t;
+}
 
 val eq_op : object_prefix -> object_prefix -> bool
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 0ec4a37cd..222c4cedc 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -359,8 +359,8 @@ let push_modtype vis sp kn =
 let push_dir vis dir dir_ref =
   the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
   match dir_ref with
-      DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab
-    | _ -> ()
+  | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab
+  | _ -> ()
 
 
 (* Locate functions *******************************************************)
@@ -386,17 +386,17 @@ let locate_dir qid = DirTab.locate qid !the_dirtab
 
 let locate_module qid =
   match locate_dir qid with
-    | DirModule (_,(mp,_)) -> mp
+    | DirModule { obj_mp ; _} -> obj_mp
     | _ -> raise Not_found
 
 let full_name_module qid =
   match locate_dir qid with
-    | DirModule (dir,_) -> dir
+    | DirModule { obj_dir ; _} -> obj_dir
     | _ -> raise Not_found
 
 let locate_section qid =
   match locate_dir qid with
-    | DirOpenSection (dir, _)
+    | DirOpenSection { obj_dir; _ } -> obj_dir
     | DirClosedSection dir -> dir
     | _ -> raise Not_found
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8fc00ed96..8b21ff761 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -359,10 +359,10 @@ let pr_located_qualid = function
       str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
   | Dir dir ->
       let s,dir = match dir with
-	| DirOpenModule (dir,_) -> "Open Module", dir
-	| DirOpenModtype (dir,_) -> "Open Module Type", dir
-	| DirOpenSection (dir,_) -> "Open Section", dir
-	| DirModule (dir,_) -> "Module", dir
+        | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir
+        | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir
+        | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir
+        | DirModule { obj_dir ; _ } -> "Module", obj_dir
 	| DirClosedSection dir -> "Closed Section", dir
       in
       str s ++ spc () ++ DirPath.print dir
@@ -409,7 +409,7 @@ let locate_term qid =
 let locate_module qid =
   let all = Nametab.locate_extended_all_dir qid in
   let map dir = match dir with
-  | DirModule (_, (mp, _)) -> Some (Dir dir, Nametab.shortest_qualid_of_module mp)
+  | DirModule { obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp)
   | DirOpenModule _ -> Some (Dir dir, qid)
   | _ -> None
   in
@@ -645,8 +645,8 @@ let gallina_print_library_entry env sigma with_values ent =
         Some (str " >>>>>>> Section " ++ pr_name oname)
     | (oname,Lib.ClosedSection _) ->
         Some (str " >>>>>>> Closed Section " ++ pr_name oname)
-    | (_,Lib.CompilingLibrary (dir,_)) ->
-        Some (str " >>>>>>> Library " ++ DirPath.print dir)
+    | (_,Lib.CompilingLibrary { obj_dir; _ }) ->
+        Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
     | (oname,Lib.OpenedModule _) ->
 	Some (str " >>>>>>> Module " ++ pr_name oname)
     | (oname,Lib.ClosedModule _) ->
@@ -775,8 +775,8 @@ let read_sec_context r =
     with Not_found ->
       user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in
   let rec get_cxt in_cxt = function
-    | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
-        if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+    | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest ->
+        if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | (_,Lib.ClosedSection _)::rest ->
         user_err Pp.(str "Cannot print the contents of a closed section.")
 	(* LEM: Actually, we could if we wanted to. *)
@@ -798,7 +798,7 @@ let print_any_name env sigma = function
   | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
   | Term (VarRef sp) -> print_section_variable env sigma sp
   | Syntactic kn -> print_syntactic_def env kn
-  | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
+  | Dir (DirModule { obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp
   | Dir _ -> mt ()
   | ModuleType mp -> print_modtype mp
   | Other (obj, info) -> info.print obj
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 13a03e9b4..dd2e99d58 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -237,10 +237,10 @@ let print_kn locals kn =
 	with
 	    Not_found -> print_modpath locals kn
 
-let nametab_register_dir mp =
+let nametab_register_dir obj_mp =
   let id = mk_fake_top () in
-  let dir = DirPath.make [id] in
-  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty)))
+  let obj_dir = DirPath.make [id] in
+  Nametab.push_dir (Nametab.Until 1) obj_dir (DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty })
 
 (** Nota: the [global_reference] we register in the nametab below
     might differ from internal ones, since we cannot recreate here
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bdd351901..c5653ceb7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -185,8 +185,8 @@ let print_module r =
   try
     let globdir = Nametab.locate_dir qid in
       match globdir with
-	  DirModule (dirpath,(mp,_)) ->
-	    Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
+          DirModule { obj_dir; obj_mp; _ } ->
+            Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp)
 	| _ -> raise Not_found
   with
       Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid)