Modulification of dir_path

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

1 files changed, 70 insertions, 28 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index c0b38666b0..2f8445ef6f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -56,31 +56,48 @@ end
 
 type name = Name of Id.t | Anonymous
 type variable = Id.t
+type module_ident = Id.t
 
 val name_eq : name -> name -> bool
 
 (** {6 Directory paths = section names paths } *)
 
-type module_ident = Id.t
-module ModIdmap : Map.S with type key = module_ident
+module Dir_path :
+sig
+  type t
+  (** Type of directory paths. Essentially a list of module identifiers. The
+      order is reversed to improve sharing. E.g. A.B.C is ["C";"B";"A"] *)
 
-type dir_path
+  val equal : t -> t -> bool
+  (** Equality over directory paths. *)
 
-val dir_path_ord : dir_path -> dir_path -> int
+  val compare : t -> t -> int
+  (** Comparison over directory paths. *)
 
-val dir_path_eq : dir_path -> dir_path -> bool
+  val make : module_ident list -> t
+  (** Create a directory path. (The list must be reversed). *)
 
-(** Inner modules idents on top of list (to improve sharing).
-   For instance: A.B.C is ["C";"B";"A"] *)
-val make_dirpath : module_ident list -> dir_path
-val repr_dirpath : dir_path -> module_ident list
+  val repr : t -> module_ident list
+  (** Represent a directory path. (The result list is reversed). *)
 
-val empty_dirpath : dir_path
+  val empty : t
+  (** The empty directory path. *)
 
-val is_empty_dirpath : dir_path -> bool
+  val is_empty : t -> bool
+  (** Test whether a directory path is empty. *)
 
-(** Printing of directory paths as ["coq_root.module.submodule"] *)
-val string_of_dirpath : dir_path -> string
+  val to_string : t -> string
+  (** Print directory paths as ["coq_root.module.submodule"] *)
+
+  val initial : t
+  (** Initial "seed" of the unique identifier generator *)
+
+  val hcons : t -> t
+  (** Hashconsing of directory paths. *)
+
+end
+
+module ModIdmap : Map.S with type key = module_ident
 
 (** {6 Names of structure elements } *)
 
@@ -108,8 +125,8 @@ val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
 (** The first argument is a file name - to prevent conflict between
    different files *)
 
-val make_mbid : dir_path -> Id.t -> mod_bound_id
-val repr_mbid : mod_bound_id -> int * Id.t * dir_path
+val make_mbid : Dir_path.t -> Id.t -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * Id.t * Dir_path.t
 val id_of_mbid : mod_bound_id -> Id.t
 val debug_string_of_mbid : mod_bound_id -> string
 val string_of_mbid : mod_bound_id -> string
@@ -117,7 +134,7 @@ val string_of_mbid : mod_bound_id -> string
 (** {6 The module part of the kernel name } *)
 
 type module_path =
-  | MPfile of dir_path
+  | MPfile of Dir_path.t
   | MPbound of mod_bound_id
   | MPdot of module_path * label
 
@@ -131,9 +148,6 @@ val string_of_mp : module_path -> string
 module MPset : Set.S with type elt = module_path
 module MPmap : Map.S with type key = module_path
 
-(** Initial "seed" of the unique identifier generator *)
-val initial_dir : dir_path
-
 (** Name of the toplevel structure *)
 val initial_path : module_path (** [= MPfile initial_dir] *)
 
@@ -142,8 +156,8 @@ val initial_path : module_path (** [= MPfile initial_dir] *)
 type kernel_name
 
 (** Constructor and destructor *)
-val make_kn : module_path -> dir_path -> label -> kernel_name
-val repr_kn : kernel_name -> module_path * dir_path * label
+val make_kn : module_path -> Dir_path.t -> label -> kernel_name
+val repr_kn : kernel_name -> module_path * Dir_path.t * label
 
 val modpath : kernel_name -> module_path
 val label : kernel_name -> label
@@ -186,12 +200,12 @@ module Constrmap_env : Map.S with type key = constructor
 
 val constant_of_kn : kernel_name -> constant
 val constant_of_kn_equiv : kernel_name -> kernel_name -> constant
-val make_con : module_path -> dir_path -> label -> constant
-val make_con_equiv : module_path -> module_path -> dir_path 
+val make_con : module_path -> Dir_path.t -> label -> constant
+val make_con_equiv : module_path -> module_path -> Dir_path.t 
   -> label -> constant
 val user_con : constant -> kernel_name
 val canonical_con : constant -> kernel_name
-val repr_con : constant -> module_path * dir_path * label
+val repr_con : constant -> module_path * Dir_path.t * label
 val eq_constant : constant -> constant -> bool
 val con_with_label : constant -> label -> constant
 
@@ -206,12 +220,12 @@ val debug_string_of_con : constant -> string
 
 val mind_of_kn : kernel_name -> mutual_inductive
 val mind_of_kn_equiv : kernel_name -> kernel_name -> mutual_inductive
-val make_mind : module_path -> dir_path -> label -> mutual_inductive
-val make_mind_equiv : module_path -> module_path -> dir_path 
+val make_mind : module_path -> Dir_path.t -> label -> mutual_inductive
+val make_mind_equiv : module_path -> module_path -> Dir_path.t 
   -> label -> mutual_inductive
 val user_mind : mutual_inductive -> kernel_name
 val canonical_mind : mutual_inductive -> kernel_name
-val repr_mind : mutual_inductive -> module_path * dir_path * label
+val repr_mind : mutual_inductive -> module_path * Dir_path.t * label
 val eq_mind : mutual_inductive -> mutual_inductive -> bool
 
 val string_of_mind : mutual_inductive -> string
@@ -244,7 +258,6 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference
 (** {6 Hash-consing } *)
 
 val hcons_name : name -> name
-val hcons_dirpath : dir_path -> dir_path
 val hcons_con : constant -> constant
 val hcons_mind : mutual_inductive -> mutual_inductive
 val hcons_ind : inductive -> inductive
@@ -315,3 +328,32 @@ module Idmap  : sig
   val singleton : key -> 'a -> 'a t
 end
 (** @deprecated Same as [Id.Map]. *)
+
+(** {5 Directory paths} *)
+
+type dir_path = Dir_path.t
+(** @deprecated Alias for [Dir_path.t]. *)
+
+val dir_path_ord : dir_path -> dir_path -> int
+(** @deprecated Same as [Dir_path.compare]. *)
+
+val dir_path_eq : dir_path -> dir_path -> bool
+(** @deprecated Same as [Dir_path.equal]. *)
+
+val make_dirpath : module_ident list -> dir_path
+(** @deprecated Same as [Dir_path.make]. *)
+
+val repr_dirpath : dir_path -> module_ident list
+(** @deprecated Same as [Dir_path.repr]. *)
+
+val empty_dirpath : dir_path
+(** @deprecated Same as [Dir_path.empty]. *)
+
+val is_empty_dirpath : dir_path -> bool
+(** @deprecated Same as [Dir_path.is_empty]. *)
+
+val string_of_dirpath : dir_path -> string
+(** @deprecated Same as [Dir_path.to_string]. *)
+
+val initial_dir : Dir_path.t
+(** @deprecated Same as [Dir_path.initial]. *)