Modulification of mod_bound_id

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

10 files changed, 188 insertions, 126 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index e2ebce28a..6b793ce2f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -389,7 +389,7 @@ and structure_body = (Label.t * structure_field_body) list
 
 and struct_expr_body =
   | SEBident of module_path
-  | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
+  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
   | SEBapply of struct_expr_body * struct_expr_body * constraints
   | SEBstruct of structure_body
   | SEBwith of struct_expr_body * with_declaration_body
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3b43baa79..2595aae07 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -202,7 +202,7 @@ and structure_body = (Label.t * structure_field_body) list
 
 and struct_expr_body =
   | SEBident of module_path
-  | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
+  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
   | SEBapply of struct_expr_body * struct_expr_body * constraints
   | SEBstruct of structure_body
   | SEBwith of struct_expr_body * with_declaration_body
diff --git a/kernel/entries.mli b/kernel/entries.mli
index db91ff597..a32892a41 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -68,7 +68,7 @@ type constant_entry =
 
 type module_struct_entry =
     MSEident of module_path
-  | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
+  | MSEfunctor of MBId.t * module_struct_entry * module_struct_entry
   | MSEwith of module_struct_entry * with_declaration
   | MSEapply of module_struct_entry * module_struct_entry
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 5af6bd5bb..867de2a0b 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -51,8 +51,8 @@ let empty_delta_resolver = Deltamap.empty
 
 module MBImap = Map.Make
   (struct
-    type t = mod_bound_id
-    let compare = mod_bound_id_ord
+    type t = MBId.t
+    let compare = MBId.compare
    end)
 
 module Umap = struct
@@ -94,7 +94,7 @@ let debug_string_of_delta resolve =
 let list_contents sub =
   let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in
   let mp_one_pair mp0 p l = (string_of_mp mp0, one_pair p)::l in
-  let mbi_one_pair mbi p l = (debug_string_of_mbid mbi, one_pair p)::l in
+  let mbi_one_pair mbi p l = (MBId.debug_to_string mbi, one_pair p)::l in
   Umap.fold mp_one_pair mbi_one_pair sub []
 
 let debug_string_of_subst sub =
@@ -524,13 +524,13 @@ let join subst1 subst2 =
   Umap.join subst2 subst
 
 let rec occur_in_path mbi = function
-  | MPbound bid' -> mod_bound_id_eq mbi bid'
+  | MPbound bid' -> MBId.equal mbi bid'
   | MPdot (mp1,_) -> occur_in_path mbi mp1
   | _ -> false
 
 let occur_mbid mbi sub =
   let check_one mbi' (mp,_) =
-    if mod_bound_id_eq mbi mbi' || occur_in_path mbi mp then raise Exit
+    if MBId.equal mbi mbi' || occur_in_path mbi mp then raise Exit
   in
   try
     Umap.iter_mbi check_one sub;
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 21b6bf93b..f3c490652 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -62,13 +62,13 @@ val is_empty_subst : substitution -> bool
 (** add_* add [arg2/arg1]\{arg3\} to the substitution with no
    sequential composition  *)
 val add_mbid :
-  mod_bound_id -> module_path -> delta_resolver  -> substitution -> substitution
+  MBId.t -> module_path -> delta_resolver  -> substitution -> substitution
 val add_mp :
   module_path -> module_path -> delta_resolver -> substitution -> substitution
 
 (** map_* create a new substitution [arg2/arg1]\{arg3\} *)
 val map_mbid :
-  mod_bound_id -> module_path -> delta_resolver -> substitution
+  MBId.t -> module_path -> delta_resolver -> substitution
 val map_mp :
   module_path -> module_path -> delta_resolver -> substitution
 
@@ -136,7 +136,7 @@ val subst_mps : substitution -> constr -> constr
 (** [occur_*id id sub] returns true iff [id] occurs in [sub]
    on either side *)
 
