aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/declarations.ml4
-rw-r--r--checker/declarations.mli6
-rw-r--r--checker/indtypes.ml4
-rw-r--r--checker/modops.mli2
-rw-r--r--dev/top_printers.ml2
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declarations.mli2
-rw-r--r--kernel/entries.mli2
-rw-r--r--kernel/mod_subst.ml10
-rw-r--r--kernel/mod_subst.mli6
-rw-r--r--kernel/modops.mli4
-rw-r--r--kernel/names.ml216
-rw-r--r--kernel/names.mli66
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--library/declaremods.ml10
-rw-r--r--library/declaremods.mli4
-rw-r--r--library/global.mli2
-rw-r--r--library/globnames.ml4
-rw-r--r--library/lib.ml4
-rw-r--r--plugins/extraction/common.ml4
-rw-r--r--plugins/extraction/miniml.mli4
-rw-r--r--printing/ppvernac.ml2
-rw-r--r--printing/printmod.ml8
24 files changed, 218 insertions, 156 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 7e368dcad..c74c95dff 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -58,7 +58,7 @@ let empty_delta_resolver = Deltamap.empty
module MBImap = Map.Make
(struct
- type t = mod_bound_id
+ type t = MBId.t
let compare = Pervasives.compare
end)
@@ -758,7 +758,7 @@ and structure_body = (label * 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 * Univ.constraints
| SEBstruct of structure_body
| SEBwith of struct_expr_body * with_declaration_body
diff --git a/checker/declarations.mli b/checker/declarations.mli
index c14d8b73a..ad234a3f5 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -185,7 +185,7 @@ and structure_body = (label * 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 * Univ.constraints
| SEBstruct of structure_body
| SEBwith of struct_expr_body * with_declaration_body
@@ -215,9 +215,9 @@ and module_type_body =
type 'a subst_fun = substitution -> 'a -> 'a
val empty_subst : substitution
-val add_mbid : mod_bound_id -> module_path -> substitution -> substitution
+val add_mbid : MBId.t -> module_path -> substitution -> substitution
val add_mp : module_path -> module_path -> substitution -> substitution
-val map_mbid : mod_bound_id -> module_path -> substitution
+val map_mbid : MBId.t -> module_path -> substitution
val map_mp : module_path -> module_path -> substitution
val mp_in_delta : module_path -> delta_resolver -> bool
val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index d354eb8c4..285be1bc9 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -20,12 +20,12 @@ open Environ
let rec debug_string_of_mp = function
| MPfile sl -> Dir_path.to_string sl
- | MPbound uid -> "bound("^string_of_mbid uid^")"
+ | MPbound uid -> "bound("^MBId.to_string uid^")"
| MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ Label.to_string l
let rec string_of_mp = function
| MPfile sl -> Dir_path.to_string sl
- | MPbound uid -> string_of_mbid uid
+ | MPbound uid -> MBId.to_string uid
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l
let string_of_mp mp =
diff --git a/checker/modops.mli b/checker/modops.mli
index 2a7899f80..ef3bb6fd2 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -23,7 +23,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 add_signature : module_path -> structure_body -> delta_resolver -> env -> env
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index d86f17033..6e1bf92f5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -34,7 +34,7 @@ let pppp x = pp x
(* name printers *)
let ppid id = pp (pr_id id)
let pplab l = pp (pr_lab l)
-let ppmbid mbid = pp (str (debug_string_of_mbid mbid))
+let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
let ppdir dir = pp (pr_dirpath dir)
let ppmp mp = pp(str (string_of_mp mp))
let ppcon con = pp(debug_pr_con con)
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
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 763aa5ffd..0d9ffb29e 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -86,7 +86,7 @@ type 'a annotated = ('a * funct_app_annot)
*)
type substitutive_objects =
- mod_bound_id list * module_path * lib_objects
+ MBId.t list * module_path * lib_objects
(* For each module, we store the following things:
@@ -124,7 +124,7 @@ let modtab_objects =
is a functor) and declared output type *)
let openmod_info =
ref ((MPfile(Dir_path.initial),[],None,[])
- : module_path * mod_bound_id list *
+ : module_path * MBId.t list *
(module_struct_entry * int option) option *
module_type_body list)
@@ -346,7 +346,7 @@ let modtypetab =
(* currently started interactive module type. We remember its arguments
if it is a functor type *)
let openmodtype_info =
- ref ([],[] : mod_bound_id list * module_type_body list)
+ ref ([],[] : MBId.t list * module_type_body list)
let _ = Summary.declare_summary "MODTYPE-INFO"
{ Summary.freeze_function = (fun () ->
@@ -529,7 +529,7 @@ let rec seb2mse = function
| _ -> failwith "seb2mse: received a non-atomic seb"
let process_module_seb_binding mbid seb =
- process_module_bindings [id_of_mbid mbid]
+ process_module_bindings [MBId.to_id mbid]
[mbid,
(seb2mse seb,
{ ann_inline = DefaultInline; ann_scope_subst = [] })]
@@ -537,7 +537,7 @@ let process_module_seb_binding mbid seb =
let intern_args interp_modtype (idl,(arg,ann)) =
let inl = inline_annot ann in
let lib_dir = Lib.library_dp() in
- let mbids = List.map (fun (_,id) -> make_mbid lib_dir id) idl in
+ let mbids = List.map (fun (_,id) -> MBId.make lib_dir id) idl in
let mty = interp_modtype (Global.env()) arg in
let dirs = List.map (fun (_,id) -> Dir_path.make [id]) idl in
let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 650b2cc81..1b661faef 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -152,8 +152,8 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
(** For translator *)
val process_module_bindings : module_ident list ->
- (mod_bound_id * (module_struct_entry annotated)) list -> unit
+ (MBId.t * (module_struct_entry annotated)) list -> unit
(** For Printer *)
val process_module_seb_binding :
- mod_bound_id -> Declarations.struct_expr_body -> unit
+ MBId.t -> Declarations.struct_expr_body -> unit
diff --git a/library/global.mli b/library/global.mli
index d49dd836b..4908d35fb 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -71,7 +71,7 @@ val end_module : Summary.frozen ->Id.t ->
(module_struct_entry * inline) option -> module_path * delta_resolver
val add_module_parameter :
- mod_bound_id -> module_struct_entry -> inline -> delta_resolver
+ MBId.t -> module_struct_entry -> inline -> delta_resolver
val start_modtype : Id.t -> module_path
val end_modtype : Summary.frozen -> Id.t -> module_path
diff --git a/library/globnames.ml b/library/globnames.ml
index c37e370a3..ea002ef58 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -146,8 +146,8 @@ let decode_mind kn =
let rec dir_of_mp = function
| MPfile dir -> Dir_path.repr dir
| MPbound mbid ->
- let _,_,dp = repr_mbid mbid in
- let id = id_of_mbid mbid in
+ let _,_,dp = MBId.repr mbid in
+ let id = MBId.to_id mbid in
id::(Dir_path.repr dp)
| MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
in
diff --git a/library/lib.ml b/library/lib.ml
index 9ac9b7c71..0f2f480cb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -658,13 +658,13 @@ let rec split_mp mp =
| Names.MPdot (prfx, lbl) ->
let mprec, dprec = split_mp prfx in
mprec, Names.Dir_path.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.Dir_path.repr dprec))
- | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.Dir_path.make [id]
+ | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in library_dp(), Names.Dir_path.make [id]
let split_modpath mp =
let rec aux = function
| Names.MPfile dp -> dp, []
| Names.MPbound mbid ->
- library_dp (), [Names.id_of_mbid 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
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index d8e489be7..286c11e5a 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -343,9 +343,9 @@ let rec mp_renaming_fun mp = match mp with
if lmp = [""] then (modfstlev_rename l)::lmp
else (modular_rename Mod (Label.to_id l))::lmp
| MPbound mbid ->
- let s = modular_rename Mod (id_of_mbid mbid) in
+ let s = modular_rename Mod (MBId.to_id mbid) in
if not (params_ren_mem mp) then [s]
- else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i]
+ else let i,_,_ = MBId.repr mbid in [s^"__"^string_of_int i]
| MPfile _ ->
assert (modular ()); (* see [at_toplevel] above *)
assert (get_phase () = Pre);
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 104a4c865..5aaef254e 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -149,7 +149,7 @@ type ml_specif =
and ml_module_type =
| MTident of module_path
- | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
+ | MTfunsig of MBId.t * ml_module_type * ml_module_type
| MTsig of module_path * ml_module_sig
| MTwith of ml_module_type * ml_with_declaration
@@ -166,7 +166,7 @@ type ml_structure_elem =
and ml_module_expr =
| MEident of module_path
- | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr
+ | MEfunctor of MBId.t * ml_module_type * ml_module_expr
| MEstruct of module_path * ml_module_structure
| MEapply of ml_module_expr * ml_module_expr
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 24b0dc6cd..b78e73e48 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -260,7 +260,7 @@ let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
let lib_dir = Lib.library_dp() in
List.iter (fun (_,id) ->
Declaremods.process_module_bindings [id]
- [make_mbid lib_dir id,
+ [MBId.make lib_dir id,
(Modintern.interp_modtype (Global.env()) mty, inl)]) idl;
(* Builds the stream *)
spc() ++
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 039d3ec43..2b0f458c1 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -155,11 +155,11 @@ let rec print_modtype env mp locals mty =
let env' = Option.map
(Modops.add_module (Modops.module_body_of_type mp1 mtb1)) env in
let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
- let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals
+ let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals
in
(try Declaremods.process_module_seb_binding mbid seb1 with _ -> ());
hov 2 (str "Funsig" ++ spc () ++ str "(" ++
- pr_id (id_of_mbid mbid) ++ str ":" ++
+ pr_id (MBId.to_id mbid) ++ str ":" ++
print_modtype env mp1 locals seb1 ++
str ")" ++ spc() ++ print_modtype env' mp locals' mtb2)
| SEBstruct (sign) ->
@@ -190,9 +190,9 @@ let rec print_modexpr env mp locals mexpr = match mexpr with
let env' = Option.map
(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
let typ = Option.default mty.typ_expr mty.typ_expr_alg in
- let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
+ let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in
(try Declaremods.process_module_seb_binding mbid typ with _ -> ());
- hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
+ hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(MBId.to_id mbid) ++
str ":" ++ print_modtype env mp' locals typ ++
str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
| SEBstruct struc ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 04:43:47 +0000