From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:58:27 +0100 Subject: [api] Deprecate all legacy uses of Names in core. This will allow to merge back `Names` with `API.Names` --- checker/cic.mli | 20 ++++++++++---------- checker/closure.ml | 12 ++++++------ checker/closure.mli | 14 +++++++------- checker/declarations.mli | 12 ++++++------ checker/environ.ml | 2 +- checker/environ.mli | 30 +++++++++++++++--------------- checker/indtypes.mli | 6 +++--- checker/inductive.mli | 2 +- checker/mod_checking.mli | 2 +- checker/modops.mli | 18 +++++++++--------- checker/term.mli | 4 ++-- checker/type_errors.ml | 6 +++--- checker/type_errors.mli | 10 +++++----- checker/values.ml | 2 +- 14 files changed, 70 insertions(+), 70 deletions(-) (limited to 'checker') diff --git a/checker/cic.mli b/checker/cic.mli index 753fd0fc0..354650964 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -81,7 +81,7 @@ type 'constr pfixpoint = type 'constr pcofixpoint = int * 'constr 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 @@ -127,12 +127,12 @@ type section_context = unit type delta_hint = | Inline of int * constr option - | Equiv of kernel_name + | Equiv of KerName.t -type delta_resolver = module_path MPmap.t * delta_hint KNmap.t +type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t type 'a umap_t = 'a MPmap.t * 'a MBImap.t -type substitution = (module_path * delta_resolver) umap_t +type substitution = (ModPath.t * delta_resolver) umap_t (** {6 Delayed constr} *) @@ -194,7 +194,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 : constr; (* Type under params *) @@ -241,7 +241,7 @@ type recarg = type wf_paths = recarg Rtree.t -type record_body = (Id.t * constant array * projection_body array) option +type record_body = (Id.t * Constant.t array * projection_body array) option (* The body is empty for non-primitive records, otherwise we get its binder name in projections and list of projections if it is primitive. *) @@ -347,12 +347,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.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 *) @@ -386,7 +386,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 *) (** algebraic type, kept if it's relevant for extraction *) diff --git a/checker/closure.ml b/checker/closure.ml index 70718bfdc..7982ffa7a 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -63,7 +63,7 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : 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 @@ -86,7 +86,7 @@ module RedFlags = (struct r_iota : bool } type red_kind = BETA | DELTA | IOTA | ZETA - | CONST of constant | VAR of Id.t + | CONST of Constant.t | VAR of Id.t let fBETA = BETA let fDELTA = DELTA let fIOTA = IOTA @@ -165,7 +165,7 @@ type 'a tableKey = | VarKey of Id.t | RelKey of int -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey module KeyHash = struct @@ -281,9 +281,9 @@ and fterm = | FCoFix of cofixpoint * fconstr subs | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *) | FLIFT of int * fconstr | FCLOS of constr * fconstr subs diff --git a/checker/closure.mli b/checker/closure.mli index ed5bb3d09..957cc4adb 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -30,7 +30,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 @@ -42,7 +42,7 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : 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 *) @@ -71,7 +71,7 @@ type 'a tableKey = | VarKey of Id.t | RelKey of int -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option @@ -100,9 +100,9 @@ type fterm = | FCoFix of cofixpoint * fconstr subs | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential_key * fconstr array | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -142,7 +142,7 @@ val inject : constr -> fconstr val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : - (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr + (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr (* Global and local constant cache *) type clos_infos diff --git a/checker/declarations.mli b/checker/declarations.mli index 6fc71bb94..7458b3e0b 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -34,12 +34,12 @@ val empty_delta_resolver : delta_resolver type 'a subst_fun = substitution -> 'a -> 'a val empty_subst : substitution -val add_mbid : MBId.t -> module_path -> substitution -> substitution -val add_mp : module_path -> module_path -> substitution -> substitution -val map_mbid : MBId.t -> module_path -> substitution -val map_mp : module_path -> module_path -> substitution -val mp_in_delta : module_path -> delta_resolver -> bool -val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive +val add_mbid : MBId.t -> ModPath.t -> substitution -> substitution +val add_mp : ModPath.t -> ModPath.t -> substitution -> substitution +val map_mbid : MBId.t -> ModPath.t -> substitution +val map_mp : ModPath.t -> ModPath.t -> substitution +val mp_in_delta : ModPath.t -> delta_resolver -> bool +val mind_of_delta : delta_resolver -> MutInd.t -> MutInd.t val subst_const_body : constant_body subst_fun val subst_mind : mutual_inductive_body subst_fun diff --git a/checker/environ.ml b/checker/environ.ml index a0818012c..9db0d60e8 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -8,7 +8,7 @@ open Declarations type globals = { env_constants : constant_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; - env_inductives_eq : kernel_name KNmap.t; + env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} diff --git a/checker/environ.mli b/checker/environ.mli index 8e8d0fd49..6bda838f8 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -6,7 +6,7 @@ open Cic type globals = { env_constants : constant_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; - env_inductives_eq : kernel_name KNmap.t; + env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} type stratification = { @@ -34,7 +34,7 @@ val rel_context : env -> rel_context val lookup_rel : int -> env -> rel_declaration val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env -val push_rec_types : name array * constr array * 'a -> env -> env +val push_rec_types : Name.t array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes @@ -44,31 +44,31 @@ val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) -val lookup_constant : constant -> env -> Cic.constant_body -val add_constant : constant -> Cic.constant_body -> env -> env -val constant_type : env -> constant puniverses -> constr Univ.constrained +val lookup_constant : Constant.t -> env -> Cic.constant_body +val add_constant : Constant.t -> Cic.constant_body -> env -> env +val constant_type : env -> Constant.t puniverses -> constr Univ.constrained type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant puniverses -> constr -val evaluable_constant : constant -> env -> bool +val constant_value : env -> Constant.t puniverses -> constr +val evaluable_constant : Constant.t -> env -> bool -val is_projection : constant -> env -> bool +val is_projection : Constant.t -> env -> bool val lookup_projection : projection -> env -> projection_body (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool val lookup_mind : - mutual_inductive -> env -> Cic.mutual_inductive_body + MutInd.t -> env -> Cic.mutual_inductive_body val add_mind : - mutual_inductive -> Cic.mutual_inductive_body -> env -> env + MutInd.t -> Cic.mutual_inductive_body -> env -> env (* Modules *) val add_modtype : - module_path -> Cic.module_type_body -> env -> env + ModPath.t -> Cic.module_type_body -> env -> env val shallow_add_module : - module_path -> Cic.module_body -> env -> env -val shallow_remove_module : module_path -> env -> env -val lookup_module : module_path -> env -> Cic.module_body -val lookup_modtype : module_path -> env -> Cic.module_type_body + ModPath.t -> Cic.module_body -> env -> env +val shallow_remove_module : ModPath.t -> env -> env +val lookup_module : ModPath.t -> env -> Cic.module_body +val lookup_modtype : ModPath.t -> env -> Cic.module_type_body diff --git a/checker/indtypes.mli b/checker/indtypes.mli index b0554989e..5d4c3ee99 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -12,8 +12,8 @@ open Cic open Environ (*i*) -val prkn : kernel_name -> Pp.t -val prcon : constant -> Pp.t +val prkn : KerName.t -> Pp.t +val prcon : Constant.t -> Pp.t (*s The different kinds of errors that may result of a malformed inductive definition. *) @@ -34,4 +34,4 @@ exception InductiveError of inductive_error (*s The following function does checks on inductive declarations. *) -val check_inductive : env -> mutual_inductive -> mutual_inductive_body -> env +val check_inductive : env -> MutInd.t -> mutual_inductive_body -> env diff --git a/checker/inductive.mli b/checker/inductive.mli index 8f605935d..0170bbc94 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -31,7 +31,7 @@ val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) val type_of_constructor : pconstructor -> mind_specif -> constr -val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array +val arities_of_specif : MutInd.t puniverses -> mind_specif -> constr array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index 16a3792aa..c7af8b286 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -6,4 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val check_module : Environ.env -> Names.module_path -> Cic.module_body -> unit +val check_module : Environ.env -> Names.ModPath.t -> Cic.module_body -> unit diff --git a/checker/modops.mli b/checker/modops.mli index 0efff63c8..b73557d92 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -15,7 +15,7 @@ open Environ (* Various operations on modules and module types *) val module_type_of_module : - module_path option -> module_body -> module_type_body + ModPath.t option -> module_body -> module_type_body val is_functor : ('ty,'a) functorize -> bool @@ -24,24 +24,24 @@ val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize (* adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env -val add_module_type : module_path -> module_type_body -> env -> env +val add_module_type : ModPath.t -> module_type_body -> env -> env -val strengthen : module_type_body -> module_path -> module_type_body +val strengthen : module_type_body -> ModPath.t -> module_type_body -val subst_and_strengthen : module_body -> module_path -> module_body +val subst_and_strengthen : module_body -> ModPath.t -> module_body val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a -val error_not_match : label -> structure_field_body -> 'a +val error_not_match : Label.t -> structure_field_body -> 'a val error_with_module : unit -> 'a -val error_no_such_label : label -> 'a +val error_no_such_label : Label.t -> 'a val error_no_such_label_sub : - label -> module_path -> 'a + Label.t -> ModPath.t -> 'a -val error_not_a_constant : label -> 'a +val error_not_a_constant : Label.t -> 'a -val error_not_a_module : label -> 'a +val error_not_a_module : Label.t -> 'a diff --git a/checker/term.mli b/checker/term.mli index 679a56ee4..2524dff18 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -38,8 +38,8 @@ val fold_rel_context_outside : val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration val map_rel_context : (constr -> constr) -> rel_context -> rel_context val extended_rel_list : int -> rel_context -> constr list -val compose_lam : (name * constr) list -> constr -> constr -val decompose_lam : constr -> (name * constr) list * constr +val compose_lam : (Name.t * constr) list -> constr -> constr +val decompose_lam : constr -> (Name.t * constr) list * constr val decompose_lam_n_assum : int -> constr -> rel_context * constr val mkProd_or_LetIn : rel_declaration -> constr -> constr val it_mkProd_or_LetIn : constr -> rel_context -> constr diff --git a/checker/type_errors.ml b/checker/type_errors.ml index c5a69efdc..5794d8713 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -52,14 +52,14 @@ type type_error = | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int | IllFormedBranch of constr * int * constr * constr - | Generalization of (name * constr) * unsafe_judgment + | Generalization of (Name.t * constr) * unsafe_judgment | ActualType of unsafe_judgment * constr | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int + | IllFormedRecBody of guard_error * Name.t array * int | IllTypedRecBody of - int * name array * unsafe_judgment array * constr array + int * Name.t array * unsafe_judgment array * constr array | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error diff --git a/checker/type_errors.mli b/checker/type_errors.mli index b5f14c718..f45144c23 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -54,14 +54,14 @@ type type_error = | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int | IllFormedBranch of constr * int * constr * constr - | Generalization of (name * constr) * unsafe_judgment + | Generalization of (Name.t * constr) * unsafe_judgment | ActualType of unsafe_judgment * constr | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int + | IllFormedRecBody of guard_error * Name.t array * int | IllTypedRecBody of - int * name array * unsafe_judgment array * constr array + int * Name.t array * unsafe_judgment array * constr array | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error @@ -96,9 +96,9 @@ val error_cant_apply_bad_type : unsafe_judgment -> unsafe_judgment array -> 'a val error_ill_formed_rec_body : - env -> guard_error -> name array -> int -> 'a + env -> guard_error -> Name.t array -> int -> 'a val error_ill_typed_rec_body : - env -> int -> name array -> unsafe_judgment array -> constr array -> 'a + env -> int -> Name.t array -> unsafe_judgment array -> constr array -> 'a val error_unsatisfied_constraints : env -> Univ.constraints -> 'a diff --git a/checker/values.ml b/checker/values.ml index 86634fbd8..9e16c8435 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli +MD5 f4b00c567a972ae950b9ed10c533fda5 checker/cic.mli *) -- cgit v1.2.3