-val occur_mbid : mod_bound_id -> substitution -> bool
+val occur_mbid : MBId.t -> substitution -> bool
 
 (** [repr_substituted r] dumps the representation of a substituted:
     - [None, a] when r is a value
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 13129cdbd..c90425fd7 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -22,7 +22,7 @@ val module_type_of_module : module_path option -> module_body ->
   module_type_body
 
 val destr_functor :
-  env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body
+  env -> struct_expr_body -> MBId.t * module_type_body * struct_expr_body
 
 val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
 
@@ -39,7 +39,7 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit
 val strengthen : module_type_body -> module_path -> module_type_body
 
 val inline_delta_resolver :
-  env -> inline -> module_path -> mod_bound_id -> module_type_body ->
+  env -> inline -> module_path -> MBId.t -> module_type_body ->
   delta_resolver -> delta_resolver
 
 val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body
diff --git a/kernel/names.ml b/kernel/names.ml
index 9b41fed1f..c6f5f891c 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -74,23 +74,6 @@ struct
 
 end
 
-(** Backward compatibility for [Id.t] *)
-
-type identifier = Id.t
-
-let id_eq = Id.equal
-let id_ord = Id.compare
-let check_ident_soft = Id.check_soft
-let check_ident = Id.check
-let string_of_id = Id.to_string
-let id_of_string = Id.of_string
-
-module Idset = Id.Set
-module Idmap = Id.Map
-module Idpred = Id.Pred
-
-(** / End of backward compatibility *)
-
 (** {6 Various types based on identifiers } *)
 
 type name = Name of Id.t | Anonymous
@@ -103,7 +86,7 @@ let name_eq n1 n2 = match n1, n2 with
 
 type module_ident = Id.t
 
-module ModIdmap = Idmap
+module ModIdmap = Id.Map
 
 (** {6 Directory paths = section names paths } *)
 
@@ -164,58 +147,61 @@ struct
 
 end
 
-(** Compatibility layer for [Dir_path] *)
+(** {6 Unique names for bound modules } *)
 
-type dir_path = Dir_path.t
-let dir_path_ord = Dir_path.compare
-let dir_path_eq = Dir_path.equal
-let make_dirpath = Dir_path.make
-let repr_dirpath = Dir_path.repr
-let empty_dirpath = Dir_path.empty
-let is_empty_dirpath = Dir_path.is_empty
-let string_of_dirpath = Dir_path.to_string
-let initial_dir = Dir_path.initial
+module MBId =
+struct
+  type t = int * Id.t * Dir_path.t
 
-(** / End of compatibility layer for [Dir_path] *)
+  let gen =
+    let seed = ref 0 in fun () ->
+      let ans = !seed in
+      let () = incr seed in
+      ans
 
-(** {6 Unique names for bound modules } *)
+  let make dir s = (gen(), s, dir)
+
+  let repr mbid = mbid
 
-let u_number = ref 0
-type uniq_ident = int * Id.t * Dir_path.t
-let make_uid dir s = incr u_number;(!u_number,s,dir)
- let debug_string_of_uid (i,s,p) =
- "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
-let string_of_uid (i,s,p) =
-  string_of_dirpath p ^"."^s
-
-let uniq_ident_ord (x : uniq_ident) (y : uniq_ident) =
-  if x == y then 0
-  else match (x, y) with
-  | (nl, idl, dpl), (nr, idr, dpr) ->
-    let ans = Int.compare nl nr in
-    if not (Int.equal ans 0) then ans
-    else
-      let ans = Id.compare idl idr in
+  let to_string (i, s, p) =
+    Dir_path.to_string p ^ "." ^ s
+
+  let debug_to_string (i, s, p) =
+    "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
+
+  let compare (x : t) (y : t) =
+    if x == y then 0
+    else match (x, y) with
+    | (nl, idl, dpl), (nr, idr, dpr) ->
+      let ans = Int.compare nl nr in
       if not (Int.equal ans 0) then ans
       else
-        Dir_path.compare dpl dpr
+        let ans = Id.compare idl idr in
+        if not (Int.equal ans 0) then ans
+        else
+          Dir_path.compare dpl dpr
 
-module UOrdered =
-struct
-  type t = uniq_ident
-  let compare = uniq_ident_ord
-end
+  let equal x y = Int.equal (compare x y) 0
+
+  let to_id (_, s, _) = s
+
+  module Self_Hashcons =
+    struct
+      type _t = t
+      type t = _t
+      type u = (Id.t -> Id.t) * (Dir_path.t -> Dir_path.t)
+      let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
+      let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
+        (x == y) ||
+        (Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
+      let hash = Hashtbl.hash
+    end
 
-module Umap = Map.Make(UOrdered)
+  module HashMBId = Hashcons.Make(Self_Hashcons)
 
-type mod_bound_id = uniq_ident
-let mod_bound_id_ord = uniq_ident_ord
-let mod_bound_id_eq mbl mbr = Int.equal (uniq_ident_ord mbl mbr) 0
-let make_mbid = make_uid
-let repr_mbid (n, id, dp) = (n, id, dp)
-let debug_string_of_mbid = debug_string_of_uid
-let string_of_mbid = string_of_uid
-let id_of_mbid (_,s,_) = s
+  let hcons = Hashcons.simple_hcons HashMBId.generate (Id.hcons, Dir_path.hcons)
+
+end
 
 (** {6 Names of structure elements } *)
 
@@ -227,24 +213,11 @@ struct
   let to_id id = id
 end
 
-(** Compatibility layer for [Label] *)
-
-type label = Id.t
-
-let mk_label = Label.make
-let string_of_label = Label.to_string
-let pr_label = Label.print
-let id_of_label = Label.to_id
-let label_of_id = Label.of_id
-let eq_label = Label.equal
-
-(** / End of compatibility layer for [Label] *)
-
 (** {6 The module part of the kernel name } *)
 
 type module_path =
   | MPfile of Dir_path.t
-  | MPbound of mod_bound_id
+  | MPbound of MBId.t
   | MPdot of module_path * Label.t
 
 let rec check_bound_mp = function
@@ -253,8 +226,8 @@ let rec check_bound_mp = function
   | _ -> false
 
 let rec string_of_mp = function
-  | MPfile sl -> string_of_dirpath sl
-  | MPbound uid -> string_of_uid uid
+  | MPfile sl -> Dir_path.to_string sl
+  | MPbound uid -> MBId.to_string uid
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l
 
 (** we compare labels first if both are MPdots *)
@@ -264,7 +237,7 @@ let rec mp_ord mp1 mp2 =
   | MPfile p1, MPfile p2 ->
     Dir_path.compare p1 p2
   | MPbound id1, MPbound id2 ->
-    uniq_ident_ord id1 id2
+    MBId.compare id1 id2
   | MPdot (mp1, l1), MPdot (mp2, l2) ->
       let c = String.compare l1 l2 in
         if not (Int.equal c 0) then c
@@ -302,7 +275,7 @@ let label kn =
 let string_of_kn (mp,dir,l) =
   let str_dir = match dir with
   | [] -> "."
-  | _ -> "#" ^ string_of_dirpath dir ^ "#"
+  | _ -> "#" ^ Dir_path.to_string dir ^ "#"
   in
   string_of_mp mp ^ str_dir ^ Label.to_string l
 
@@ -491,21 +464,10 @@ module Hname = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-module Huniqid = Hashcons.Make(
-  struct
-    type t = uniq_ident
-    type u = (Id.t -> Id.t) * (Dir_path.t -> Dir_path.t)
-    let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
-    let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
-      (x == y) ||
-      (Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
-    let hash = Hashtbl.hash
-  end)
-
 module Hmod = Hashcons.Make(
   struct
     type t = module_path
-    type u = (Dir_path.t -> Dir_path.t) * (uniq_ident -> uniq_ident) *
+    type u = (Dir_path.t -> Dir_path.t) * (MBId.t -> MBId.t) *
 	(string -> string)
     let rec hashcons (hdir,huniqid,hstr as hfuns) = function
       | MPfile dir -> MPfile (hdir dir)
@@ -565,9 +527,8 @@ module Hconstruct = Hashcons.Make(
   end)
 
 let hcons_name = Hashcons.simple_hcons Hname.generate Id.hcons
-let hcons_uid = Hashcons.simple_hcons Huniqid.generate (Id.hcons,Dir_path.hcons)
 let hcons_mp =
-  Hashcons.simple_hcons Hmod.generate (Dir_path.hcons,hcons_uid,String.hcons)
+  Hashcons.simple_hcons Hmod.generate (Dir_path.hcons,MBId.hcons,String.hcons)
 let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,Dir_path.hcons,String.hcons)
 let hcons_con = Hashcons.simple_hcons Hcn.generate hcons_kn
 let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn
@@ -577,12 +538,12 @@ let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind
 
 (*******)
 
-type transparent_state = Idpred.t * Cpred.t
+type transparent_state = Id.Pred.t * Cpred.t
 
-let empty_transparent_state = (Idpred.empty, Cpred.empty)
-let full_transparent_state = (Idpred.full, Cpred.full)
-let var_full_transparent_state = (Idpred.full, Cpred.empty)
-let cst_full_transparent_state = (Idpred.empty, Cpred.full)
+let empty_transparent_state = (Id.Pred.empty, Cpred.empty)
+let full_transparent_state = (Id.Pred.full, Cpred.full)
+let var_full_transparent_state = (Id.Pred.full, Cpred.empty)
+let cst_full_transparent_state = (Id.Pred.empty, Cpred.full)
 
 type 'a tableKey =
   | ConstKey of constant
@@ -611,3 +572,62 @@ let eq_id_key ik1 ik2 =
 let eq_con_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0
 let eq_mind_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0
 let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
+
+(** Compatibility layers *)
+
+(** Backward compatibility for [Id.t] *)
+
+type identifier = Id.t
+
+let id_eq = Id.equal
+let id_ord = Id.compare
+let check_ident_soft = Id.check_soft
+let check_ident = Id.check
+let string_of_id = Id.to_string
+let id_of_string = Id.of_string
+
+module Idset = Id.Set
+module Idmap = Id.Map
+module Idpred = Id.Pred
+
+(** / End of backward compatibility *)
+
+(** Compatibility layer for [Dir_path] *)
+
+type dir_path = Dir_path.t
+let dir_path_ord = Dir_path.compare
+let dir_path_eq = Dir_path.equal
+let make_dirpath = Dir_path.make
+let repr_dirpath = Dir_path.repr
+let empty_dirpath = Dir_path.empty
+let is_empty_dirpath = Dir_path.is_empty
+let string_of_dirpath = Dir_path.to_string
+let initial_dir = Dir_path.initial
+
+(** / End of compatibility layer for [Dir_path] *)
+
+(** Compatibility layer for [MBId] *)
+
+type mod_bound_id = MBId.t
+let mod_bound_id_ord = MBId.compare
+let mod_bound_id_eq = MBId.equal
+let make_mbid = MBId.make
+let repr_mbid = MBId.repr
+let debug_string_of_mbid = MBId.debug_to_string
+let string_of_mbid = MBId.to_string
+let id_of_mbid = MBId.to_id
+
+(** / End of compatibility layer for [MBId] *)
+
+(** Compatibility layer for [Label] *)
+
+type label = Id.t
+
+let mk_label = Label.make
+let string_of_label = Label.to_string
+let pr_label = Label.print
+let id_of_label = Label.to_id
+let label_of_id = Label.of_id
+let eq_label = Label.equal
+
+(** / End of compatibility layer for [Label] *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 78d2d6216..947b9e3fd 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -132,27 +132,43 @@ sig
 
 end
 
-(** {6 Unique names for bound modules } *)
+(** {6 Unique names for bound modules} *)
 
-type mod_bound_id
+module MBId :
+sig
+  type t
+  (** Unique names for bound modules. Each call to [make] constructs a fresh
+      unique identifier. *)
 
-val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
-val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
+  val equal : t -> t -> bool
+  (** Equality over unique bound names. *)
 
-(** The first argument is a file name - to prevent conflict between
-   different files *)
+  val compare : t -> t -> int
+  (** Comparison over unique bound names. *)
 
-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
+  val make : Dir_path.t -> Id.t -> t
+  (** The first argument is a file name, to prevent conflict between different
+      files. *)
+
+  val repr : t -> int * Id.t * Dir_path.t
+  (** Reverse of [make]. *)
+
+  val to_id : t -> Id.t
+  (** Return the identifier contained in the argument. *)
+
+  val to_string : t -> string
+  (** Conversion to a string. *)
+
+  val debug_to_string : t -> string
+  (** Same as [to_string], but outputs information related to debug. *)
+
+end
 
 (** {6 The module part of the kernel name } *)
 
 type module_path =
   | MPfile of Dir_path.t
-  | MPbound of mod_bound_id
+  | MPbound of MBId.t
   | MPdot of module_path * Label.t
 
 val mp_ord : module_path -> module_path -> int
@@ -397,3 +413,29 @@ val id_of_label : label -> Id.t
 
 val eq_label : label -> label -> bool
 (** @deprecated Same as [Label.equal]. *)
+
+(** {5 Unique bound module names} *)
+
+type mod_bound_id = MBId.t
+(** Alias type. *)
+
+val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
+(** @deprecated Same as [MBId.compare]. *)
+
+val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
+(** @deprecated Same as [MBId.equal]. *)
+
+val make_mbid : Dir_path.t -> Id.t -> mod_bound_id
+(** @deprecated Same as [MBId.make]. *)
+
+val repr_mbid : mod_bound_id -> int * Id.t * Dir_path.t
+(** @deprecated Same as [MBId.repr]. *)
+
+val id_of_mbid : mod_bound_id -> Id.t
+(** @deprecated Same as [MBId.to_id]. *)
+
+val string_of_mbid : mod_bound_id -> string
+(** @deprecated Same as [MBId.to_string]. *)
+
+val debug_string_of_mbid : mod_bound_id -> string
+(** @deprecated Same as [MBId.debug_to_string]. *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 823047974..412ccfa31 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -74,8 +74,8 @@ open Mod_subst
 
 type modvariant =
   | NONE
-  | SIG of (* funsig params *) (mod_bound_id * module_type_body) list
-  | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
+  | SIG of (* funsig params *) (MBId.t * module_type_body) list
+  | STRUCT of (* functor params *) (MBId.t * module_type_body) list
   | LIBRARY of Dir_path.t
 
 type module_info =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 0add7109a..8f86123c0 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -79,7 +79,7 @@ val end_module :
       -> safe_environment -> module_path * delta_resolver * safe_environment 
 
 val add_module_parameter :
-  mod_bound_id -> module_struct_entry -> inline -> safe_environment -> delta_resolver * safe_environment
+  MBId.t -> module_struct_entry -> inline -> safe_environment -> delta_resolver * safe_environment
 
 val start_modtype :
   Label.t -> safe_environment -> module_path * safe_environment