diff options
61 files changed, 306 insertions, 255 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 548dd32fc..d354eb8c4 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -21,19 +21,19 @@ open Environ let rec debug_string_of_mp = function | MPfile sl -> Dir_path.to_string sl | MPbound uid -> "bound("^string_of_mbid uid^")" - | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l + | 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 - | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + | MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l let string_of_mp mp = if !Flags.debug then debug_string_of_mp mp else string_of_mp mp let prkn kn = let (mp,_,l) = repr_kn kn in - str(string_of_mp mp ^ "." ^ string_of_label l) + str(string_of_mp mp ^ "." ^ Label.to_string l) let prcon c = let ck = canonical_con c in let uk = user_con c in diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index b8e5fa043..fa1b26cc5 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -152,7 +152,7 @@ and check_with_def env mtb (idl,c) mp = | [] -> assert false | id::idl -> id,idl in - let l = label_of_id id in + let l = Label.of_id id in try let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in let before = List.rev rev_before in @@ -189,7 +189,7 @@ and check_with_mod env mtb (idl,mp1) mp = | [] -> assert false | id::idl -> id,idl in - let l = label_of_id id in + let l = Label.of_id id in try let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in let before = List.rev rev_before in diff --git a/checker/modops.ml b/checker/modops.ml index 4330eff30..f9c52c2e9 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -16,32 +16,32 @@ open Declarations (*i*) let error_not_a_constant l = - error ("\""^(string_of_label l)^"\" is not a constant") + error ("\""^(Label.to_string l)^"\" is not a constant") let error_not_a_functor _ = error "Application of not a functor" let error_incompatible_modtypes _ _ = error "Incompatible module types" let error_not_match l _ = - error ("Signature components for label "^string_of_label l^" do not match") + error ("Signature components for label "^Label.to_string l^" do not match") -let error_no_such_label l = error ("No such label "^string_of_label l) +let error_no_such_label l = error ("No such label "^Label.to_string l) let error_no_such_label_sub l l1 = let l1 = string_of_mp l1 in error ("The field "^ - string_of_label l^" is missing in "^l1^".") + Label.to_string l^" is missing in "^l1^".") let error_not_a_module_loc loc s = - user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module")) + user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module")) let error_not_a_module s = error_not_a_module_loc Loc.ghost s let error_with_incorrect l = - error ("Incorrect constraint for label \""^(string_of_label l)^"\"") + error ("Incorrect constraint for label \""^(Label.to_string l)^"\"") let error_a_generative_module_expected l = - error ("The module " ^ string_of_label l ^ " is not generative. Only " ^ + error ("The module " ^ Label.to_string l ^ " is not generative. Only " ^ "component of generative modules can be changed using the \"with\" " ^ "construct.") diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 951bed6c1..b23043a37 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -41,36 +41,36 @@ let add_mib_nameobjects mp l mib map = let map = Array.fold_right_i (fun i id map -> - Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) + Label.Map.add (Label.of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames map in - Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map + Label.Map.add (Label.of_id oib.mind_typename) (IndType (ip, mib)) map in Array.fold_right_i add_mip_nameobjects mib.mind_packets map (* creates (namedobject/namedmodule) map for the whole signature *) -type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t } +type labmap = { objs : namedobject Label.Map.t; mods : namedmodule Label.Map.t } -let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty } +let empty_labmap = { objs = Label.Map.empty; mods = Label.Map.empty } let get_obj mp map l = - try Labmap.find l map.objs + try Label.Map.find l map.objs with Not_found -> error_no_such_label_sub l mp let get_mod mp map l = - try Labmap.find l map.mods + try Label.Map.find l map.mods with Not_found -> error_no_such_label_sub l mp let make_labmap mp list = let add_one (l,e) map = match e with - | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs } + | SFBconst cb -> { map with objs = Label.Map.add l (Constant cb) map.objs } | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs } - | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods } - | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods } + | SFBmodule mb -> { map with mods = Label.Map.add l (Module mb) map.mods } + | SFBmodtype mtb -> { map with mods = Label.Map.add l (Modtype mtb) map.mods } in List.fold_right add_one list empty_labmap diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 7163f4429..d86f17033 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -456,29 +456,29 @@ let encode_path loc prefix mpdir suffix id = let raw_string_of_ref loc = function | ConstRef cst -> let (mp,dir,id) = repr_con cst in - encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id) + encode_path loc "CST" (Some (mp,dir)) [] (Label.to_id id) | IndRef (kn,i) -> let (mp,dir,id) = repr_mind kn in - encode_path loc "IND" (Some (mp,dir)) [id_of_label id] + encode_path loc "IND" (Some (mp,dir)) [Label.to_id id] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> let (mp,dir,id) = repr_mind kn in encode_path loc "CSTR" (Some (mp,dir)) - [id_of_label id;Id.of_string ("_"^string_of_int i)] + [Label.to_id id;Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) | VarRef id -> encode_path loc "SECVAR" None [] id let short_string_of_ref loc = function | VarRef id -> Ident (loc,id) - | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst))) - | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn))) + | ConstRef cst -> Ident (loc,Label.to_id (pi3 (repr_con cst))) + | IndRef (kn,0) -> Ident (loc,Label.to_id (pi3 (repr_mind kn))) | IndRef (kn,i) -> - encode_path loc "IND" None [id_of_label (pi3 (repr_mind kn))] + encode_path loc "IND" None [Label.to_id (pi3 (repr_mind kn))] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> encode_path loc "CSTR" None - [id_of_label (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)] + [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) (* Anticipate that printers can be used from ocamldebug and that diff --git a/kernel/declarations.ml b/kernel/declarations.ml index baeab9142..e2ebce28a 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -385,7 +385,7 @@ type structure_field_body = | SFBmodule of module_body | SFBmodtype of module_type_body -and structure_body = (label * structure_field_body) list +and structure_body = (Label.t * structure_field_body) list and struct_expr_body = | SEBident of module_path diff --git a/kernel/declarations.mli b/kernel/declarations.mli index fc142d253..3b43baa79 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -198,7 +198,7 @@ type structure_field_body = a [structure_body], once for a module ([SFBmodule] or [SFBmodtype]) and once for an object ([SFBconst] or [SFBmind]) *) -and structure_body = (label * structure_field_body) list +and structure_body = (Label.t * structure_field_body) list and struct_expr_body = | SEBident of module_path diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index b358d805a..0d29cf10b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -41,7 +41,7 @@ let is_modular = function let rec list_split_assoc ((k,m) as km) rev_before = function | [] -> raise Not_found - | (k',b)::after when eq_label k k' && (is_modular b) == (m : bool) -> rev_before,b,after + | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) -> rev_before,b,after | h::tail -> list_split_assoc km (h::rev_before) tail let discr_resolver env mtb = @@ -80,7 +80,7 @@ and check_with_def env sign (idl,c) mp equiv = | [] -> assert false | id::idl -> id,idl in - let l = label_of_id id in + let l = Label.of_id id in try let not_empty = match idl with [] -> false | _ :: _ -> true in let rev_before,spec,after = list_split_assoc (l, not_empty) [] sig_b in @@ -125,7 +125,7 @@ and check_with_def env sign (idl,c) mp equiv = (* Definition inside a sub-module *) let old = match spec with | SFBmodule msb -> msb - | _ -> error_not_a_module (string_of_label l) + | _ -> error_not_a_module (Label.to_string l) in begin match old.mod_expr with @@ -153,7 +153,7 @@ and check_with_mod env sign (idl,mp1) mp equiv = | [] -> assert false | id::idl -> id,idl in - let l = label_of_id id in + let l = Label.of_id id in try let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in let before = List.rev rev_before in @@ -162,7 +162,7 @@ and check_with_mod env sign (idl,mp1) mp equiv = (* Toplevel module definition *) let old = match spec with SFBmodule msb -> msb - | _ -> error_not_a_module (string_of_label l) + | _ -> error_not_a_module (Label.to_string l) in let mb_mp1 = (lookup_module mp1 env) in let mtb_mp1 = @@ -175,7 +175,7 @@ and check_with_mod env sign (idl,mp1) mp equiv = (check_subtypes env' mtb_mp1 (module_type_of_module None old)) old.mod_constraints - with Failure _ -> error_incorrect_with_constraint (label_of_id id) + with Failure _ -> error_incorrect_with_constraint (Label.of_id id) end | Some (SEBident(mp')) -> check_modpath_equiv env' mp1 mp'; @@ -197,7 +197,7 @@ and check_with_mod env sign (idl,mp1) mp equiv = (* Module definition of a sub-module *) let old = match spec with SFBmodule msb -> msb - | _ -> error_not_a_module (string_of_label l) + | _ -> error_not_a_module (Label.to_string l) in begin match old.mod_expr with @@ -215,7 +215,7 @@ and check_with_mod env sign (idl,mp1) mp equiv = SEBstruct(before@(l,new_spec)::subst_signature id_subst after), new_equiv,cst | Some (SEBident(mp')) -> - let mpnew = rebuild_mp mp' (List.map label_of_id idl) in + let mpnew = rebuild_mp mp' (List.map Label.of_id idl) in check_modpath_equiv env' mpnew mp; SEBstruct(before@(l,spec)::after) ,equiv,empty_constraint diff --git a/kernel/modops.ml b/kernel/modops.ml index b81627f22..e7afec2a0 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -44,24 +44,24 @@ type signature_mismatch_error = | NoTypeConstraintExpected type module_typing_error = - | SignatureMismatch of label * structure_field_body * signature_mismatch_error - | LabelAlreadyDeclared of label + | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error + | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry | NotAFunctor of struct_expr_body | IncompatibleModuleTypes of module_type_body * module_type_body | NotEqualModulePaths of module_path * module_path - | NoSuchLabel of label - | IncompatibleLabels of label * label + | NoSuchLabel of Label.t + | IncompatibleLabels of Label.t * Label.t | SignatureExpected of struct_expr_body | NoModuleToEnd | NoModuleTypeToEnd | NotAModule of string | NotAModuleType of string - | NotAConstant of label - | IncorrectWithConstraint of label - | GenerativeModuleExpected of label - | NonEmptyLocalContect of label option - | LabelMissing of label * string + | NotAConstant of Label.t + | IncorrectWithConstraint of Label.t + | GenerativeModuleExpected of Label.t + | NonEmptyLocalContect of Label.t option + | LabelMissing of Label.t * string exception ModuleTypingError of module_typing_error diff --git a/kernel/modops.mli b/kernel/modops.mli index 0d87ce88b..13129cdbd 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -71,28 +71,28 @@ type signature_mismatch_error = | NoTypeConstraintExpected type module_typing_error = - | SignatureMismatch of label * structure_field_body * signature_mismatch_error - | LabelAlreadyDeclared of label + | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error + | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry | NotAFunctor of struct_expr_body | IncompatibleModuleTypes of module_type_body * module_type_body | NotEqualModulePaths of module_path * module_path - | NoSuchLabel of label - | IncompatibleLabels of label * label + | NoSuchLabel of Label.t + | IncompatibleLabels of Label.t * Label.t | SignatureExpected of struct_expr_body | NoModuleToEnd | NoModuleTypeToEnd | NotAModule of string | NotAModuleType of string - | NotAConstant of label - | IncorrectWithConstraint of label - | GenerativeModuleExpected of label - | NonEmptyLocalContect of label option - | LabelMissing of label * string + | NotAConstant of Label.t + | IncorrectWithConstraint of Label.t + | GenerativeModuleExpected of Label.t + | NonEmptyLocalContect of Label.t option + | LabelMissing of Label.t * string exception ModuleTypingError of module_typing_error -val error_existing_label : label -> 'a +val error_existing_label : Label.t -> 'a val error_application_to_not_path : module_struct_entry -> 'a @@ -100,11 +100,11 @@ val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a val error_signature_mismatch : - label -> structure_field_body -> signature_mismatch_error -> 'a + Label.t -> structure_field_body -> signature_mismatch_error -> 'a -val error_incompatible_labels : label -> label -> 'a +val error_incompatible_labels : Label.t -> Label.t -> 'a -val error_no_such_label : label -> 'a +val error_no_such_label : Label.t -> 'a val error_signature_expected : struct_expr_body -> 'a @@ -114,12 +114,12 @@ val error_no_modtype_to_end : unit -> 'a val error_not_a_module : string -> 'a -val error_not_a_constant : label -> 'a +val error_not_a_constant : Label.t -> 'a -val error_incorrect_with_constraint : label -> 'a +val error_incorrect_with_constraint : Label.t -> 'a -val error_generative_module_expected : label -> 'a +val error_generative_module_expected : Label.t -> 'a -val error_non_empty_local_context : label option -> 'a +val error_non_empty_local_context : Label.t option -> 'a -val error_no_such_label_sub : label->string->'a +val error_no_such_label_sub : Label.t->string->'a diff --git a/kernel/names.ml b/kernel/names.ml index e10b34eb2..9b41fed1f 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -49,6 +49,8 @@ struct let to_string id = String.copy id + let print id = str id + module Self = struct type t = string @@ -217,24 +219,33 @@ let id_of_mbid (_,s,_) = s (** {6 Names of structure elements } *) +module Label = +struct + include Id + let make = Id.of_string + let of_id id = id + let to_id id = id +end + +(** Compatibility layer for [Label] *) + type label = Id.t -let mk_label = id_of_string -let string_of_label = string_of_id -let pr_label l = str (string_of_label l) -let id_of_label l = l -let label_of_id id = id -let eq_label = String.equal +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 -module Labset = Idset -module Labmap = Idmap +(** / 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 - | MPdot of module_path * label + | MPdot of module_path * Label.t let rec check_bound_mp = function | MPbound _ -> true @@ -244,7 +255,7 @@ let rec check_bound_mp = function let rec string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> string_of_uid uid - | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + | MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l (** we compare labels first if both are MPdots *) let rec mp_ord mp1 mp2 = @@ -277,7 +288,7 @@ let initial_path = MPfile Dir_path.initial (** {6 Kernel names } *) -type kernel_name = module_path * Dir_path.t * label +type kernel_name = module_path * Dir_path.t * Label.t let make_kn mp dir l = (mp,dir,l) let repr_kn kn = kn @@ -293,7 +304,7 @@ let string_of_kn (mp,dir,l) = | [] -> "." | _ -> "#" ^ string_of_dirpath dir ^ "#" in - string_of_mp mp ^ str_dir ^ string_of_label l + string_of_mp mp ^ str_dir ^ Label.to_string l let pr_kn kn = str (string_of_kn kn) diff --git a/kernel/names.mli b/kernel/names.mli index 150c04608..78d2d6216 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -33,6 +33,9 @@ sig val to_string : t -> string (** Converts a identifier into an string. *) + val print : t -> Pp.std_ppcmds + (** Pretty-printer. *) + module Set : Set.S with type elt = t (** Finite sets of identifiers. *) @@ -101,19 +104,33 @@ module ModIdmap : Map.S with type key = module_ident (** {6 Names of structure elements } *) -type label +module Label : +sig + type t + (** Type of labels *) -val mk_label : string -> label -val string_of_label : label -> string -val pr_label : label -> Pp.std_ppcmds + val equal : t -> t -> bool + (** Equality over labels *) -val label_of_id : Id.t -> label -val id_of_label : label -> Id.t + val make : string -> t + (** Create a label out of a string. *) -val eq_label : label -> label -> bool + val to_string : t -> string + (** Conversion to string. *) + + val of_id : Id.t -> t + (** Conversion from an identifier. *) -module Labset : Set.S with type elt = label -module Labmap : Map.S with type key = label + val to_id : t -> Id.t + (** Conversion to an identifier. *) + + val print : t -> Pp.std_ppcmds + (** Pretty-printer. *) + + module Set : Set.S with type elt = t + module Map : Map.S with type key = t + +end (** {6 Unique names for bound modules } *) @@ -136,7 +153,7 @@ val string_of_mbid : mod_bound_id -> string type module_path = | MPfile of Dir_path.t | MPbound of mod_bound_id - | MPdot of module_path * label + | MPdot of module_path * Label.t val mp_ord : module_path -> module_path -> int val mp_eq : module_path -> module_path -> bool @@ -156,11 +173,11 @@ val initial_path : module_path (** [= MPfile initial_dir] *) type kernel_name (** Constructor and destructor *) -val make_kn : module_path -> Dir_path.t -> label -> kernel_name -val repr_kn : kernel_name -> module_path * Dir_path.t * label +val make_kn : module_path -> Dir_path.t -> Label.t -> kernel_name +val repr_kn : kernel_name -> module_path * Dir_path.t * Label.t val modpath : kernel_name -> module_path -val label : kernel_name -> label +val label : kernel_name -> Label.t val string_of_kn : kernel_name -> string val pr_kn : kernel_name -> Pp.std_ppcmds @@ -200,17 +217,17 @@ 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.t -> label -> constant +val make_con : module_path -> Dir_path.t -> Label.t -> constant val make_con_equiv : module_path -> module_path -> Dir_path.t - -> label -> constant + -> Label.t -> constant val user_con : constant -> kernel_name val canonical_con : constant -> kernel_name -val repr_con : constant -> module_path * Dir_path.t * label +val repr_con : constant -> module_path * Dir_path.t * Label.t val eq_constant : constant -> constant -> bool -val con_with_label : constant -> label -> constant +val con_with_label : constant -> Label.t -> constant val string_of_con : constant -> string -val con_label : constant -> label +val con_label : constant -> Label.t val con_modpath : constant -> module_path val pr_con : constant -> Pp.std_ppcmds val debug_pr_con : constant -> Pp.std_ppcmds @@ -220,16 +237,16 @@ 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.t -> label -> mutual_inductive +val make_mind : module_path -> Dir_path.t -> Label.t -> mutual_inductive val make_mind_equiv : module_path -> module_path -> Dir_path.t - -> label -> mutual_inductive + -> Label.t -> 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.t * label +val repr_mind : mutual_inductive -> module_path * Dir_path.t * Label.t val eq_mind : mutual_inductive -> mutual_inductive -> bool val string_of_mind : mutual_inductive -> string -val mind_label : mutual_inductive -> label +val mind_label : mutual_inductive -> Label.t val mind_modpath : mutual_inductive -> module_path val pr_mind : mutual_inductive -> Pp.std_ppcmds val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds @@ -357,3 +374,26 @@ val string_of_dirpath : dir_path -> string val initial_dir : Dir_path.t (** @deprecated Same as [Dir_path.initial]. *) + +(** {5 Labels} *) + +type label = Label.t +(** Alias type *) + +val mk_label : string -> label +(** @deprecated Same as [Label.make]. *) + +val string_of_label : label -> string +(** @deprecated Same as [Label.to_string]. *) + +val pr_label : label -> Pp.std_ppcmds +(** @deprecated Same as [Label.print]. *) + +val label_of_id : Id.t -> label +(** @deprecated Same as [Label.of_id]. *) + +val id_of_label : label -> Id.t +(** @deprecated Same as [Label.to_id]. *) + +val eq_label : label -> label -> bool +(** @deprecated Same as [Label.equal]. *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c7bc76e57..823047974 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -80,7 +80,7 @@ type modvariant = type module_info = {modpath : module_path; - label : label; + label : Label.t; variant : modvariant; resolver : delta_resolver; resolver_of_param : delta_resolver;} @@ -96,8 +96,8 @@ type safe_environment = { old : safe_environment; env : env; modinfo : module_info; - modlabels : Labset.t; - objlabels : Labset.t; + modlabels : Label.Set.t; + objlabels : Label.Set.t; revstruct : structure_body; univ : Univ.constraints; engagement : engagement option; @@ -105,8 +105,8 @@ type safe_environment = loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list} -let exists_modlabel l senv = Labset.mem l senv.modlabels -let exists_objlabel l senv = Labset.mem l senv.objlabels +let exists_modlabel l senv = Label.Set.mem l senv.modlabels +let exists_objlabel l senv = Label.Set.mem l senv.objlabels let check_modlabel l senv = if exists_modlabel l senv then error_existing_label l @@ -114,12 +114,12 @@ let check_objlabel l senv = if exists_objlabel l senv then error_existing_label l let check_objlabels ls senv = - Labset.iter (fun l -> check_objlabel l senv) ls + Label.Set.iter (fun l -> check_objlabel l senv) ls let labels_of_mib mib = let add,get = - let labels = ref Labset.empty in - (fun id -> labels := Labset.add (label_of_id id) !labels), + let labels = ref Label.Set.empty in + (fun id -> labels := Label.Set.add (Label.of_id id) !labels), (fun () -> !labels) in let visit_mip mip = @@ -135,12 +135,12 @@ let rec empty_environment = env = empty_env; modinfo = { modpath = initial_path; - label = mk_label "_"; + label = Label.make "_"; variant = NONE; resolver = empty_delta_resolver; resolver_of_param = empty_delta_resolver}; - modlabels = Labset.empty; - objlabels = Labset.empty; + modlabels = Label.Set.empty; + objlabels = Label.Set.empty; revstruct = []; univ = Univ.empty_constraint; engagement = None; @@ -175,11 +175,11 @@ let add_field ((l,sfb) as field) gn senv = let mlabs,olabs = match sfb with | SFBmind mib -> let l = labels_of_mib mib in - check_objlabels l senv; (Labset.empty,l) + check_objlabels l senv; (Label.Set.empty,l) | SFBconst _ -> - check_objlabel l senv; (Labset.empty, Labset.singleton l) + check_objlabel l senv; (Label.Set.empty, Label.Set.singleton l) | SFBmodule _ | SFBmodtype _ -> - check_modlabel l senv; (Labset.singleton l, Labset.empty) + check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty) in let senv = add_constraints (constraints_of_sfb sfb) senv in let env' = match sfb, gn with @@ -191,8 +191,8 @@ let add_field ((l,sfb) as field) gn senv = in { senv with env = env'; - modlabels = Labset.union mlabs senv.modlabels; - objlabels = Labset.union olabs senv.objlabels; + modlabels = Label.Set.union mlabs senv.modlabels; + objlabels = Label.Set.union olabs senv.objlabels; revstruct = field :: senv.revstruct } (* Applying a certain function to the resolver of a safe environment *) @@ -291,7 +291,7 @@ let add_mind dir l mie senv = | _ -> () in let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in - if not (eq_label l (label_of_id id)) then + if not (Label.equal l (Label.of_id id)) then anomaly ("the label of inductive packet and its first inductive"^ " type do not match"); let kn = make_mind senv.modinfo.modpath dir l in @@ -339,8 +339,8 @@ let start_module l senv = mp, { old = senv; env = senv.env; modinfo = modinfo; - modlabels = Labset.empty; - objlabels = Labset.empty; + modlabels = Label.Set.empty; + objlabels = Label.Set.empty; revstruct = []; univ = Univ.empty_constraint; engagement = None; @@ -361,7 +361,7 @@ let end_module l restype senv = | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () | STRUCT params -> params, (List.length params > 0) in - if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label; + if not (Label.equal l modinfo.label) then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_non_empty_local_context None; let functorize_struct tb = List.fold_left @@ -424,7 +424,7 @@ let end_module l restype senv = mp,resolver,{ old = oldsenv.old; env = newenv; modinfo = modinfo; - modlabels = Labset.add l oldsenv.modlabels; + modlabels = Label.Set.add l oldsenv.modlabels; objlabels = oldsenv.objlabels; revstruct = (l,SFBmodule mb)::oldsenv.revstruct; univ = Univ.union_constraints senv'.univ oldsenv.univ; @@ -547,8 +547,8 @@ let start_modtype l senv = mp, { old = senv; env = senv.env; modinfo = modinfo; - modlabels = Labset.empty; - objlabels = Labset.empty; + modlabels = Label.Set.empty; + objlabels = Label.Set.empty; revstruct = []; univ = Univ.empty_constraint; engagement = None; @@ -565,7 +565,7 @@ let end_modtype l senv = | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end () | SIG params -> params in - if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label; + if not (Label.equal l modinfo.label) then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_non_empty_local_context None; let auto_tb = SEBstruct (List.rev senv.revstruct) @@ -599,7 +599,7 @@ let end_modtype l senv = mp, { old = oldsenv.old; env = newenv; modinfo = oldsenv.modinfo; - modlabels = Labset.add l oldsenv.modlabels; + modlabels = Label.Set.add l oldsenv.modlabels; objlabels = oldsenv.objlabels; revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct; univ = Univ.union_constraints senv.univ oldsenv.univ; @@ -646,7 +646,7 @@ let start_library dir senv = match (Dir_path.repr dir) with [] -> anomaly "Empty dirpath in Safe_typing.start_library" | hd::tl -> - Dir_path.make tl, label_of_id hd + Dir_path.make tl, Label.of_id hd in let mp = MPfile dir in let modinfo = {modpath = mp; @@ -658,8 +658,8 @@ let start_library dir senv = mp, { old = senv; env = senv.env; modinfo = modinfo; - modlabels = Labset.empty; - objlabels = Labset.empty; + modlabels = Label.Set.empty; + objlabels = Label.Set.empty; revstruct = []; univ = Univ.empty_constraint; engagement = None; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index bfcc3b8a9..0add7109a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,22 +43,22 @@ type global_declaration = | GlobalRecipe of Cooking.recipe val add_constant : - Dir_path.t -> label -> global_declaration -> safe_environment -> + Dir_path.t -> Label.t -> global_declaration -> safe_environment -> constant * safe_environment (** Adding an inductive type *) val add_mind : - Dir_path.t -> label -> mutual_inductive_entry -> safe_environment -> + Dir_path.t -> Label.t -> mutual_inductive_entry -> safe_environment -> mutual_inductive * safe_environment (** Adding a module *) val add_module : - label -> module_entry -> inline -> safe_environment + Label.t -> module_entry -> inline -> safe_environment -> module_path * delta_resolver * safe_environment (** Adding a module type *) val add_modtype : - label -> module_struct_entry -> inline -> safe_environment + Label.t -> module_struct_entry -> inline -> safe_environment -> module_path * safe_environment (** Adding universe constraints *) @@ -72,20 +72,20 @@ val set_engagement : engagement -> safe_environment -> safe_environment (** {6 Interactive module functions } *) val start_module : - label -> safe_environment -> module_path * safe_environment + Label.t -> safe_environment -> module_path * safe_environment val end_module : - label -> (module_struct_entry * inline) option + Label.t -> (module_struct_entry * inline) option -> 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 val start_modtype : - label -> safe_environment -> module_path * safe_environment + Label.t -> safe_environment -> module_path * safe_environment val end_modtype : - label -> safe_environment -> module_path * safe_environment + Label.t -> safe_environment -> module_path * safe_environment val add_include : module_struct_entry -> bool -> inline -> safe_environment -> @@ -138,7 +138,7 @@ val typing : safe_environment -> constr -> judgment (** {7 Query } *) -val exists_objlabel : label -> safe_environment -> bool +val exists_objlabel : Label.t -> safe_environment -> bool (*spiwack: safe retroknowledge functionalities *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index dbc5b01f1..c15681b04 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -45,36 +45,36 @@ let add_mib_nameobjects mp l mib map = let map = Array.fold_right_i (fun i id map -> - Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) + Label.Map.add (Label.of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames map in - Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map + Label.Map.add (Label.of_id oib.mind_typename) (IndType (ip, mib)) map in Array.fold_right_i add_mip_nameobjects mib.mind_packets map (* creates (namedobject/namedmodule) map for the whole signature *) -type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t } +type labmap = { objs : namedobject Label.Map.t; mods : namedmodule Label.Map.t } -let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty } +let empty_labmap = { objs = Label.Map.empty; mods = Label.Map.empty } let get_obj mp map l = - try Labmap.find l map.objs + try Label.Map.find l map.objs with Not_found -> error_no_such_label_sub l (string_of_mp mp) let get_mod mp map l = - try Labmap.find l map.mods + try Label.Map.find l map.mods with Not_found -> error_no_such_label_sub l (string_of_mp mp) let make_labmap mp list = let add_one (l,e) map = match e with - | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs } + | SFBconst cb -> { map with objs = Label.Map.add l (Constant cb) map.objs } | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs } - | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods } - | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods } + | SFBmodule mb -> { map with mods = Label.Map.add l (Module mb) map.mods } + | SFBmodtype mtb -> { map with mods = Label.Map.add l (Modtype mtb) map.mods } in List.fold_right add_one list empty_labmap diff --git a/library/assumptions.ml b/library/assumptions.ml index 1f6c8eeeb..84e870499 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -60,12 +60,12 @@ let modcache = ref (MPmap.empty : structure_body MPmap.t) let rec search_mod_label lab = function | [] -> raise Not_found - | (l, SFBmodule mb) :: _ when eq_label l lab -> mb + | (l, SFBmodule mb) :: _ when Label.equal l lab -> mb | _ :: fields -> search_mod_label lab fields let rec search_cst_label lab = function | [] -> raise Not_found - | (l, SFBconst cb) :: _ when eq_label l lab -> cb + | (l, SFBconst cb) :: _ when Label.equal l lab -> cb | _ :: fields -> search_cst_label lab fields let rec lookup_module_in_impl mp = diff --git a/library/declare.ml b/library/declare.ml index 015fc9894..20e5bdddc 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -117,7 +117,7 @@ let open_constant i ((sp,kn),_) = Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = - variable_exists id or Global.exists_objlabel (label_of_id id) + variable_exists id or Global.exists_objlabel (Label.of_id id) let check_exists sp = let id = basename sp in diff --git a/library/declaremods.ml b/library/declaremods.ml index 10b04c588..763aa5ffd 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -440,7 +440,7 @@ let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 = if not (String.equal (object_tag obj) "MODULE") then anomaly "MODULE expected!"; let substobjs = match idl with | [] -> - let mp' = MPdot(mp, label_of_id id) in + let mp' = MPdot(mp, Label.of_id id) in mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs | _ -> replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp diff --git a/library/global.ml b/library/global.ml index c2bd55128..f56cb7d61 100644 --- a/library/global.ml +++ b/library/global.ml @@ -46,7 +46,7 @@ let push_named_def d = let add_thing add dir id thing = - let kn, newenv = add dir (label_of_id id) thing !global_env in + let kn, newenv = add dir (Label.of_id id) thing !global_env in global_env := newenv; kn @@ -56,7 +56,7 @@ let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y let add_module id me inl = - let l = label_of_id id in + let l = Label.of_id id in let mp,resolve,new_env = add_module l me inl !global_env in global_env := new_env; mp,resolve @@ -72,13 +72,13 @@ let add_include me is_module inl = resolve let start_module id = - let l = label_of_id id in + let l = Label.of_id id in let mp,newenv = start_module l !global_env in global_env := newenv; mp let end_module fs id mtyo = - let l = label_of_id id in + let l = Label.of_id id in let mp,resolve,newenv = end_module l mtyo !global_env in Summary.unfreeze_summaries fs; global_env := newenv; @@ -92,13 +92,13 @@ let add_module_parameter mbid mte inl = let start_modtype id = - let l = label_of_id id in + let l = Label.of_id id in let mp,newenv = start_modtype l !global_env in global_env := newenv; mp let end_modtype fs id = - let l = label_of_id id in + let l = Label.of_id id in let kn,newenv = end_modtype l !global_env in Summary.unfreeze_summaries fs; global_env := newenv; diff --git a/library/global.mli b/library/global.mli index dac230a44..d49dd836b 100644 --- a/library/global.mli +++ b/library/global.mli @@ -87,7 +87,7 @@ val lookup_module : module_path -> module_body val lookup_modtype : module_path -> module_type_body val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive -val exists_objlabel : label -> bool +val exists_objlabel : Label.t -> bool (** Compiled modules *) val start_library : Dir_path.t -> module_path diff --git a/library/globnames.ml b/library/globnames.ml index efc46a7ac..c37e370a3 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -138,9 +138,9 @@ let constr_of_global_or_constr = function (** {6 Temporary function to brutally form kernel names from section paths } *) -let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (label_of_id id) +let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (Label.of_id id) -let encode_con dir id = make_con (MPfile dir) Dir_path.empty (label_of_id id) +let encode_con dir id = make_con (MPfile dir) Dir_path.empty (Label.of_id id) let decode_mind kn = let rec dir_of_mp = function @@ -149,18 +149,18 @@ let decode_mind kn = let _,_,dp = repr_mbid mbid in let id = id_of_mbid mbid in id::(Dir_path.repr dp) - | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp) + | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp) in let mp,sec_dir,l = repr_mind kn in if (Dir_path.repr sec_dir) = [] then - (Dir_path.make (dir_of_mp mp)),id_of_label l + (Dir_path.make (dir_of_mp mp)),Label.to_id l else anomaly "Section part should be empty!" let decode_con kn = let mp,sec_dir,l = repr_con kn in match mp,(Dir_path.repr sec_dir) with - MPfile dir,[] -> (dir,id_of_label l) + MPfile dir,[] -> (dir,Label.to_id l) | _ , [] -> anomaly "MPfile expected!" | _ -> anomaly "Section part should be empty!" diff --git a/library/lib.ml b/library/lib.ml index ed64b1f40..9ac9b7c71 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -61,7 +61,7 @@ let classify_segment seg = let rec clean ((substl,keepl,anticipl) as acc) = function | (_,CompilingLibrary _) :: _ | [] -> acc | ((sp,kn),Leaf o) :: stk -> - let id = Names.id_of_label (Names.label kn) in + let id = Names.Label.to_id (Names.label kn) in (match classify_object o with | Dispose -> clean acc stk | Keep o' -> @@ -136,11 +136,11 @@ let current_prefix () = snd !path_prefix 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) + Names.make_con mp dir (Names.Label.of_id id) let make_oname id = make_path id, make_kn id @@ -657,7 +657,7 @@ let rec split_mp mp = | Names.MPfile dp -> dp, Names.Dir_path.empty | Names.MPdot (prfx, lbl) -> let mprec, dprec = split_mp prfx in - mprec, Names.Dir_path.make (Names.Id.of_string (Names.string_of_label lbl) :: (Names.Dir_path.repr dprec)) + 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] let split_modpath mp = @@ -666,7 +666,7 @@ let split_modpath mp = | Names.MPbound mbid -> library_dp (), [Names.id_of_mbid mbid] | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in - (mp', Names.id_of_label l :: lab) + (mp', Names.Label.to_id l :: lab) in let (mp, l) = aux mp in mp, l diff --git a/library/libnames.ml b/library/libnames.ml index 8e026d8c2..7680e5248 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -151,7 +151,7 @@ type object_name = full_path * kernel_name type object_prefix = Dir_path.t * (module_path * Dir_path.t) let make_oname (dirpath,(mp,dir)) id = - make_path dirpath id, make_kn mp dir (label_of_id id) + make_path dirpath id, make_kn mp dir (Label.of_id id) (* to this type are mapped Dir_path.t's in the nametab *) type global_dir_reference = diff --git a/library/nameops.ml b/library/nameops.ml index 361a53d6b..a8803e7a5 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -136,7 +136,7 @@ let name_fold_map f e = function | Name id -> let (e,id) = f e id in (e,Name id) | Anonymous -> e,Anonymous -let pr_lab l = str (string_of_label l) +let pr_lab l = str (Label.to_string l) let default_library = Names.Dir_path.initial (* = ["Top"] *) diff --git a/library/nameops.mli b/library/nameops.mli index 6e9bde839..0f71d28a1 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -36,7 +36,7 @@ val name_app : (Id.t -> Id.t) -> name -> name val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> name -> 'a * name -val pr_lab : label -> Pp.std_ppcmds +val pr_lab : Label.t -> Pp.std_ppcmds (** some preset paths *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index bd5e2291a..d8e489be7 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -255,7 +255,7 @@ let params_ren_add, params_ren_mem = type visible_layer = { mp : module_path; params : module_path list; - content : ((kind*string),label) Hashtbl.t } + content : ((kind*string),Label.t) Hashtbl.t } let pop_visible, push_visible, get_visible = let vis = ref [] in @@ -321,7 +321,7 @@ let modfstlev_rename = let add_prefixes,get_prefixes,_ = mktable true in fun l -> let coqid = Id.of_string "Coq" in - let id = id_of_label l in + let id = Label.to_id l in try let coqset = get_prefixes id in let nextcoq = next_ident_away coqid coqset in @@ -341,7 +341,7 @@ let rec mp_renaming_fun mp = match mp with | MPdot (mp,l) -> let lmp = mp_renaming mp in if lmp = [""] then (modfstlev_rename l)::lmp - else (modular_rename Mod (id_of_label l))::lmp + else (modular_rename Mod (Label.to_id l))::lmp | MPbound mbid -> let s = modular_rename Mod (id_of_mbid mbid) in if not (params_ren_mem mp) then [s] @@ -584,7 +584,7 @@ let pp_module mp = the constants are directly turned into chars *) let mk_ind path s = - make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (mk_label s) + make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (Label.make s) let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 9ddd0f2af..0fd3e7bb7 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -63,7 +63,7 @@ val top_visible_mp : unit -> module_path val push_visible : module_path -> module_path list -> unit val pop_visible : unit -> unit -val check_duplicate : module_path -> label -> string +val check_duplicate : module_path -> Label.t -> string type reset_kind = AllButExternal | Everything diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 754016715..7f5ad4f66 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -208,7 +208,7 @@ let env_for_mtb_with_def env mp seb idl = | SEBstruct(sig_b) -> sig_b | _ -> assert false in - let l = label_of_id (List.hd idl) in + let l = Label.of_id (List.hd idl) in let spot = function (l',SFBconst _) -> l = l' | _ -> false in let before = fst (List.split_when spot sig_b) in Modops.add_signature mp before empty_delta_resolver env diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index b892ae57a..5ab3647d6 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -450,7 +450,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) | Anonymous::l, typ::typs -> None :: (select_fields l typs) | Name id::l, typ::typs -> - let knp = make_con mp d (label_of_id id) in + let knp = make_con mp d (Label.of_id id) in (* Is it safe to use [id] for projections [foo.id] ? *) if List.for_all ((=) Keep) (type2signature env typ) then projs := Cset.add knp !projs; diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 14a30ae79..104a4c865 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -157,7 +157,7 @@ and ml_with_declaration = | ML_With_type of Id.t list * Id.t list * ml_type | ML_With_module of Id.t list * module_path -and ml_module_sig = (label * ml_specif) list +and ml_module_sig = (Label.t * ml_specif) list type ml_structure_elem = | SEdecl of ml_decl @@ -170,7 +170,7 @@ and ml_module_expr = | MEstruct of module_path * ml_module_structure | MEapply of ml_module_expr * ml_module_expr -and ml_module_structure = (label * ml_structure_elem) list +and ml_module_structure = (Label.t * ml_structure_elem) list and ml_module = { ml_mod_expr : ml_module_expr; diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index bcdee5954..dba77b923 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1306,7 +1306,7 @@ let inline_test r t = let con_of_string s = let null = Dir_path.empty in match Dir_path.repr (dirpath_of_string s) with - | id :: d -> make_con (MPfile (Dir_path.make d)) null (label_of_id id) + | id :: d -> make_con (MPfile (Dir_path.make d)) null (Label.of_id id) | [] -> assert false let manual_inline_set = diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9746c39e4..0ed6a2855 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -32,14 +32,14 @@ let se_iter do_decl do_spec do_mp = let mp_mt = msid_of_mt mt in let l',idl' = List.sep_last idl in let mp_w = - List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' + List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l')) in + let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l')) in mt_iter mt; do_decl (Dtype(r,l,t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in let mp_w = - List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl + List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl in mt_iter mt; do_mp mp_w; do_mp mp | MTsig (_, sign) -> List.iter spec_iter sign @@ -249,7 +249,7 @@ let dfix_to_mlfix rv av i = (try MLrel (n + (Refmap'.find refe s)) with Not_found -> t) | _ -> ast_map_lift subst n t in - let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in + let ids = Array.map (fun r -> Label.to_id (label_of_r r)) rv in let c = Array.map (subst 0) av in MLfix(i, ids, c) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 7742dd783..fbd3fd4ea 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -648,9 +648,9 @@ and pp_module_type params = function let mp_mt = msid_of_mt mt in let l,idl' = List.sep_last idl in let mp_w = - List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' + List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l)) in + let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l)) in push_visible mp_mt []; let pp_w = str " with type " ++ ids ++ pp_global Type r in pop_visible(); @@ -658,7 +658,7 @@ and pp_module_type params = function | MTwith(mt,ML_With_module(idl,mp)) -> let mp_mt = msid_of_mt mt in let mp_w = - List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl + List.fold_left (fun mp id -> MPdot(mp,Label.of_id id)) mp_mt idl in push_visible mp_mt []; let pp_w = str " with module " ++ pp_modname mp_w in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a54121139..74728f412 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -175,7 +175,7 @@ let add_recursors env kn = make_con_equiv (modpath (user_mind kn)) (modpath (canonical_mind kn)) - Dir_path.empty (label_of_id id) + Dir_path.empty (Label.of_id id) in let mib = Environ.lookup_mind kn env in Array.iter @@ -245,8 +245,8 @@ let safe_basename_of_global r = anomaly "Inductive object unknown to extraction and not globally visible" in match r with - | ConstRef kn -> id_of_label (con_label kn) - | IndRef (kn,0) -> id_of_label (mind_label kn) + | ConstRef kn -> Label.to_id (con_label kn) + | IndRef (kn,0) -> Label.to_id (mind_label kn) | IndRef (kn,i) -> (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename with Not_found -> last_chance r) @@ -268,7 +268,7 @@ let safe_pr_long_global r = with _ -> match r with | ConstRef kn -> let mp,_,l = repr_con kn in - str ((string_of_mp mp)^"."^(string_of_label l)) + str ((string_of_mp mp)^"."^(Label.to_string l)) | _ -> assert false let pr_long_mp mp = diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2cf3c475e..b69715fc9 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -46,9 +46,9 @@ val info_file : string -> unit (*s utilities about [module_path] and [kernel_names] and [global_reference] *) val occur_kn_in_ref : mutual_inductive -> global_reference -> bool -val repr_of_r : global_reference -> module_path * Dir_path.t * label +val repr_of_r : global_reference -> module_path * Dir_path.t * Label.t val modpath_of_r : global_reference -> module_path -val label_of_r : global_reference -> label +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 @@ -61,8 +61,8 @@ val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t val common_prefix_from_list : module_path -> module_path list -> module_path option -val get_nth_label_mp : int -> module_path -> label -val labels_of_ref : global_reference -> module_path * label list +val get_nth_label_mp : int -> module_path -> Label.t +val labels_of_ref : global_reference -> module_path * Label.t list (*s Some table-related operations *) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 455f3539b..4c3c48915 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -83,7 +83,7 @@ let string_of_R_constant kn = | MPfile dir, sec_dir, id when sec_dir = Dir_path.empty && Dir_path.to_string dir = "Coq.Reals.Rdefinitions" - -> string_of_label id + -> Label.to_string id | _ -> "constant_not_of_R" let rec string_of_R_constr c = diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ca73799c1..9c895e6a9 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -966,7 +966,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in - let f_id = id_of_label (con_label (destConst f)) in + let f_id = Label.to_id (con_label (destConst f)) in let prove_replacement = tclTHENSEQ [ @@ -1000,7 +1000,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let finfos = find_Function_infos (destConst f) in mkConst (Option.get finfos.equation_lemma) with (Not_found | Option.IsNone as e) -> - let f_id = id_of_label (con_label (destConst f)) in + let f_id = Label.to_id (con_label (destConst f)) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious i*) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1d30ce9a6..9678fb547 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,14 +322,14 @@ let generate_functional_principle match new_princ_name with | Some (id) -> id,id | None -> - let id_of_f = id_of_label (con_label f) in + let id_of_f = Label.to_id (con_label f) in id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in let names = ref [new_princ_name] in let hook new_principle_type _ _ = if sorts = None then - (* let id_of_f = id_of_label (con_label f) in *) + (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = let s = Termops.new_sort_in_family fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in @@ -390,7 +390,7 @@ let get_funs_constant mp dp = (fun i na -> match na with | Name id -> - let const = make_con mp dp (label_of_id id) in + let const = make_con mp dp (Label.of_id id) in const,i | Anonymous -> anomaly "Anonymous fix" diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dfce8bf4..6c3b009f8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -58,7 +58,7 @@ let functional_induction with_clean c princl pat = (or f_rec, f_rect) i*) let princ_name = Indrec.make_elimination_ident - (id_of_label (con_label c')) + (Label.to_id (con_label c')) (Tacticals.elimination_sort_of_goal g) in try @@ -810,14 +810,14 @@ let make_graph (f_ref:global_reference) = in l | _ -> - let id = id_of_label (con_label c) in + let id = Label.to_id (con_label c) in [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in do_generate_principle error_error false false expr_list; (* We register the infos *) let mp,dp,_ = repr_con c in List.iter - (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (label_of_id id))) + (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) expr_list); Dumpglob.continue () diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5942e11b4..dfbfdce3a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -408,7 +408,7 @@ let update_Function finfo = let add_Function is_general f = - let f_id = id_of_label (con_label f) in + let f_id = Label.to_id (con_label f) in let equation_lemma = find_or_none (mk_equation_id f_id) and correctness_lemma = find_or_none (mk_correct_id f_id) and completeness_lemma = find_or_none (mk_complete_id f_id) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 4a466175f..eed421159 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -179,7 +179,7 @@ let find_induction_principle f = (* let fname = *) (* match kind_of_term f with *) (* | Const c' -> *) -(* id_of_label (con_label c') *) +(* Label.to_id (con_label c') *) (* | _ -> error "Must be used with a function" *) (* in *) @@ -1049,7 +1049,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g in Array.iteri (fun i f_as_constant -> - let f_id = id_of_label (con_label f_as_constant) in + let f_id = Label.to_id (con_label f_as_constant) in (*i The next call to mk_correct_id is valid since we are constructing the lemma Ensures by: obvious i*) @@ -1100,7 +1100,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g in Array.iteri (fun i f_as_constant -> - let f_id = id_of_label (con_label f_as_constant) in + let f_id = Label.to_id (con_label f_as_constant) in (*i The next call to mk_complete_id is valid since we are constructing the lemma Ensures by: obvious i*) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 68c5e16ae..7b77afd07 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -73,7 +73,7 @@ let def_of_const t = | _ -> assert false) with _ -> anomaly ("Cannot find definition of constant "^ - (Id.to_string (id_of_label (con_label sp)))) + (Id.to_string (Label.to_id (con_label sp)))) ) |_ -> assert false diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index d02d26007..c89e06f7c 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -246,11 +246,11 @@ let my_constant c = let new_ring_path = Dir_path.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) let ltac s = - lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (mk_label s)) + lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (Label.make s)) let znew_ring_path = Dir_path.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = - lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (mk_label s)) + lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (Label.make s)) let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; @@ -829,7 +829,7 @@ let new_field_path = Dir_path.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) let field_ltac s = - lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (mk_label s)) + lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (Label.make s)) let _ = add_map "field" diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index d6b9f73d5..643dacbab 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -17,10 +17,10 @@ open Glob_term let make_dir l = Names.Dir_path.make (List.map Names.Id.of_string (List.rev l)) let make_path dir id = Libnames.make_path (make_dir dir) (Names.Id.of_string id) -let make_mind mp id = Names.make_mind mp Names.Dir_path.empty (Names.mk_label id) +let make_mind mp id = Names.make_mind mp Names.Dir_path.empty (Names.Label.make id) let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id let make_mind_mpdot dir modname id = - let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label modname) + let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.Label.make modname) in make_mind mp id diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index fb951b35f..4a8436d76 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -128,12 +128,12 @@ let token_list_of_kernel_name tag = let module GN = Globnames in let id,dir = match tag with | Variable kn -> - N.id_of_label (N.label kn), Lib.cwd () + N.Label.to_id (N.label kn), Lib.cwd () | Constant con -> - N.id_of_label (N.con_label con), + N.Label.to_id (N.con_label con), Lib.remove_section_part (GN.ConstRef con) | Inductive kn -> - N.id_of_label (N.mind_label kn), + N.Label.to_id (N.mind_label kn), Lib.remove_section_part (GN.IndRef (kn,0)) in token_list_of_path dir id (etag_of_tag tag) diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index b4ec85ab7..864f35e80 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -21,7 +21,7 @@ let cprop = (N.MPfile (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) (N.Dir_path.make []) - (N.mk_label "CProp") + (N.Label.make "CProp") ;; let whd_betadeltaiotacprop env _evar_map ty = diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 50309317e..e16f9dd19 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -384,12 +384,12 @@ let print internal glob_ref kind xml_library_root = (* 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) + N.make_kn mod_path dir_path (N.Label.of_id id) in let (_,body,typ) = G.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ | Gn.ConstRef kn -> - let id = N.id_of_label (N.con_label kn) in + let id = N.Label.to_id (N.con_label kn) in let cb = G.lookup_constant kn in let val0 = D.body_of_constant cb in let typ = cb.D.const_type in @@ -467,7 +467,7 @@ let _ = (* I saved in the Pfedit.set_xml_cook_proof callback. *) let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in show_pftreestate internal fn pftreestate - (Names.id_of_label (Names.con_label kn)) ; + (Names.Label.to_id (Names.con_label kn)) ; proof_to_export := None) ;; diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e42013b33..b01a463a1 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -559,7 +559,7 @@ let lookup_eliminator ind_sp s = (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) try - let cst =Global.constant_of_delta_kn (make_kn mp dp (label_of_id id)) in + let cst =Global.constant_of_delta_kn (make_kn mp dp (Label.of_id id)) in let _ = Global.lookup_constant cst in mkConst cst with Not_found -> diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index a7b49fbe2..cbfd78deb 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -77,7 +77,7 @@ let hdchar env c = | LetIn (_,_,_,c) -> hdrec (k+1) c | Cast (c,_,_) -> hdrec k c | App (f,l) -> hdrec k f - | Const kn -> lowercase_first_char (id_of_label (con_label kn)) + | Const kn -> lowercase_first_char (Label.to_id (con_label kn)) | Ind x -> lowercase_first_char (basename_of_global (IndRef x)) | Construct x -> lowercase_first_char (basename_of_global (ConstructRef x)) | Var id -> lowercase_first_char id diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1a4bd3877..78b01a42a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -227,7 +227,7 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - Some (EvalConst (con_with_label kn (label_of_id id))) in + Some (EvalConst (con_with_label kn (Label.of_id id))) in match refi with | None -> None | Some ref -> @@ -502,7 +502,7 @@ let reduce_mind_case_use_function func env sigma mia = mutual inductive, try to reuse the global name if the block was indeed initially built as a global definition *) - let kn = con_with_label (destConst func) (label_of_id id) + let kn = con_with_label (destConst func) (Label.of_id id) in try match constant_opt_value env kn with | None -> None diff --git a/printing/printer.ml b/printing/printer.ml index a3e2fd9c2..9b8c16938 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -587,7 +587,7 @@ let pr_assumptionset env s = try pr_constant env kn with Not_found -> let mp,_,lab = repr_con kn in - str (string_of_mp mp ^ "." ^ string_of_label lab) + str (string_of_mp mp ^ "." ^ Label.to_string lab) in let safe_pr_ltype typ = try str " : " ++ pr_ltype typ with _ -> mt () diff --git a/printing/printmod.ml b/printing/printmod.ml index 7ee5b92de..039d3ec43 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -90,7 +90,7 @@ let nametab_register_body mp fp (l,body) = | SFBmodule _ -> () (* TODO *) | SFBmodtype _ -> () (* TODO *) | SFBconst _ -> - push (id_of_label l) (ConstRef (make_con mp Dir_path.empty l)) + push (Label.to_id l) (ConstRef (make_con mp Dir_path.empty l)) | SFBmind mib -> let mind = make_mind mp Dir_path.empty l in Array.iteri @@ -101,7 +101,7 @@ let nametab_register_body mp fp (l,body) = mib.mind_packets let print_body is_impl env mp (l,body) = - let name = str (string_of_label l) in + let name = str (Label.to_string l) in hov 2 (match body with | SFBmodule _ -> str "Module " ++ name | SFBmodtype _ -> str "Module Type " ++ name diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index f1297647c..caebb76d4 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -538,7 +538,7 @@ TACTIC EXTEND autounfold_one TACTIC EXTEND autounfoldify | [ "autounfoldify" constr(x) ] -> [ let db = match kind_of_term x with - | Const c -> string_of_label (con_label c) + | Const c -> Label.to_string (con_label c) | _ -> assert false in autounfold ["core";db] onConcl ] END diff --git a/tactics/equality.ml b/tactics/equality.ml index 16ee05f9e..7ca1116ba 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -253,14 +253,14 @@ let find_elim hdcncl lft2rgt dep cls args gl = | Some false, Some _ -> let c1 = destConst pr1 in let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in - let l' = label_of_id (add_suffix (id_of_label l) "_r") in + let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in begin try let _ = Global.lookup_constant c1' in mkConst c1' with Not_found -> - let rwr_thm = string_of_label l' in + let rwr_thm = Label.to_string l' in error ("Cannot find rewrite principle "^rwr_thm^".") end | _ -> pr1 diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 0f2ac6cfe..93b39583b 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -127,7 +127,7 @@ let _ = let lookup_atomic id = Id.Map.find id !atomic_mactab let is_atomic_kn kn = let (_,_,l) = repr_kn kn in - Id.Map.mem (id_of_label l) !atomic_mactab + Id.Map.mem (Label.to_id l) !atomic_mactab (* Tactics table (TacExtend). *) @@ -875,7 +875,7 @@ let load_md i ((sp,kn),(local,defs)) = match id with | NewTac id -> let sp = Libnames.make_path dp id in - let kn = Names.make_kn mp dir (label_of_id id) in + let kn = Names.make_kn mp dir (Label.of_id id) in Nametab.push_tactic (Until i) sp kn; add (kn,t) | UpdateTac kn -> replace (kn,t)) defs @@ -887,7 +887,7 @@ let open_md i ((sp,kn),(local,defs)) = match id with NewTac id -> let sp = Libnames.make_path dp id in - let kn = Names.make_kn mp dir (label_of_id id) in + let kn = Names.make_kn mp dir (Label.of_id id) in Nametab.push_tactic (Exactly i) sp kn | UpdateTac kn -> ()) defs diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index eaca147e1..5ef789561 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -328,9 +328,9 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q = Parameter*) ( let mp,dir,lbl = repr_con (destConst v) in - mkConst (make_con mp dir (mk_label ( - if Int.equal offset 1 then ("eq_"^(string_of_label lbl)) - else ((string_of_label lbl)^"_lb") + mkConst (make_con mp dir (Label.make ( + if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) + else ((Label.to_string lbl)^"_lb") ))) ) in @@ -375,9 +375,9 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = Parameter*) ( let mp,dir,lbl = repr_con (destConst v) in - mkConst (make_con mp dir (mk_label ( - if Int.equal offset 1 then ("eq_"^(string_of_label lbl)) - else ((string_of_label lbl)^"_bl") + mkConst (make_con mp dir (Label.make ( + if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) + else ((Label.to_string lbl)^"_bl") ))) ) in diff --git a/toplevel/class.ml b/toplevel/class.ml index 01205e597..6f0ac1793 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -164,8 +164,8 @@ let get_strength stre ref cls clt = let ident_key_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" - | CL_CONST sp -> string_of_label (con_label sp) - | CL_IND (sp,_) -> string_of_label (mind_label sp) + | CL_CONST sp -> Label.to_string (con_label sp) + | CL_IND (sp,_) -> Label.to_string (mind_label sp) | CL_SECVAR id -> Id.to_string id (* coercion identité *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index fbabaa432..a5805b637 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -85,7 +85,7 @@ let refine_ref = ref (fun _ -> assert(false)) let id_of_class cl = match cl.cl_impl with - | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l + | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l | IndRef (kn,i) -> let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in mip.(0).Declarations.mind_typename diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ef510aee5..8289f6ca2 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -572,11 +572,11 @@ let explain_not_match_error = function strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained" let explain_signature_mismatch l spec why = - str "Signature components for label " ++ str (string_of_label l) ++ + str "Signature components for label " ++ str (Label.to_string l) ++ str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." let explain_label_already_declared l = - str ("The label "^string_of_label l^" is already declared.") + str ("The label "^Label.to_string l^" is already declared.") let explain_application_to_not_path _ = str "Application of modules is restricted to paths." @@ -591,11 +591,11 @@ let explain_not_equal_module_paths mp1 mp2 = str "Non equal modules." let explain_no_such_label l = - str "No such label " ++ str (string_of_label l) ++ str "." + str "No such label " ++ str (Label.to_string l) ++ str "." let explain_incompatible_labels l l' = str "Opening and closing labels are not the same: " ++ - str (string_of_label l) ++ str " <> " ++ str (string_of_label l') ++ str "!" + str (Label.to_string l) ++ str " <> " ++ str (Label.to_string l') ++ str "!" let explain_signature_expected mtb = str "Signature expected." @@ -613,24 +613,24 @@ let explain_not_a_module_type s = quote (str s) ++ str " is not a module type." let explain_not_a_constant l = - quote (pr_label l) ++ str " is not a constant." + quote (Label.print l) ++ str " is not a constant." let explain_incorrect_label_constraint l = str "Incorrect constraint for label " ++ - quote (pr_label l) ++ str "." + quote (Label.print l) ++ str "." let explain_generative_module_expected l = - str "The module " ++ str (string_of_label l) ++ + str "The module " ++ str (Label.to_string l) ++ strbrk " is not generative. Only components of generative modules can be changed using the \"with\" construct." let explain_non_empty_local_context = function | None -> str "The local context is not empty." | Some l -> str "The local context of the component " ++ - str (string_of_label l) ++ str " is not empty." + str (Label.to_string l) ++ str " is not empty." let explain_label_missing l s = - str "The field " ++ str (string_of_label l) ++ str " is missing in " + str "The field " ++ str (Label.to_string l) ++ str " is missing in " ++ str s ++ str "." let explain_module_error = function diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f37d99dd1..2a9af66ff 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -268,7 +268,7 @@ let print_namespace ns = | MPbound _ -> None (* Not a proper namespace. *) | MPfile dir -> match_dirpath ns (Names.Dir_path.repr dir) | MPdot (mp,lbl) -> - let id = Names.id_of_label lbl in + let id = Names.Label.to_id lbl in begin match match_modulepath ns mp with | Some [] as y -> y | Some (a::ns') -> @@ -287,7 +287,7 @@ let print_namespace ns = let rec list_of_modulepath = function | MPbound _ -> assert false (* MPbound never matches *) | MPfile dir -> Names.Dir_path.repr dir - | MPdot (mp,lbl) -> (Names.id_of_label lbl)::(list_of_modulepath mp) + | MPdot (mp,lbl) -> (Names.Label.to_id lbl)::(list_of_modulepath mp) in snd (Util.List.chop n (List.rev (list_of_modulepath mp))) in @@ -295,7 +295,7 @@ let print_namespace ns = let print_kn kn = (* spiwack: I'm ignoring the dirpath, is that bad? *) let (mp,_,lbl) = Names.repr_kn kn in - let qn = (qualified_minus (List.length ns) mp)@[Names.id_of_label lbl] in + let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in print_list pr_id qn in let print_constant k body = diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 4999cd0c2..935606fc4 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -83,7 +83,7 @@ let error_whelp_unknown_reference ref = let uri_of_repr_kn ref (mp,dir,l) = match mp with | MPfile sl -> - uri_of_dirpath (id_of_label l :: Dir_path.repr dir @ Dir_path.repr sl) + uri_of_dirpath (Label.to_id l :: Dir_path.repr dir @ Dir_path.repr sl) | _ -> error_whelp_unknown_reference ref |