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

14 files changed, 89 insertions, 123 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index aac7f9a28..ab4a6a25c 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -69,8 +69,8 @@ let check_required_library d =
   let dir = make_dir d in
   if Library.library_is_loaded dir then ()
   else
-    let in_current_dir = match Lib.current_prefix () with
-      | MPfile dp, _ -> DirPath.equal dir dp
+    let in_current_dir = match Lib.current_mp () with
+      | MPfile dp -> DirPath.equal dir dp
       | _ -> false
     in
     if not in_current_dir then
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
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7fffc960b..f57832d3f 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -52,7 +52,7 @@ let toplevel_env () =
 
 let environment_until dir_opt =
   let rec parse = function
-    | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
+    | [] when dir_opt = None -> [Lib.current_mp (), toplevel_env ()]
     | [] -> []
     | d :: l ->
       let meb =
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 659ee4ec4..0903f85a0 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1301,9 +1301,8 @@ let inline_test r t =
        not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
-  match DirPath.repr (dirpath_of_string s) with
-    | id :: d -> Constant.make2 (MPfile (DirPath.make d)) (Label.of_id id)
-    | [] -> assert false
+  let d, id = Libnames.split_dirpath (dirpath_of_string s) in
+  Constant.make2 (MPfile d) (Label.of_id id)
 
 let manual_inline_set =
   List.fold_right (fun x -> Cset_env.add (con_of_string x))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2109ba632..66acf23ed 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -58,18 +58,16 @@ let raw_string_of_modfile = function
   | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
-let current_toplevel () = fst (Lib.current_prefix ())
-
 let is_toplevel mp =
-  mp = initial_path || mp = current_toplevel ()
+  ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ())
 
 let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
 let mp_length mp =
-  let mp0 = current_toplevel () in
+  let mp0 = Lib.current_mp () in
   let rec len = function
-    | mp when mp = mp0 -> 1
+    | mp when ModPath.equal mp mp0 -> 1
     | MPdot (mp,_) -> 1 + len mp
     | _ -> 1
   in len mp
@@ -97,7 +95,7 @@ let rec parse_labels2 ll mp1 = function
   | mp -> mp,ll
 
 let labels_of_ref r =
-  let mp_top = current_toplevel () in
+  let mp_top = Lib.current_mp () in
   let mp,_,l = repr_of_r r in
   parse_labels2 [l] mp_top mp
 
@@ -419,8 +417,8 @@ let error_non_implicit msg =
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
       if not (Library.library_is_loaded dp) then begin
-	match base_mp (current_toplevel ()) with
-	  | MPfile dp' when dp<>dp' ->
+	match base_mp (Lib.current_mp ()) with
+	  | MPfile dp' when not (DirPath.equal dp dp') ->
 	      err (str ("Please load library "^(DirPath.to_string dp^" first.")))
 	  | _ -> ()
       end
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index ce6f8e229..91d2531dd 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -49,7 +49,6 @@ val occur_kn_in_ref : mutual_inductive -> global_reference -> bool
 val repr_of_r : global_reference -> module_path * DirPath.t * Label.t
 val modpath_of_r : global_reference -> module_path
 val label_of_r : global_reference -> Label.t
-val current_toplevel : unit -> module_path
 val base_mp : module_path -> module_path
 val is_modfile : module_path -> bool
 val string_of_modfile : module_path -> string
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 857e82fc5..7fbc1b981 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1258,7 +1258,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	  ConstRef c -> is_opaque_constant c
 	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
     in
-    let lemma = mkConst (Lib.make_con na) in
+    let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
     ref_ := Some lemma ;
     let lid = ref [] in
     let h_num = ref (-1) in
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 6145548b2..d065ba61a 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -380,10 +380,7 @@ let print internal glob_ref kind xml_library_root =
    match glob_ref with
       Gn.VarRef id ->
        (* this kn is fake since it is not provided by Coq *)
-       let kn =
-        let (mod_path,dir_path) = Lib.current_prefix () in
-        N.make_kn mod_path dir_path (N.Label.of_id id)
-       in
+       let kn = Lib.make_kn id in
        let (_,body,typ) = G.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Gn.ConstRef kn ->
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index a2fa81750..1736bcff2 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -26,16 +26,14 @@ open Termops
 (**********************************************************************)
 (* Globality of identifiers *)
 
-let is_imported_modpath mp =
-  let current_mp,_ = Lib.current_prefix() in
-    match mp with
-      | MPfile dp ->
-	  let rec find_prefix = function
-	    |MPfile dp1 -> not (DirPath.equal dp1 dp)
-	    |MPdot(mp,_) -> find_prefix mp
-	    |MPbound(_) -> false
-	  in find_prefix current_mp
-      | p -> false
+let is_imported_modpath = function
+  | MPfile dp ->
+    let rec find_prefix = function
+      |MPfile dp1 -> not (DirPath.equal dp1 dp)
+      |MPdot(mp,_) -> find_prefix mp
+      |MPbound(_) -> false
+    in find_prefix (Lib.current_mp ())
+  | _ -> false
 
 let is_imported_ref = function
   | VarRef _ -> false
diff --git a/printing/printer.ml b/printing/printer.ml
index cc9356cda..05037a150 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -144,12 +144,11 @@ let id_of_global env = function
     (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
   | VarRef v -> v
 
-let cons_dirpath id dp = DirPath.make (id :: DirPath.repr dp)
-
 let rec dirpath_of_mp = function
   | MPfile sl -> sl
   | MPbound uid -> DirPath.make [MBId.to_id uid]
-  | MPdot (mp,l) -> cons_dirpath (Label.to_id l) (dirpath_of_mp mp)
+  | MPdot (mp,l) ->
+    Libnames.add_dirpath_suffix (dirpath_of_mp mp) (Label.to_id l)
 
 let dirpath_of_global = function
   | ConstRef kn -> dirpath_of_mp (Constant.modpath kn)