diff options
Diffstat (limited to 'kernel')
50 files changed, 390 insertions, 387 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 7e193ef829..e8cce0841d 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -85,7 +85,7 @@ module type RedFlagsSig = sig val fFIX : red_kind val fCOFIX : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind + val fCONST : Constant.t -> red_kind val fVAR : Id.t -> red_kind val no_red : reds val red_add : reds -> red_kind -> reds @@ -114,7 +114,7 @@ module RedFlags = (struct type red_kind = BETA | DELTA | ETA | MATCH | FIX | COFIX | ZETA - | CONST of constant | VAR of Id.t + | CONST of Constant.t | VAR of Id.t let fBETA = BETA let fDELTA = DELTA let fETA = ETA @@ -234,7 +234,7 @@ let unfold_red kn = * instantiations (cbv or lazy) are. *) -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey let eq_pconstant_key (c,u) (c',u') = eq_constant_key c c' && Univ.Instance.equal u u' @@ -401,7 +401,7 @@ let update v1 no t = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * constant + | Zproj of int * int * Constant.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 9e5cb48a49..de1bb120ee 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -29,7 +29,7 @@ val all_opaque : transparent_state val all_transparent : transparent_state val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> constant -> bool +val is_transparent_constant : transparent_state -> Constant.t -> bool (** Sets of reduction kinds. *) module type RedFlagsSig = sig @@ -46,7 +46,7 @@ module type RedFlagsSig = sig val fFIX : red_kind val fCOFIX : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind + val fCONST : Constant.t -> red_kind val fVAR : Id.t -> red_kind (** No reduction at all *) @@ -92,7 +92,7 @@ val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds (***********************************************************************) -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey type 'a infos_cache type 'a infos = { @@ -145,7 +145,7 @@ type fterm = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * constant + | Zproj of int * int * Constant.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 25f61c7aa9..63b0e69295 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -74,7 +74,7 @@ type instruction = | Kclosurerec of int * int * Label.t array * Label.t array | Kclosurecofix of int * int * Label.t array * Label.t array (* nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of Constant.t | Kconst of structured_constant | Kmakeblock of int * tag | Kmakeprod @@ -193,7 +193,7 @@ let pp_sort s = let rec pp_struct_const = function | Const_sorts s -> pp_sort s - | Const_ind (mind, i) -> pr_mind mind ++ str"#" ++ int i + | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i | Const_proj p -> Constant.print p | Const_b0 i -> int i | Const_bn (i,t) -> @@ -241,7 +241,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal idu -> str "getglobal " ++ pr_con idu + | Kgetglobal idu -> str "getglobal " ++ Constant.print idu | Kconst sc -> str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 718917ab35..e9070b26a7 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -69,7 +69,7 @@ type instruction = (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of Constant.t | Kconst of structured_constant | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0 ** is accu, all others are popped from diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index d63fcffa2c..5bac26bf9e 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -998,7 +998,7 @@ let compile_constant_body fail_on_error env univs = function match kind_of_term body with | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) - let con= constant_of_kn (canonical_con kn') in + let con= Constant.make1 (Constant.canonical kn') in Some (BCalias (get_alias env con)) | _ -> let res = compile fail_on_error ~universes:instance_size env body in @@ -1006,7 +1006,7 @@ let compile_constant_body fail_on_error env univs = function (* Shortcut of the previous function used during module strengthening *) -let compile_alias kn = BCalias (constant_of_kn (canonical_con kn)) +let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn)) (* spiwack: additional function which allow different part of compilation of the 31-bit integers *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 48c2e45332..9209e84606 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -14,7 +14,7 @@ val compile_constant_body : bool -> (** Shortcut of the previous function used during module strengthening *) -val compile_alias : Names.constant -> body_code +val compile_alias : Names.Constant.t -> body_code (** spiwack: this function contains the information needed to perform the static compilation of int31 (trying and obtaining diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 092bcecc38..eeea19c12b 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -19,7 +19,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of Names.constant + | Reloc_getglobal of Names.Constant.t type patch = reloc_info * int @@ -348,12 +348,12 @@ let subst_to_patch s (code,pl,fv) = type body_code = | BCdefined of to_patch - | BCalias of Names.constant + | BCalias of Names.Constant.t | BCconstant type to_patch_substituted = | PBCdefined of to_patch substituted -| PBCalias of Names.constant substituted +| PBCalias of Names.Constant.t substituted | PBCconstant let from_val = function diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index c80edd5965..fee45aafd8 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -4,7 +4,7 @@ open Cbytecodes type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant + | Reloc_getglobal of Constant.t type patch = reloc_info * int @@ -23,7 +23,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = | BCdefined of to_patch - | BCalias of constant + | BCalias of Constant.t | BCconstant diff --git a/kernel/constr.ml b/kernel/constr.ml index c3e6095363..cec00c04b3 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -75,7 +75,7 @@ type ('constr, 'types) pfixpoint = type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration type 'a puniverses = 'a Univ.puniverses -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of (constant * 'univs) + | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array @@ -520,7 +520,7 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = eq c1 c2 && Array.equal_norefl eq l1 l2 | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2 - | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2 + | Const (c1,u1), Const (c2,u2) -> Constant.equal c1 c2 && eq_universes true u1 u2 | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> @@ -681,7 +681,7 @@ let constr_ord_int f t1 t2 = | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 - | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2 + | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2 | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> diff --git a/kernel/constr.mli b/kernel/constr.mli index 76dbf55309..da074d85ca 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -15,7 +15,7 @@ open Names type 'a puniverses = 'a Univ.puniverses (** {6 Simply type aliases } *) -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -113,8 +113,8 @@ val mkApp : constr * constr array -> constr val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses -(** Constructs a constant *) -val mkConst : constant -> constr +(** Constructs a Constant.t *) +val mkConst : Constant.t -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) @@ -208,7 +208,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = - [F] itself is not {!App} - and [[|P1;..;Pn|]] is not empty. *) - | Const of (constant * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + | Const of (Constant.t * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *) | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) @@ -302,7 +302,7 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to compare universe - instances (the first boolean tells if they belong to a constant), [s] to + instances (the first boolean tells if they belong to a Constant.t), [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) @@ -335,7 +335,7 @@ val compare_head_gen_with : (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for conversion, [fle] for cumulativity, [u] to compare universe - instances (the first boolean tells if they belong to a constant), + instances (the first boolean tells if they belong to a Constant.t), [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 248cd2b30e..02c179ab69 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -16,7 +16,7 @@ val empty : oracle If [oracle_order kn1 kn2] is true, then unfold kn1 first. Note: the oracle does not introduce incompleteness, it only tries to postpone unfolding of "opaque" constants. *) -val oracle_order : ('a -> constant) -> oracle -> bool -> +val oracle_order : ('a -> Constant.t) -> oracle -> bool -> 'a tableKey -> 'a tableKey -> bool (** Priority for the expansion of constant in the conversion test. @@ -30,14 +30,14 @@ val transparent : level (** Check whether a level is transparent *) val is_transparent : level -> bool -val get_strategy : oracle -> constant tableKey -> level +val get_strategy : oracle -> Constant.t tableKey -> level (** Sets the level of a constant. * Level of RelKey constant cannot be set. *) -val set_strategy : oracle -> constant tableKey -> level -> oracle +val set_strategy : oracle -> Constant.t tableKey -> level -> oracle (** Fold over the non-transparent levels of the oracle. Order unspecified. *) -val fold_strategy : (constant tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a +val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a val get_transp_state : oracle -> transparent_state diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 80d41847cd..08fff0ca41 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -29,15 +29,15 @@ let pop_dirpath p = match DirPath.repr p with | _::l -> DirPath.make l let pop_mind kn = - let (mp,dir,l) = Names.repr_mind kn in - Names.make_mind mp (pop_dirpath dir) l + let (mp,dir,l) = MutInd.repr3 kn in + MutInd.make3 mp (pop_dirpath dir) l let pop_con con = - let (mp,dir,l) = Names.repr_con con in - Names.make_con mp (pop_dirpath dir) l + let (mp,dir,l) = Constant.repr3 con in + Constant.make3 mp (pop_dirpath dir) l type my_global_reference = - | ConstRef of constant + | ConstRef of Constant.t | IndRef of inductive | ConstructRef of constructor diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 633cf0abdd..30d0e55880 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -14,5 +14,5 @@ open Pre_env val val_of_constr : env -> constr -> values -val set_opaque_const : constant -> unit -val set_transparent_const : constant -> unit +val set_opaque_const : Constant.t -> unit +val set_transparent_const : Constant.t -> unit diff --git a/kernel/declarations.ml b/kernel/declarations.ml index e17fb1c38f..8b949f9289 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -48,7 +48,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : mutual_inductive; + proj_ind : MutInd.t; proj_npars : int; proj_arg : int; proj_type : types; (* Type under params *) @@ -115,7 +115,7 @@ v} - The constants associated to each projection. - The checked projection bodies. *) -type record_body = (Id.t * constant array * projection_body array) option +type record_body = (Id.t * Constant.t array * projection_body array) option type regular_inductive_arity = { mind_user_arity : types; @@ -212,12 +212,12 @@ type ('ty,'a) functorize = only for short module printing and for extraction. *) type with_declaration = - | WithMod of Id.t list * module_path + | WithMod of Id.t list * ModPath.t | WithDef of Id.t list * constr Univ.in_universe_context type module_alg_expr = - | MEident of module_path - | MEapply of module_alg_expr * module_path + | MEident of ModPath.t + | MEapply of module_alg_expr * ModPath.t | MEwith of module_alg_expr * with_declaration (** A component of a module structure *) @@ -251,7 +251,7 @@ and module_implementation = | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) and 'a generic_module_body = - { mod_mp : module_path; (** absolute path of the module *) + { mod_mp : ModPath.t; (** absolute path of the module *) mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) mod_type_alg : module_expression option; (** algebraic type *) @@ -290,5 +290,5 @@ and _ module_retroknowledge = - A module application is atomic, for instance ((M N) P) : * the head of [MEapply] can only be another [MEapply] or a [MEident] - * the argument of [MEapply] is now directly forced to be a [module_path]. + * the argument of [MEapply] is now directly forced to be a [ModPath.t]. *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 66d66c7d09..d7329a319e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -287,9 +287,9 @@ let hcons_mind mib = (** {6 Stm machinery } *) let string_of_side_effect { Entries.eff } = match eff with - | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")" | Entries.SEscheme (cl,_) -> - "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")" (** Hashconsing of modules *) diff --git a/kernel/entries.ml b/kernel/entries.ml index a1ccbdbc1b..f294c4ce4a 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -85,7 +85,7 @@ type parameter_entry = Context.Named.t option * bool * types Univ.in_universe_context * inline type projection_entry = { - proj_entry_ind : mutual_inductive; + proj_entry_ind : MutInd.t; proj_entry_arg : int } type 'a constant_entry = @@ -115,8 +115,8 @@ type seff_env = | `Opaque of Constr.t * Univ.universe_context_set ] type side_eff = - | SEsubproof of constant * Declarations.constant_body * seff_env - | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string + | SEsubproof of Constant.t * Declarations.constant_body * seff_env + | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string type side_effect = { from_env : Declarations.structure_body CEphemeron.key; diff --git a/kernel/environ.mli b/kernel/environ.mli index 2667ad7ca9..37816f1e5e 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -126,19 +126,19 @@ val pop_rel_context : int -> env -> env (** {5 Global constants } {6 Add entries to global environment } *) -val add_constant : constant -> constant_body -> env -> env -val add_constant_key : constant -> constant_body -> Pre_env.link_info -> +val add_constant : Constant.t -> constant_body -> env -> env +val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info -> env -> env (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) -val lookup_constant : constant -> env -> constant_body -val evaluable_constant : constant -> env -> bool +val lookup_constant : Constant.t -> env -> constant_body +val evaluable_constant : Constant.t -> env -> bool (** New-style polymorphism *) -val polymorphic_constant : constant -> env -> bool +val polymorphic_constant : Constant.t -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool -val type_in_type_constant : constant -> env -> bool +val type_in_type_constant : Constant.t -> env -> bool (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if @@ -149,35 +149,35 @@ val type_in_type_constant : constant -> env -> bool type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant puniverses -> constr constrained -val constant_type : env -> constant puniverses -> types constrained +val constant_value : env -> Constant.t puniverses -> constr constrained +val constant_type : env -> Constant.t puniverses -> types constrained -val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option -val constant_value_and_type : env -> constant puniverses -> +val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.constraints) option +val constant_value_and_type : env -> Constant.t puniverses -> constr option * types * Univ.constraints (** The universe context associated to the constant, empty if not polymorphic *) -val constant_context : env -> constant -> Univ.abstract_universe_context +val constant_context : env -> Constant.t -> Univ.abstract_universe_context (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) -val constant_value_in : env -> constant puniverses -> constr -val constant_type_in : env -> constant puniverses -> types -val constant_opt_value_in : env -> constant puniverses -> constr option +val constant_value_in : env -> Constant.t puniverses -> constr +val constant_type_in : env -> Constant.t puniverses -> types +val constant_opt_value_in : env -> Constant.t puniverses -> constr option (** {6 Primitive projections} *) val lookup_projection : Names.projection -> env -> projection_body -val is_projection : constant -> env -> bool +val is_projection : Constant.t -> env -> bool (** {5 Inductive types } *) -val add_mind_key : mutual_inductive -> Pre_env.mind_key -> env -> env -val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env +val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env +val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names raises [Not_found] if the required path is not found *) -val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +val lookup_mind : MutInd.t -> env -> mutual_inductive_body (** New-style polymorphism *) val polymorphic_ind : inductive -> env -> bool @@ -195,8 +195,8 @@ val add_modtype : module_type_body -> env -> env (** [shallow_add_module] does not add module components *) val shallow_add_module : module_body -> env -> env -val lookup_module : module_path -> env -> module_body -val lookup_modtype : module_path -> env -> module_type_body +val lookup_module : ModPath.t -> env -> module_body +val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e248436ec4..c0f564dc3c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -787,7 +787,7 @@ exception UndefinableExpansion a substitution of the form [params, x : ind params] *) let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params mind_consnrealdecls mind_consnrealargs paramslet ctx = - let mp, dp, l = repr_mind kn in + let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not matching with a parameter context. *) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index e4b7c086af..f5d0ed3f29 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -34,7 +34,7 @@ exception InductiveError of inductive_error (** The following function does checks on inductive declarations. *) -val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body +val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body (** The following enforces a system compatible with the univalent model *) @@ -44,4 +44,4 @@ val is_indices_matter : unit -> bool val compute_projections : pinductive -> Id.t -> Id.t -> int -> Context.Rel.t -> int array -> int array -> Context.Rel.t -> Context.Rel.t -> - (constant array * projection_body array) + (Constant.t array * projection_body array) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 0dfa8db00e..1caede8573 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -32,7 +32,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) -val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list +val ind_subst : MutInd.t -> mutual_inductive_body -> universe_instance -> constr list val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t @@ -65,7 +65,7 @@ val arities_of_constructors : pinductive -> mind_specif -> types array val type_of_constructors : pinductive -> mind_specif -> types array (** Transforms inductive specification into types (in nf) *) -val arities_of_specif : mutual_inductive puniverses -> mind_specif -> types array +val arities_of_specif : MutInd.t puniverses -> mind_specif -> types array val inductive_params : mind_specif -> int diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 7b660939b5..1793e4f715 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -23,13 +23,13 @@ open Term type delta_hint = | Inline of int * constr option - | Equiv of kernel_name + | Equiv of KerName.t -(* NB: earlier constructor Prefix_equiv of module_path +(* NB: earlier constructor Prefix_equiv of ModPath.t is now stored in a separate table, see Deltamap.t below *) module Deltamap = struct - type t = module_path MPmap.t * delta_hint KNmap.t + type t = ModPath.t MPmap.t * delta_hint KNmap.t let empty = MPmap.empty, KNmap.empty let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km @@ -45,7 +45,7 @@ module Deltamap = struct end (* Invariant: in the [delta_hint] map, an [Equiv] should only - relate [kernel_name] with the same label (and section dirpath). *) + relate [KerName.t] with the same label (and section dirpath). *) type delta_resolver = Deltamap.t @@ -65,7 +65,7 @@ module Umap = struct let join map1 map2 = fold add_mp add_mbi map1 map2 end -type substitution = (module_path * delta_resolver) Umap.t +type substitution = (ModPath.t * delta_resolver) Umap.t let empty_subst = Umap.empty @@ -76,21 +76,21 @@ let is_empty_subst = Umap.is_empty let string_of_hint = function | Inline (_,Some _) -> "inline(Some _)" | Inline _ -> "inline()" - | Equiv kn -> string_of_kn kn + | Equiv kn -> KerName.to_string kn let debug_string_of_delta resolve = let kn_to_string kn hint l = - (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l + (KerName.to_string kn ^ "=>" ^ string_of_hint hint) :: l in let mp_to_string mp mp' l = - (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l + (ModPath.to_string mp ^ "=>" ^ ModPath.to_string mp') :: l in let l = Deltamap.fold mp_to_string kn_to_string resolve [] in String.concat ", " (List.rev l) 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 one_pair (mp,reso) = (ModPath.to_string mp,debug_string_of_delta reso) in + let mp_one_pair mp0 p l = (ModPath.to_string mp0, 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 [] @@ -117,7 +117,7 @@ let debug_pr_subst sub = let add_inline_delta_resolver kn (lev,oc) = Deltamap.add_kn kn (Inline (lev,oc)) let add_kn_delta_resolver kn kn' = - assert (Label.equal (label kn) (label kn')); + assert (Label.equal (KerName.label kn) (KerName.label kn')); Deltamap.add_kn kn (Equiv kn') let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2 @@ -165,12 +165,12 @@ let solve_delta_kn resolve kn = | Inline (lev, Some c) -> raise (Change_equiv_to_inline (lev,c)) | Inline (_, None) -> raise Not_found with Not_found -> - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in let new_mp = find_prefix resolve mp in if mp == new_mp then kn else - make_kn new_mp dir l + KerName.make new_mp dir l let kn_of_delta resolve kn = try solve_delta_kn resolve kn @@ -242,18 +242,18 @@ let subst_mp sub mp = | Some (mp',_) -> mp' let subst_kn_delta sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',resolve) -> - solve_delta_kn resolve (make_kn mp' dir l) + solve_delta_kn resolve (KerName.make mp' dir l) | None -> kn let subst_kn sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',_) -> - (make_kn mp' dir l) + (KerName.make mp' dir l) | None -> kn exception No_subst @@ -419,7 +419,7 @@ let subst_mps sub c = let rec replace_mp_in_mp mpfrom mpto mp = match mp with - | _ when mp_eq mp mpfrom -> mpto + | _ when ModPath.equal mp mpfrom -> mpto | MPdot (mp1,l) -> let mp1' = replace_mp_in_mp mpfrom mpto mp1 in if mp1 == mp1' then mp @@ -427,14 +427,14 @@ let rec replace_mp_in_mp mpfrom mpto mp = | _ -> mp let replace_mp_in_kn mpfrom mpto kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in let mp'' = replace_mp_in_mp mpfrom mpto mp in if mp==mp'' then kn - else make_kn mp'' dir l + else KerName.make mp'' dir l let rec mp_in_mp mp mp1 = match mp1 with - | _ when mp_eq mp1 mp -> true + | _ when ModPath.equal mp1 mp -> true | MPdot (mp2,l) -> mp_in_mp mp mp2 | _ -> false @@ -446,7 +446,7 @@ let subset_prefixed_by mp resolver = match hint with | Inline _ -> rslv | Equiv _ -> - if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv + if mp_in_mp mp (KerName.modpath kn) then Deltamap.add_kn kn hint rslv else rslv in Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver @@ -515,7 +515,7 @@ let add_delta_resolver resolver1 resolver2 = let substition_prefixed_by k mp subst = let mp_prefixmp kmp (mp_to,reso) sub = - if mp_in_mp mp kmp && not (mp_eq mp kmp) then + if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then let new_key = replace_mp_in_mp mp k kmp in Umap.add_mp new_key (mp_to,reso) sub else sub diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index f1d0e42796..1d7012ce5c 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -20,44 +20,44 @@ type delta_resolver val empty_delta_resolver : delta_resolver val add_mp_delta_resolver : - module_path -> module_path -> delta_resolver -> delta_resolver + ModPath.t -> ModPath.t -> delta_resolver -> delta_resolver val add_kn_delta_resolver : - kernel_name -> kernel_name -> delta_resolver -> delta_resolver + KerName.t -> KerName.t -> delta_resolver -> delta_resolver val add_inline_delta_resolver : - kernel_name -> (int * constr option) -> delta_resolver -> delta_resolver + KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver (** Effect of a [delta_resolver] on a module path, on a kernel name *) -val mp_of_delta : delta_resolver -> module_path -> module_path -val kn_of_delta : delta_resolver -> kernel_name -> kernel_name +val mp_of_delta : delta_resolver -> ModPath.t -> ModPath.t +val kn_of_delta : delta_resolver -> KerName.t -> KerName.t (** Build a constant whose canonical part is obtained via a resolver *) -val constant_of_delta_kn : delta_resolver -> kernel_name -> constant +val constant_of_delta_kn : delta_resolver -> KerName.t -> Constant.t (** Same, but a 2nd resolver is tried if the 1st one had no effect *) val constant_of_deltas_kn : - delta_resolver -> delta_resolver -> kernel_name -> constant + delta_resolver -> delta_resolver -> KerName.t -> Constant.t (** Same for inductive names *) -val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive +val mind_of_delta_kn : delta_resolver -> KerName.t -> MutInd.t val mind_of_deltas_kn : - delta_resolver -> delta_resolver -> kernel_name -> mutual_inductive + delta_resolver -> delta_resolver -> KerName.t -> MutInd.t (** Extract the set of inlined constant in the resolver *) -val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list +val inline_of_delta : int option -> delta_resolver -> (int * KerName.t) list (** Does a [delta_resolver] contains a [mp], a constant, an inductive ? *) -val mp_in_delta : module_path -> delta_resolver -> bool -val con_in_delta : constant -> delta_resolver -> bool -val mind_in_delta : mutual_inductive -> delta_resolver -> bool +val mp_in_delta : ModPath.t -> delta_resolver -> bool +val con_in_delta : Constant.t -> delta_resolver -> bool +val mind_in_delta : MutInd.t -> delta_resolver -> bool (** {6 Substitution} *) @@ -72,15 +72,15 @@ val is_empty_subst : substitution -> bool composition. Most often this is not what you want. For sequential composition, try [join (map_mbid mp delta) subs] **) val add_mbid : - MBId.t -> module_path -> delta_resolver -> substitution -> substitution + MBId.t -> ModPath.t -> delta_resolver -> substitution -> substitution val add_mp : - module_path -> module_path -> delta_resolver -> substitution -> substitution + ModPath.t -> ModPath.t -> delta_resolver -> substitution -> substitution (** map_* create a new substitution [arg2/arg1]\{arg3\} *) val map_mbid : - MBId.t -> module_path -> delta_resolver -> substitution + MBId.t -> ModPath.t -> delta_resolver -> substitution val map_mp : - module_path -> module_path -> delta_resolver -> substitution + ModPath.t -> ModPath.t -> delta_resolver -> substitution (** sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] @@ -117,10 +117,10 @@ val debug_pr_delta : delta_resolver -> Pp.t as well [==] *) val subst_mp : - substitution -> module_path -> module_path + substitution -> ModPath.t -> ModPath.t val subst_mind : - substitution -> mutual_inductive -> mutual_inductive + substitution -> MutInd.t -> MutInd.t val subst_ind : substitution -> inductive -> inductive @@ -128,10 +128,10 @@ val subst_ind : val subst_pind : substitution -> pinductive -> pinductive val subst_kn : - substitution -> kernel_name -> kernel_name + substitution -> KerName.t -> KerName.t val subst_con : - substitution -> pconstant -> constant * constr + substitution -> pconstant -> Constant.t * constr val subst_pcon : substitution -> pconstant -> pconstant @@ -140,10 +140,10 @@ val subst_pcon_term : substitution -> pconstant -> pconstant * constr val subst_con_kn : - substitution -> constant -> constant * constr + substitution -> Constant.t -> Constant.t * constr -val subst_constant : - substitution -> constant -> constant +val subst_constant : + substitution -> Constant.t -> Constant.t (** Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? @@ -154,7 +154,7 @@ val subst_evaluable_reference : substitution -> evaluable_global_reference -> evaluable_global_reference (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) -val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name +val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t (** [subst_mps sub c] performs the substitution [sub] on all kernel names appearing in [c] *) diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index dcabb13346..1225c3e1e3 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -21,16 +21,16 @@ open Names *) val translate_module : - env -> module_path -> inline -> module_entry -> module_body + env -> ModPath.t -> inline -> module_entry -> module_body (** [translate_modtype] produces a [module_type_body] whose [mod_type_alg] cannot be [None] (and of course [mod_expr] is [Abstract]). *) val translate_modtype : - env -> module_path -> inline -> module_type_entry -> module_type_body + env -> ModPath.t -> inline -> module_type_entry -> module_type_body (** Low-level function for translating a module struct entry : - - We translate to a module when a [module_path] is given, + - We translate to a module when a [ModPath.t] is given, otherwise to a module type. - The first output is the expanded signature - The second output is the algebraic expression, kept mostly for @@ -40,14 +40,14 @@ type 'alg translation = module_signature * 'alg * delta_resolver * Univ.ContextSet.t val translate_mse : - env -> module_path option -> inline -> module_struct_entry -> + env -> ModPath.t option -> inline -> module_struct_entry -> module_alg_expr translation (** From an already-translated (or interactive) implementation and an (optional) signature entry, produces a final [module_body] *) val finalize_module : - env -> module_path -> (module_expression option) translation -> + env -> ModPath.t -> (module_expression option) translation -> (module_type_entry * inline) option -> module_body @@ -55,5 +55,5 @@ val finalize_module : module type given to an Include *) val translate_mse_incl : - bool -> env -> module_path -> inline -> module_struct_entry -> + bool -> env -> ModPath.t -> inline -> module_struct_entry -> unit translation diff --git a/kernel/modops.ml b/kernel/modops.ml index 76915e917a..c10af0725b 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -59,7 +59,7 @@ type module_typing_error = | NotAFunctor | IsAFunctor | IncompatibleModuleTypes of module_type_body * module_type_body - | NotEqualModulePaths of module_path * module_path + | NotEqualModulePaths of ModPath.t * ModPath.t | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | NotAModule of string @@ -68,7 +68,7 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | IncludeRestrictedFunctor of module_path + | IncludeRestrictedFunctor of ModPath.t exception ModuleTypingError of module_typing_error @@ -403,8 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta = let constr = Mod_subst.force_constr body in add_inline_delta_resolver kn (lev, Some constr) l with Not_found -> - error_no_such_label_sub (con_label con) - (string_of_mp (con_modpath con)) + error_no_such_label_sub (Constant.label con) + (ModPath.to_string (Constant.modpath con)) in make_inline delta constants diff --git a/kernel/modops.mli b/kernel/modops.mli index e2a94b6919..e1bba21d3c 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -26,9 +26,9 @@ val destr_nofunctor : ('ty,'a) functorize -> 'a (** Conversions between [module_body] and [module_type_body] *) val module_type_of_module : module_body -> module_type_body -val module_body_of_type : module_path -> module_type_body -> module_body +val module_body_of_type : ModPath.t -> module_type_body -> module_body -val check_modpath_equiv : env -> module_path -> module_path -> unit +val check_modpath_equiv : env -> ModPath.t -> ModPath.t -> unit val implem_smartmap : (module_signature -> module_signature) -> @@ -43,7 +43,7 @@ val subst_structure : substitution -> structure_body -> structure_body (** {6 Adding to an environment } *) val add_structure : - module_path -> structure_body -> delta_resolver -> env -> env + ModPath.t -> structure_body -> delta_resolver -> env -> env (** adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env @@ -53,19 +53,19 @@ the native compiler. The linking information is updated. *) val add_linked_module : module_body -> Pre_env.link_info -> env -> env (** same, for a module type *) -val add_module_type : module_path -> module_type_body -> env -> env +val add_module_type : ModPath.t -> module_type_body -> env -> env (** {6 Strengthening } *) -val strengthen : module_type_body -> module_path -> module_type_body +val strengthen : module_type_body -> ModPath.t -> module_type_body val inline_delta_resolver : - env -> inline -> module_path -> MBId.t -> module_type_body -> + env -> inline -> ModPath.t -> MBId.t -> module_type_body -> delta_resolver -> delta_resolver -val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body +val strengthen_and_subst_mb : module_body -> ModPath.t -> bool -> module_body -val subst_modtype_and_resolver : module_type_body -> module_path -> +val subst_modtype_and_resolver : module_type_body -> ModPath.t -> module_type_body (** {6 Cleaning a module expression from bounded parts } @@ -118,7 +118,7 @@ type module_typing_error = | NotAFunctor | IsAFunctor | IncompatibleModuleTypes of module_type_body * module_type_body - | NotEqualModulePaths of module_path * module_path + | NotEqualModulePaths of ModPath.t * ModPath.t | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | NotAModule of string @@ -127,7 +127,7 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | IncludeRestrictedFunctor of module_path + | IncludeRestrictedFunctor of ModPath.t exception ModuleTypingError of module_typing_error @@ -153,4 +153,4 @@ val error_generative_module_expected : Label.t -> 'a val error_no_such_label_sub : Label.t->string->'a -val error_include_restricted_functor : module_path -> 'a +val error_include_restricted_functor : ModPath.t -> 'a diff --git a/kernel/names.mli b/kernel/names.mli index d97fd2b3aa..531a0cccb2 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -113,6 +113,8 @@ end (** {6 Type aliases} *) type name = Name.t = Anonymous | Name of Id.t +[@@ocaml.deprecated "Use Name.t"] + type variable = Id.t type module_ident = Id.t @@ -572,54 +574,55 @@ module Idmap : module type of Id.Map (** {5 Directory paths} *) type dir_path = DirPath.t -(** @deprecated Alias for [DirPath.t]. *) +[@@ocaml.deprecated "Alias for [DirPath.t]."] -val dir_path_ord : dir_path -> dir_path -> int -(** @deprecated Same as [DirPath.compare]. *) +val dir_path_ord : DirPath.t -> DirPath.t -> int +[@@ocaml.deprecated "Same as [DirPath.compare]."] -val dir_path_eq : dir_path -> dir_path -> bool -(** @deprecated Same as [DirPath.equal]. *) +val dir_path_eq : DirPath.t -> DirPath.t -> bool +[@@ocaml.deprecated "Same as [DirPath.equal]."] -val make_dirpath : module_ident list -> dir_path -(** @deprecated Same as [DirPath.make]. *) +val make_dirpath : module_ident list -> DirPath.t +[@@ocaml.deprecated "Same as [DirPath.make]."] -val repr_dirpath : dir_path -> module_ident list -(** @deprecated Same as [DirPath.repr]. *) +val repr_dirpath : DirPath.t -> module_ident list +[@@ocaml.deprecated "Same as [DirPath.repr]."] -val empty_dirpath : dir_path -(** @deprecated Same as [DirPath.empty]. *) +val empty_dirpath : DirPath.t +[@@ocaml.deprecated "Same as [DirPath.empty]."] -val is_empty_dirpath : dir_path -> bool -(** @deprecated Same as [DirPath.is_empty]. *) +val is_empty_dirpath : DirPath.t -> bool +[@@ocaml.deprecated "Same as [DirPath.is_empty]."] -val string_of_dirpath : dir_path -> string -(** @deprecated Same as [DirPath.to_string]. *) +val string_of_dirpath : DirPath.t -> string +[@@ocaml.deprecated "Same as [DirPath.to_string]."] val initial_dir : DirPath.t -(** @deprecated Same as [DirPath.initial]. *) +[@@ocaml.deprecated "Same as [DirPath.initial]."] (** {5 Labels} *) type label = Label.t +[@@ocaml.deprecated "Same as [Label.t]."] (** Alias type *) -val mk_label : string -> label -(** @deprecated Same as [Label.make]. *) +val mk_label : string -> Label.t +[@@ocaml.deprecated "Same as [Label.make]."] -val string_of_label : label -> string -(** @deprecated Same as [Label.to_string]. *) +val string_of_label : Label.t -> string +[@@ocaml.deprecated "Same as [Label.to_string]."] -val pr_label : label -> Pp.t -(** @deprecated Same as [Label.print]. *) +val pr_label : Label.t -> Pp.t +[@@ocaml.deprecated "Same as [Label.print]."] -val label_of_id : Id.t -> label -(** @deprecated Same as [Label.of_id]. *) +val label_of_id : Id.t -> Label.t +[@@ocaml.deprecated "Same as [Label.of_id]."] -val id_of_label : label -> Id.t -(** @deprecated Same as [Label.to_id]. *) +val id_of_label : Label.t -> Id.t +[@@ocaml.deprecated "Same as [Label.to_id]."] -val eq_label : label -> label -> bool -(** @deprecated Same as [Label.equal]. *) +val eq_label : Label.t -> Label.t -> bool +[@@ocaml.deprecated "Same as [Label.equal]."] (** {5 Unique bound module names} *) @@ -627,89 +630,89 @@ 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]. *) +[@@ocaml.deprecated "Same as [MBId.compare]."] val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool -(** @deprecated Same as [MBId.equal]. *) +[@@ocaml.deprecated "Same as [MBId.equal]."] val make_mbid : DirPath.t -> Id.t -> mod_bound_id -(** @deprecated Same as [MBId.make]. *) +[@@ocaml.deprecated "Same as [MBId.make]."] val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t -(** @deprecated Same as [MBId.repr]. *) +[@@ocaml.deprecated "Same as [MBId.repr]."] val id_of_mbid : mod_bound_id -> Id.t -(** @deprecated Same as [MBId.to_id]. *) +[@@ocaml.deprecated "Same as [MBId.to_id]."] val string_of_mbid : mod_bound_id -> string -(** @deprecated Same as [MBId.to_string]. *) +[@@ocaml.deprecated "Same as [MBId.to_string]."] val debug_string_of_mbid : mod_bound_id -> string -(** @deprecated Same as [MBId.debug_to_string]. *) +[@@ocaml.deprecated "Same as [MBId.debug_to_string]."] (** {5 Names} *) -val name_eq : name -> name -> bool -(** @deprecated Same as [Name.equal]. *) +val name_eq : Name.t -> Name.t -> bool +[@@ocaml.deprecated "Same as [Name.equal]."] (** {5 Module paths} *) type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t - | MPdot of module_path * Label.t -(** @deprecated Alias type *) + | MPdot of ModPath.t * Label.t +[@@ocaml.deprecated "Alias type"] -val mp_ord : module_path -> module_path -> int -(** @deprecated Same as [ModPath.compare]. *) +val mp_ord : ModPath.t -> ModPath.t -> int +[@@ocaml.deprecated "Same as [ModPath.compare]."] -val mp_eq : module_path -> module_path -> bool -(** @deprecated Same as [ModPath.equal]. *) +val mp_eq : ModPath.t -> ModPath.t -> bool +[@@ocaml.deprecated "Same as [ModPath.equal]."] -val check_bound_mp : module_path -> bool -(** @deprecated Same as [ModPath.is_bound]. *) +val check_bound_mp : ModPath.t -> bool +[@@ocaml.deprecated "Same as [ModPath.is_bound]."] -val string_of_mp : module_path -> string -(** @deprecated Same as [ModPath.to_string]. *) +val string_of_mp : ModPath.t -> string +[@@ocaml.deprecated "Same as [ModPath.to_string]."] -val initial_path : module_path -(** @deprecated Same as [ModPath.initial]. *) +val initial_path : ModPath.t +[@@ocaml.deprecated "Same as [ModPath.initial]."] (** {5 Kernel names} *) type kernel_name = KerName.t -(** @deprecated Alias type *) +[@@ocaml.deprecated "Alias type"] -val make_kn : ModPath.t -> DirPath.t -> Label.t -> kernel_name -(** @deprecated Same as [KerName.make]. *) +val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t +[@@ocaml.deprecated "Same as [KerName.make]."] -val repr_kn : kernel_name -> module_path * DirPath.t * Label.t -(** @deprecated Same as [KerName.repr]. *) +val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t +[@@ocaml.deprecated "Same as [KerName.repr]."] -val modpath : kernel_name -> module_path -(** @deprecated Same as [KerName.modpath]. *) +val modpath : KerName.t -> ModPath.t +[@@ocaml.deprecated "Same as [KerName.modpath]."] -val label : kernel_name -> Label.t -(** @deprecated Same as [KerName.label]. *) +val label : KerName.t -> Label.t +[@@ocaml.deprecated "Same as [KerName.label]."] -val string_of_kn : kernel_name -> string -(** @deprecated Same as [KerName.to_string]. *) +val string_of_kn : KerName.t -> string +[@@ocaml.deprecated "Same as [KerName.to_string]."] -val pr_kn : kernel_name -> Pp.t -(** @deprecated Same as [KerName.print]. *) +val pr_kn : KerName.t -> Pp.t +[@@ocaml.deprecated "Same as [KerName.print]."] -val kn_ord : kernel_name -> kernel_name -> int -(** @deprecated Same as [KerName.compare]. *) +val kn_ord : KerName.t -> KerName.t -> int +[@@ocaml.deprecated "Same as [KerName.compare]."] (** {5 Constant names} *) type constant = Constant.t -(** @deprecated Alias type *) +[@@ocaml.deprecated "Alias type"] module Projection : sig type t - - val make : constant -> bool -> t + + val make : Constant.t -> bool -> t module SyntacticOrd : sig val compare : t -> t -> int @@ -717,7 +720,7 @@ module Projection : sig val hash : t -> int end - val constant : t -> constant + val constant : t -> Constant.t val unfolded : t -> bool val unfold : t -> t @@ -727,8 +730,8 @@ module Projection : sig (** Hashconsing of projections. *) val compare : t -> t -> int - - val map : (constant -> constant) -> t -> t + + val map : (Constant.t -> Constant.t) -> t -> t val to_string : t -> string val print : t -> Pp.t @@ -737,100 +740,100 @@ end type projection = Projection.t -val constant_of_kn_equiv : KerName.t -> KerName.t -> constant -(** @deprecated Same as [Constant.make] *) +val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t +[@@ocaml.deprecated "Same as [Constant.make]"] -val constant_of_kn : KerName.t -> constant -(** @deprecated Same as [Constant.make1] *) +val constant_of_kn : KerName.t -> Constant.t +[@@ocaml.deprecated "Same as [Constant.make1]"] -val make_con : ModPath.t -> DirPath.t -> Label.t -> constant -(** @deprecated Same as [Constant.make3] *) +val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t +[@@ocaml.deprecated "Same as [Constant.make3]"] -val repr_con : constant -> ModPath.t * DirPath.t * Label.t -(** @deprecated Same as [Constant.repr3] *) +val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t +[@@ocaml.deprecated "Same as [Constant.repr3]"] -val user_con : constant -> KerName.t -(** @deprecated Same as [Constant.user] *) +val user_con : Constant.t -> KerName.t +[@@ocaml.deprecated "Same as [Constant.user]"] -val canonical_con : constant -> KerName.t -(** @deprecated Same as [Constant.canonical] *) +val canonical_con : Constant.t -> KerName.t +[@@ocaml.deprecated "Same as [Constant.canonical]"] -val con_modpath : constant -> ModPath.t -(** @deprecated Same as [Constant.modpath] *) +val con_modpath : Constant.t -> ModPath.t +[@@ocaml.deprecated "Same as [Constant.modpath]"] -val con_label : constant -> Label.t -(** @deprecated Same as [Constant.label] *) +val con_label : Constant.t -> Label.t +[@@ocaml.deprecated "Same as [Constant.label]"] -val eq_constant : constant -> constant -> bool -(** @deprecated Same as [Constant.equal] *) +val eq_constant : Constant.t -> Constant.t -> bool +[@@ocaml.deprecated "Same as [Constant.equal]"] -val con_ord : constant -> constant -> int -(** @deprecated Same as [Constant.CanOrd.compare] *) +val con_ord : Constant.t -> Constant.t -> int +[@@ocaml.deprecated "Same as [Constant.CanOrd.compare]"] -val con_user_ord : constant -> constant -> int -(** @deprecated Same as [Constant.UserOrd.compare] *) +val con_user_ord : Constant.t -> Constant.t -> int +[@@ocaml.deprecated "Same as [Constant.UserOrd.compare]"] -val con_with_label : constant -> Label.t -> constant -(** @deprecated Same as [Constant.change_label] *) +val con_with_label : Constant.t -> Label.t -> Constant.t +[@@ocaml.deprecated "Same as [Constant.change_label]"] -val string_of_con : constant -> string -(** @deprecated Same as [Constant.to_string] *) +val string_of_con : Constant.t -> string +[@@ocaml.deprecated "Same as [Constant.to_string]"] -val pr_con : constant -> Pp.t -(** @deprecated Same as [Constant.print] *) +val pr_con : Constant.t -> Pp.t +[@@ocaml.deprecated "Same as [Constant.print]"] -val debug_pr_con : constant -> Pp.t -(** @deprecated Same as [Constant.debug_print] *) +val debug_pr_con : Constant.t -> Pp.t +[@@ocaml.deprecated "Same as [Constant.debug_print]"] -val debug_string_of_con : constant -> string -(** @deprecated Same as [Constant.debug_to_string] *) +val debug_string_of_con : Constant.t -> string +[@@ocaml.deprecated "Same as [Constant.debug_to_string]"] (** {5 Mutual Inductive names} *) type mutual_inductive = MutInd.t -(** @deprecated Alias type *) +[@@ocaml.deprecated "Alias type"] -val mind_of_kn : KerName.t -> mutual_inductive -(** @deprecated Same as [MutInd.make1] *) +val mind_of_kn : KerName.t -> MutInd.t +[@@ocaml.deprecated "Same as [MutInd.make1]"] -val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive -(** @deprecated Same as [MutInd.make] *) +val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t +[@@ocaml.deprecated "Same as [MutInd.make]"] -val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive -(** @deprecated Same as [MutInd.make3] *) +val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t +[@@ocaml.deprecated "Same as [MutInd.make3]"] -val user_mind : mutual_inductive -> KerName.t -(** @deprecated Same as [MutInd.user] *) +val user_mind : MutInd.t -> KerName.t +[@@ocaml.deprecated "Same as [MutInd.user]"] -val canonical_mind : mutual_inductive -> KerName.t -(** @deprecated Same as [MutInd.canonical] *) +val canonical_mind : MutInd.t -> KerName.t +[@@ocaml.deprecated "Same as [MutInd.canonical]"] -val repr_mind : mutual_inductive -> ModPath.t * DirPath.t * Label.t -(** @deprecated Same as [MutInd.repr3] *) +val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t +[@@ocaml.deprecated "Same as [MutInd.repr3]"] -val eq_mind : mutual_inductive -> mutual_inductive -> bool -(** @deprecated Same as [MutInd.equal] *) +val eq_mind : MutInd.t -> MutInd.t -> bool +[@@ocaml.deprecated "Same as [MutInd.equal]"] -val mind_ord : mutual_inductive -> mutual_inductive -> int -(** @deprecated Same as [MutInd.CanOrd.compare] *) +val mind_ord : MutInd.t -> MutInd.t -> int +[@@ocaml.deprecated "Same as [MutInd.CanOrd.compare]"] -val mind_user_ord : mutual_inductive -> mutual_inductive -> int -(** @deprecated Same as [MutInd.UserOrd.compare] *) +val mind_user_ord : MutInd.t -> MutInd.t -> int +[@@ocaml.deprecated "Same as [MutInd.UserOrd.compare]"] -val mind_label : mutual_inductive -> Label.t -(** @deprecated Same as [MutInd.label] *) +val mind_label : MutInd.t -> Label.t +[@@ocaml.deprecated "Same as [MutInd.label]"] -val mind_modpath : mutual_inductive -> ModPath.t -(** @deprecated Same as [MutInd.modpath] *) +val mind_modpath : MutInd.t -> ModPath.t +[@@ocaml.deprecated "Same as [MutInd.modpath]"] -val string_of_mind : mutual_inductive -> string -(** @deprecated Same as [MutInd.to_string] *) +val string_of_mind : MutInd.t -> string +[@@ocaml.deprecated "Same as [MutInd.to_string]"] -val pr_mind : mutual_inductive -> Pp.t -(** @deprecated Same as [MutInd.print] *) +val pr_mind : MutInd.t -> Pp.t +[@@ocaml.deprecated "Same as [MutInd.print]"] -val debug_pr_mind : mutual_inductive -> Pp.t -(** @deprecated Same as [MutInd.debug_print] *) +val debug_pr_mind : MutInd.t -> Pp.t +[@@ocaml.deprecated "Same as [MutInd.debug_print]"] -val debug_string_of_mind : mutual_inductive -> string -(** @deprecated Same as [MutInd.debug_to_string] *) +val debug_string_of_mind : MutInd.t -> string +[@@ocaml.deprecated "Same as [MutInd.debug_to_string]"] diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 6e9991ac54..bb4c2585d9 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -25,7 +25,7 @@ to OCaml code. *) (** Local names **) (* The first component is there for debugging purposes only *) -type lname = { lname : name; luid : int } +type lname = { lname : Name.t; luid : int } let eq_lname ln1 ln2 = Int.equal ln1.luid ln2.luid @@ -50,13 +50,13 @@ let fresh_lname n = type gname = | Gind of string * inductive (* prefix, inductive name *) | Gconstruct of string * constructor (* prefix, constructor name *) - | Gconstant of string * constant (* prefix, constant name *) - | Gproj of string * constant (* prefix, constant name *) - | Gcase of label option * int - | Gpred of label option * int - | Gfixtype of label option * int - | Gnorm of label option * int - | Gnormtbl of label option * int + | Gconstant of string * Constant.t (* prefix, constant name *) + | Gproj of string * Constant.t (* prefix, constant name *) + | Gcase of Label.t option * int + | Gpred of Label.t option * int + | Gfixtype of Label.t option * int + | Gnorm of Label.t option * int + | Gnormtbl of Label.t option * int | Ginternal of string | Grel of int | Gnamed of Id.t @@ -143,8 +143,8 @@ let fresh_gnormtbl l = type symbol = | SymbValue of Nativevalues.t | SymbSort of sorts - | SymbName of name - | SymbConst of constant + | SymbName of Name.t + | SymbConst of Constant.t | SymbMatch of annot_sw | SymbInd of inductive | SymbMeta of metavariable @@ -296,7 +296,7 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of CPrimitives.t * (prefix * constant) option + | Coq_primitive of CPrimitives.t * (prefix * Constant.t) option let eq_primitive p1 p2 = match p1, p2 with @@ -921,7 +921,7 @@ let merge_branches t = type prim_aux = - | PAprim of string * constant * CPrimitives.t * prim_aux array + | PAprim of string * Constant.t * CPrimitives.t * prim_aux array | PAml of mllambda let add_check cond args = @@ -1504,7 +1504,7 @@ let string_of_dirpath = function (* OCaml as a module identifier. *) let string_of_dirpath s = "N"^string_of_dirpath s -let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir) +let mod_uid_of_dirpath dir = string_of_dirpath (DirPath.repr dir) let link_info_of_dirpath dir = Linked (mod_uid_of_dirpath dir ^ ".") @@ -1523,19 +1523,19 @@ let string_of_label_def l = let rec list_of_mp acc = function | MPdot (mp,l) -> list_of_mp (string_of_label l::acc) mp | MPfile dp -> - let dp = repr_dirpath dp in + let dp = DirPath.repr dp in string_of_dirpath dp :: acc - | MPbound mbid -> ("X"^string_of_id (id_of_mbid mbid))::acc + | MPbound mbid -> ("X"^string_of_id (MBId.to_id mbid))::acc let list_of_mp mp = list_of_mp [] mp let string_of_kn kn = - let (mp,dp,l) = repr_kn kn in + let (mp,dp,l) = KerName.repr kn in let mp = list_of_mp mp in String.concat "_" mp ^ "_" ^ string_of_label l -let string_of_con c = string_of_kn (user_con c) -let string_of_mind mind = string_of_kn (user_mind mind) +let string_of_con c = string_of_kn (Constant.user c) +let string_of_mind mind = string_of_kn (MutInd.user mind) let string_of_gname g = match g with @@ -1877,7 +1877,7 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix in - let l = con_label con in + let l = Constant.label con in let auxdefs,code = if no_univs then compile_with_fv env sigma None [] (Some l) code else diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index ae6fb1bd6b..764598097d 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -34,9 +34,9 @@ val get_value : symbols -> int -> Nativevalues.t val get_sort : symbols -> int -> sorts -val get_name : symbols -> int -> name +val get_name : symbols -> int -> Name.t -val get_const : symbols -> int -> constant +val get_const : symbols -> int -> Constant.t val get_match : symbols -> int -> Nativevalues.annot_sw @@ -60,20 +60,20 @@ val empty_updates : code_location_updates val register_native_file : string -> unit -val compile_constant_field : env -> string -> constant -> +val compile_constant_field : env -> string -> Constant.t -> global list -> constant_body -> global list -val compile_mind_field : string -> module_path -> label -> +val compile_mind_field : string -> ModPath.t -> Label.t -> global list -> mutual_inductive_body -> global list val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code val mk_norm_code : env -> evars -> string -> constr -> linkable_code -val mk_library_header : dir_path -> global list +val mk_library_header : DirPath.t -> global list -val mod_uid_of_dirpath : dir_path -> string +val mod_uid_of_dirpath : DirPath.t -> string -val link_info_of_dirpath : dir_path -> link_info +val link_info_of_dirpath : DirPath.t -> link_info val update_locations : code_location_updates -> unit diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 73f18f7a7b..b2c8662da0 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -20,17 +20,17 @@ type uint = | UintDecomp of prefix * constructor * lambda and lambda = - | Lrel of name * int + | Lrel of Name.t * int | Lvar of Id.t | Lmeta of metavariable * lambda (* type *) | Levar of existential * lambda (* type *) | Lprod of lambda * lambda - | Llam of name array * lambda - | Llet of name * lambda * lambda + | Llam of Name.t array * lambda + | Llet of Name.t * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant - | Lproj of prefix * constant (* prefix, projection name *) - | Lprim of prefix * constant * CPrimitives.t * lambda array + | Lproj of prefix * Constant.t (* prefix, projection name *) + | Lprim of prefix * Constant.t * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda @@ -48,6 +48,6 @@ and lambda = | Llazy | Lforce -and lam_branches = (constructor * name array * lambda) array +and lam_branches = (constructor * Name.t array * lambda) array -and fix_decl = name array * lambda array * lambda array +and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 508112b35d..aaa9f9b002 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -378,7 +378,7 @@ module Renv = type constructor_info = tag * int * int (* nparam nrealargs *) type t = { - name_rel : name Vect.t; + name_rel : Name.t Vect.t; construct_tbl : constructor_info ConstrTable.t; } diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 156e4f834a..392961f5d8 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -18,13 +18,13 @@ type evars = val empty_evars : evars -val decompose_Llam : lambda -> Names.name array * lambda -val decompose_Llam_Llet : lambda -> (Names.name * lambda option) array * lambda +val decompose_Llam : lambda -> Name.t array * lambda +val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda val is_lazy : prefix -> constr -> bool val mk_lazy : lambda -> lambda -val get_mind_prefix : env -> mutual_inductive -> string +val get_mind_prefix : env -> MutInd.t -> string val get_alias : env -> pconstant -> pconstant @@ -38,5 +38,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array -> val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda -> lambda -val compile_prim : CPrimitives.t -> constant -> bool -> prefix -> lambda array -> +val compile_prim : CPrimitives.t -> Constant.t -> bool -> prefix -> lambda array -> lambda diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index a262a9f58a..b74d4fdd05 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -21,7 +21,7 @@ val get_ml_filename : unit -> string * string val compile : string -> global list -> profile:bool -> bool * string -val compile_library : Names.dir_path -> global list -> string -> bool +val compile_library : Names.DirPath.t -> global list -> string -> bool val call_linker : ?fatal:bool -> string -> string -> code_location_updates option -> unit diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 3e273dde20..c68f781213 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -26,7 +26,7 @@ let rec translate_mod prefix mp env mod_expr acc = and translate_field prefix mp env acc (l,x) = match x with | SFBconst cb -> - let con = make_con mp empty_dirpath l in + let con = Constant.make3 mp DirPath.empty l in (if !Flags.debug then let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Feedback.msg_debug (Pp.str msg)); diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index f327ba224a..72e3d80413 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -13,5 +13,5 @@ open Nativecode (** This file implements separate compilation for libraries in the native compiler *) -val dump_library : module_path -> dir_path -> env -> module_signature -> +val dump_library : ModPath.t -> DirPath.t -> env -> module_signature -> global list * symbols diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 1c9996d894..2f89200885 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -58,10 +58,10 @@ type atom = (* types, bodies, rec_pos, pos *) | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t - | Aprod of name * t * (t -> t) + | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of existential * t - | Aproj of constant * accumulator + | Aproj of Constant.t * accumulator let accumulate_tag = 0 diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 0e2db8486f..1368b4470e 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -49,27 +49,27 @@ type atom = | Afix of t array * t array * rec_pos * int | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t - | Aprod of name * t * (t -> t) + | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of existential * t - | Aproj of constant * accumulator + | Aproj of Constant.t * accumulator (* Constructors *) val mk_accu : atom -> t val mk_rel_accu : int -> t val mk_rels_accu : int -> int -> t array -val mk_constant_accu : constant -> Univ.Level.t array -> t +val mk_constant_accu : Constant.t -> Univ.Level.t array -> t val mk_ind_accu : inductive -> Univ.Level.t array -> t val mk_sort_accu : sorts -> Univ.Level.t array -> t val mk_var_accu : Id.t -> t val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t) -val mk_prod_accu : name -> t -> t -> t +val mk_prod_accu : Name.t -> t -> t -> t val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t val mk_evar_accu : existential -> t -> t -val mk_proj_accu : constant -> accumulator -> t +val mk_proj_accu : Constant.t -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t val mk_const : tag -> t diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index f2a009b868..27f9511e17 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -88,9 +88,9 @@ val env_of_named : Id.t -> env -> env (** Global constants *) -val lookup_constant_key : constant -> env -> constant_key -val lookup_constant : constant -> env -> constant_body +val lookup_constant_key : Constant.t -> env -> constant_key +val lookup_constant : Constant.t -> env -> constant_body (** Mutual Inductives *) -val lookup_mind_key : mutual_inductive -> env -> mind_key -val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +val lookup_mind_key : MutInd.t -> env -> mind_key +val lookup_mind : MutInd.t -> env -> mutual_inductive_body diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2bf9f43a5a..79a35d292d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -62,7 +62,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of constant * lift + | Zlproj of Constant.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -239,7 +239,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (eq_constant c1 c2) then + if not (Constant.equal c1 c2) then raise NotConvertible else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fd024b2157..0e416b3e53 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -114,7 +114,7 @@ module DPMap = Map.Make(DirPath) type safe_environment = { env : Environ.env; - modpath : module_path; + modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; paramresolver : Mod_subst.delta_resolver; @@ -125,7 +125,7 @@ type safe_environment = future_cst : Univ.ContextSet.t Future.computation list; engagement : engagement option; required : vodigest DPMap.t; - loads : (module_path * module_body) list; + loads : (ModPath.t * module_body) list; local_retroknowledge : Retroknowledge.action list; native_symbols : Nativecode.symbols DPMap.t } @@ -143,7 +143,7 @@ let rec library_dp_of_senv senv = let empty_environment = { env = Environ.empty_env; - modpath = initial_path; + modpath = ModPath.initial; modvariant = NONE; modresolver = Mod_subst.empty_delta_resolver; paramresolver = Mod_subst.empty_delta_resolver; @@ -160,7 +160,7 @@ let empty_environment = let is_initial senv = match senv.revstruct, senv.modvariant with - | [], NONE -> ModPath.equal senv.modpath initial_path + | [], NONE -> ModPath.equal senv.modpath ModPath.initial | _ -> false let delta_of_senv senv = senv.modresolver,senv.paramresolver @@ -458,8 +458,8 @@ let constraints_of_sfb env sfb = It also performs the corresponding [add_constraints]. *) type generic_name = - | C of constant - | I of mutual_inductive + | C of Constant.t + | I of MutInd.t | M (** name already known, cf the mod_mp field *) | MT (** name already known, cf the mod_mp field *) @@ -502,7 +502,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constant_role + Constant.t * private_constant_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in @@ -521,7 +521,7 @@ let add_constant_aux no_section senv (kn, cb) = let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver - (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv' + (Mod_subst.add_inline_delta_resolver (Constant.user kn) (lev,None)) senv' | _ -> senv' in senv'' @@ -535,7 +535,7 @@ let export_private_constants ~in_section ce senv = (ce, exported), senv let add_constant dir l decl senv = - let kn = make_con senv.modpath dir l in + let kn = Constant.make3 senv.modpath dir l in let no_section = DirPath.is_empty dir in let senv = let cb = @@ -562,7 +562,7 @@ let check_mind mie lab = let add_mind dir l mie senv = let () = check_mind mie l in - let kn = make_mind senv.modpath dir l in + let kn = MutInd.make3 senv.modpath dir l in let mib = Term_typing.translate_mind senv.env kn mie in let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f0f273f354..ee96329447 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -60,8 +60,8 @@ val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> constant -> private_constant -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant +val private_con_of_con : safe_environment -> Constant.t -> private_constant +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : @@ -103,7 +103,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constant_role + Constant.t * private_constant_role val export_private_constants : in_section:bool -> private_constants Entries.constant_entry -> @@ -113,22 +113,22 @@ val export_private_constants : in_section:bool -> unless one requires the side effects to be exported) *) val add_constant : DirPath.t -> Label.t -> global_declaration -> - constant safe_transformer + Constant.t safe_transformer (** Adding an inductive type *) val add_mind : DirPath.t -> Label.t -> Entries.mutual_inductive_entry -> - mutual_inductive safe_transformer + MutInd.t safe_transformer (** Adding a module or a module type *) val add_module : Label.t -> Entries.module_entry -> Declarations.inline -> - (module_path * Mod_subst.delta_resolver) safe_transformer + (ModPath.t * Mod_subst.delta_resolver) safe_transformer val add_modtype : Label.t -> Entries.module_type_entry -> Declarations.inline -> - module_path safe_transformer + ModPath.t safe_transformer (** Adding universe constraints *) @@ -150,9 +150,9 @@ val set_typing_flags : Declarations.typing_flags -> safe_transformer0 (** {6 Interactive module functions } *) -val start_module : Label.t -> module_path safe_transformer +val start_module : Label.t -> ModPath.t safe_transformer -val start_modtype : Label.t -> module_path safe_transformer +val start_modtype : Label.t -> ModPath.t safe_transformer val add_module_parameter : MBId.t -> Entries.module_struct_entry -> Declarations.inline -> @@ -166,17 +166,17 @@ val allow_delayed_constants : bool ref val end_module : Label.t -> (Entries.module_struct_entry * Declarations.inline) option -> - (module_path * MBId.t list * Mod_subst.delta_resolver) safe_transformer + (ModPath.t * MBId.t list * Mod_subst.delta_resolver) safe_transformer -val end_modtype : Label.t -> (module_path * MBId.t list) safe_transformer +val end_modtype : Label.t -> (ModPath.t * MBId.t list) safe_transformer val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer -val current_modpath : safe_environment -> module_path +val current_modpath : safe_environment -> ModPath.t -val current_dirpath : safe_environment -> dir_path +val current_dirpath : safe_environment -> DirPath.t (** {6 Libraries : loading and saving compilation units } *) @@ -186,16 +186,16 @@ type native_library = Nativecode.global list val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols -val start_library : DirPath.t -> module_path safe_transformer +val start_library : DirPath.t -> ModPath.t safe_transformer val export : ?except:Future.UUIDSet.t -> safe_environment -> DirPath.t -> - module_path * compiled_library * native_library + ModPath.t * compiled_library * native_library (* Constraints are non empty iff the file is a vi2vo *) val import : compiled_library -> Univ.universe_context_set -> vodigest -> - module_path safe_transformer + ModPath.t safe_transformer (** {6 Safe typing judgments } *) @@ -223,7 +223,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a val register : field -> Retroknowledge.entry -> Term.constr -> safe_transformer0 -val register_inline : constant -> safe_transformer0 +val register_inline : Constant.t -> safe_transformer0 val set_strategy : - safe_environment -> Names.constant Names.tableKey -> Conv_oracle.level -> safe_environment + safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index b564b2a8c1..d8e281d524 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -63,11 +63,11 @@ let empty_labmap = { objs = Label.Map.empty; mods = Label.Map.empty } let get_obj mp map l = try Label.Map.find l map.objs - with Not_found -> error_no_such_label_sub l (string_of_mp mp) + with Not_found -> error_no_such_label_sub l (ModPath.to_string mp) let get_mod mp map l = try Label.Map.find l map.mods - with Not_found -> error_no_such_label_sub l (string_of_mp mp) + with Not_found -> error_no_such_label_sub l (ModPath.to_string mp) let make_labmap mp list = let add_one (l,e) map = @@ -181,7 +181,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in cst in - let mind = mind_of_kn kn1 in + let mind = MutInd.make1 kn1 in let check_cons_types i cst p1 p2 = Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst diff --git a/kernel/term.ml b/kernel/term.ml index 0e0af2f59d..161abfba12 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -67,7 +67,7 @@ type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint type 'a puniverses = 'a Univ.puniverses (** Simply type aliases *) -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -83,7 +83,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of (constant * 'univs) + | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array diff --git a/kernel/term.mli b/kernel/term.mli index d5aaf6ad06..051979180c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -26,7 +26,7 @@ type sorts_family = Sorts.family = InProp | InSet | InType type 'a puniverses = 'a Univ.puniverses (** Simply type aliases *) -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -80,7 +80,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of (constant * 'univs) + | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array @@ -165,7 +165,7 @@ val decompose_app : constr -> constr * constr list val decompose_appvect : constr -> constr * constr array (** Destructs a constant *) -val destConst : constr -> constant puniverses +val destConst : constr -> Constant.t puniverses (** Destructs an existential variable *) val destEvar : constr -> existential @@ -415,11 +415,11 @@ val mkProd : Name.t * types * types -> types val mkLambda : Name.t * types * constr -> constr val mkLetIn : Name.t * constr * types * constr -> constr val mkApp : constr * constr array -> constr -val mkConst : constant -> constr +val mkConst : Constant.t -> constr val mkProj : projection * constr -> constr val mkInd : inductive -> constr val mkConstruct : constructor -> constr -val mkConstU : constant puniverses -> constr +val mkConstU : Constant.t puniverses -> constr val mkIndU : inductive puniverses -> constr val mkConstructU : constructor puniverses -> constr val mkConstructUi : (pinductive * int) -> constr diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e28c8e8267..d50abf0717 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -525,7 +525,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effect_role + Constant.t * constant_body * side_effect_role let export_side_effects mb env ce = match ce with diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index b16f81c5a6..815269169a 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -47,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list val equal_eff : side_effect -> side_effect -> bool val translate_constant : - 'a trust -> env -> constant -> 'a constant_entry -> + 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body type side_effect_role = @@ -55,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effect_role + Constant.t * constant_body * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -66,14 +66,14 @@ val export_side_effects : exported_side_effect list * unit constant_entry val translate_mind : - env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body + env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body -val translate_recipe : env -> constant -> Cooking.recipe -> constant_body +val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> constant option -> +val infer_declaration : trust:'a trust -> env -> Constant.t option -> 'a constant_entry -> Cooking.result val build_constant_declaration : - constant -> env -> Cooking.result -> constant_body + Constant.t -> env -> Cooking.result -> constant_body diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b40badd7c8..f99f34b06a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -298,7 +298,7 @@ let type_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); + assert(MutInd.equal pb.proj_ind (fst ind)); let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in substl (c :: List.rev args) ty diff --git a/kernel/vars.ml b/kernel/vars.ml index d0dad02ece..f52d734eff 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -354,5 +354,5 @@ let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else Context.Rel.map (fun x -> subst_instance_constr s x) ctx -type id_key = constant tableKey +type id_key = Constant.t tableKey let eq_id_key x y = Names.eq_table_key Constant.equal x y diff --git a/kernel/vars.mli b/kernel/vars.mli index 59dc09a75d..ae846fd42f 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -144,5 +144,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Co val subst_instance_constr : universe_instance -> constr -> constr val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t -type id_key = constant tableKey +type id_key = Constant.t tableKey val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vm.ml b/kernel/vm.ml index 6b7a86d6f9..4e13881b87 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -357,7 +357,7 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = constant tableKey + type t = Constant.t tableKey let equal = Names.eq_table_key Constant.equal open Hashset.Combine let hash = function @@ -654,10 +654,10 @@ let apply_whd k whd = let rec pr_atom a = Pp.(match a with | Aid c -> str "Aid(" ++ (match c with - | ConstKey c -> Names.pr_con c + | ConstKey c -> Constant.print c | RelKey i -> str "#" ++ int i | _ -> str "...") ++ str ")" - | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" | Atype _ -> str "Atype(") and pr_whd w = Pp.(match w with @@ -679,4 +679,4 @@ and pr_zipper z = | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" | Zswitch s -> str "Zswitch(...)" - | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")") + | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") diff --git a/kernel/vm.mli b/kernel/vm.mli index df638acc1f..ea38ee43f6 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -59,7 +59,7 @@ val pr_stack : stack -> Pp.t val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values -val val_of_constant : constant -> values +val val_of_constant : Constant.t -> values external val_of_annot_switch : annot_switch -> values = "%identity" |