From 6946bbbf2390024b3ded7654814104e709cce755 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 18 Dec 2012 18:05:56 +0000 Subject: Modulification of mod_bound_id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/declarations.ml | 4 +- checker/declarations.mli | 6 +- checker/indtypes.ml | 4 +- checker/modops.mli | 2 +- dev/top_printers.ml | 2 +- kernel/declarations.ml | 2 +- kernel/declarations.mli | 2 +- kernel/entries.mli | 2 +- kernel/mod_subst.ml | 10 +- kernel/mod_subst.mli | 6 +- kernel/modops.mli | 4 +- kernel/names.ml | 216 +++++++++++++++++++++++------------------- kernel/names.mli | 66 ++++++++++--- kernel/safe_typing.ml | 4 +- kernel/safe_typing.mli | 2 +- library/declaremods.ml | 10 +- library/declaremods.mli | 4 +- library/global.mli | 2 +- library/globnames.ml | 4 +- library/lib.ml | 4 +- plugins/extraction/common.ml | 4 +- plugins/extraction/miniml.mli | 4 +- printing/ppvernac.ml | 2 +- printing/printmod.ml | 8 +- 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 -> -- cgit v1.2.3