aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checkInductive.ml2
-rw-r--r--kernel/cooking.ml10
-rw-r--r--kernel/entries.ml2
-rw-r--r--kernel/indTyping.ml67
-rw-r--r--kernel/inferCumulativity.ml24
-rw-r--r--kernel/inferCumulativity.mli4
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/safe_typing.ml1
-rw-r--r--vernac/comInductive.ml11
-rw-r--r--vernac/comInductive.mli32
-rw-r--r--vernac/record.ml4
11 files changed, 37 insertions, 122 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index d20eea7874..06ee4fcc7a 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -61,7 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
mind_entry_params = mb.mind_params_ctxt;
mind_entry_inds;
mind_entry_universes;
- mind_entry_variance = mb.mind_variance;
+ mind_entry_cumulative= Option.has_some mb.mind_variance;
mind_entry_private = mb.mind_private;
}
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9d7387c7ad..261a3510d6 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -315,10 +315,6 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
let ctx = List.rev mip.mind_arity_ctxt in
mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
-let dummy_variance = let open Entries in function
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant
-
let cook_inductive { Opaqueproof.modlist; abstract } mib =
let open Entries in
let (section_decls, subst, abs_uctx) = abstract in
@@ -333,10 +329,6 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
let auctx = Univ.AUContext.repr auctx in
subst, Polymorphic_entry (nas, auctx)
in
- let variance = match mib.mind_variance with
- | None -> None
- | Some _ -> Some (dummy_variance ind_univs)
- in
let cache = RefTable.create 13 in
let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in
let inds =
@@ -363,7 +355,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
mind_entry_params = params';
mind_entry_inds = inds';
mind_entry_private = mib.mind_private;
- mind_entry_variance = variance;
+ mind_entry_cumulative = Option.has_some mib.mind_variance;
mind_entry_universes = ind_univs
}
diff --git a/kernel/entries.ml b/kernel/entries.ml
index b50c3ebbc3..8d930b521c 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
mind_entry_params : Constr.rel_context;
mind_entry_inds : one_inductive_entry list;
mind_entry_universes : universes_entry;
- mind_entry_variance : Univ.Variance.t array option;
+ mind_entry_cumulative : bool;
(* universe constraints and the constraints for subtyping of
inductive types in the block. *)
mind_entry_private : bool option;
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c91cb39fe2..982bc49927 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -61,64 +61,6 @@ let mind_check_names mie =
(************************************************************************)
-(************************** Cumulativity checking************************)
-(************************************************************************)
-
-(* Check arities and constructors *)
-let check_subtyping_arity_constructor env subst arcn numparams is_arity =
- let numchecked = ref 0 in
- let basic_check ev tp =
- if !numchecked < numparams then () else Reduction.conv_leq ev tp (subst tp);
- numchecked := !numchecked + 1
- in
- let check_typ typ typ_env =
- match typ with
- | LocalAssum (_, typ') ->
- begin
- try
- basic_check typ_env typ'; Environ.push_rel typ typ_env
- with Reduction.NotConvertible ->
- CErrors.anomaly ~label:"bad inductive subtyping relation"
- Pp.(str "Invalid subtyping relation")
- end
- | _ -> CErrors.anomaly Pp.(str "")
- in
- let typs, codom = Reduction.dest_prod env arcn in
- let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
- if not is_arity then basic_check last_env codom else ()
-
-let check_cumulativity univs variances env_ar params data =
- let uctx = match univs with
- | Monomorphic_entry _ -> raise (InductiveError BadUnivs)
- | Polymorphic_entry (_,uctx) -> uctx
- in
- let instance = UContext.instance uctx in
- if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs);
- let numparams = Context.Rel.nhyps params in
- let new_levels = Array.init (Instance.length instance)
- (fun i -> Level.(make (UGlobal.make DirPath.empty i)))
- in
- let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
- LMap.empty (Instance.to_array instance) new_levels
- in
- let dosubst = Vars.subst_univs_level_constr lmap in
- let instance_other = Instance.of_array new_levels in
- let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in
- let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
- let env = Environ.push_context uctx_other env_ar in
- let subtyp_constraints =
- Univ.enforce_leq_variance_instances variances
- instance instance_other
- Constraint.empty
- in
- let env = Environ.add_constraints subtyp_constraints env in
- (* process individual inductive types: *)
- List.iter (fun (arity,lc) ->
- check_subtyping_arity_constructor env dosubst arity numparams true;
- Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc)
- data
-
-(************************************************************************)
(************************** Type checking *******************************)
(************************************************************************)
@@ -389,11 +331,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
data, Some None
in
- let () = match mie.mind_entry_variance with
- | None -> ()
- | Some variances ->
- check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data)
- in
+ (* TODO pass only the needed bits *)
+ let variance = InferCumulativity.infer_inductive env mie in
(* Abstract universes *)
let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
@@ -408,4 +347,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
Environ.push_rel_context ctx env
in
- env_ar_par, univs, mie.mind_entry_variance, record, params, Array.of_list data
+ env_ar_par, univs, variance, record, params, Array.of_list data
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 550c81ed82..77abe6b410 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -216,19 +216,11 @@ let infer_inductive env mie =
let open Entries in
let params = mie.mind_entry_params in
let entries = mie.mind_entry_inds in
- let variances =
- match mie.mind_entry_variance with
- | None -> None
- | Some _ ->
- let uctx = match mie.mind_entry_universes with
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> uctx
- in
- try Some (infer_inductive_core env params entries uctx)
- with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
- in
- { mie with mind_entry_variance = variances }
-
-let dummy_variance = let open Entries in function
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant
+ if not mie.mind_entry_cumulative then None
+ else
+ let uctx = match mie.mind_entry_universes with
+ | Monomorphic_entry _ -> assert false
+ | Polymorphic_entry (_,uctx) -> uctx
+ in
+ try Some (infer_inductive_core env params entries uctx)
+ with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index a234e334d1..2bddfe21e2 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -9,6 +9,4 @@
(************************************************************************)
val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
- Entries.mutual_inductive_entry
-
-val dummy_variance : Entries.universes_entry -> Univ.Variance.t array
+ Univ.Variance.t array option
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 2b83c2d868..f1e994b337 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -42,9 +42,9 @@ Type_errors
Modops
Inductive
Typeops
+InferCumulativity
IndTyping
Indtypes
-InferCumulativity
Cooking
Term_typing
Subtyping
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 759feda9ab..d04f43f5bd 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1015,7 +1015,6 @@ let close_section senv =
| `Inductive (ind, mib) ->
let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
let mie = Cooking.cook_inductive info mib in
- let mie = InferCumulativity.infer_inductive senv.env mie in
let _, senv = add_mind (MutInd.label ind) mie senv in
senv
in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 56ff757e1a..5cf2b680ca 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -353,7 +353,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
Evd.restrict_universe_context sigma uvars
-let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
(* Compute renewed arities *)
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
@@ -403,7 +403,6 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~
})
indnames arities arityconcl constructors
in
- let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in
(* Build the mutual inductive entry *)
let mind_ent =
{ mind_entry_params = ctx_params;
@@ -412,12 +411,10 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~
mind_entry_inds = entries;
mind_entry_private = if private_ind then Some false else None;
mind_entry_universes = uctx;
- mind_entry_variance = variance;
+ mind_entry_cumulative = poly && cumulative;
}
in
- (if poly && cumulative then
- InferCumulativity.infer_inductive env_ar mind_ent
- else mind_ent), Evd.universe_binders sigma
+ mind_ent, Evd.universe_binders sigma
let interp_params env udecl uparamsl paramsl =
let sigma, udecl = interp_univ_decl_opt env udecl in
@@ -504,7 +501,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
indimpls, List.map (fun impls ->
userimpls @ impls) cimpls) indimpls constructors
in
- let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
+ let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
(mie, pl, impls)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 73d385dec8..418d971558 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -49,22 +49,22 @@ val declare_mutual_inductive_with_eliminations
-> Names.MutInd.t
[@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
-val interp_mutual_inductive_constr :
- sigma:Evd.evar_map ->
- template:bool option ->
- udecl:UState.universe_decl ->
- env_ar:Environ.env ->
- ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list ->
- indnames:Names.Id.t list ->
- arities:EConstr.t list ->
- arityconcl:(bool * EConstr.ESorts.t) option list ->
- constructors:(Names.Id.t list * Constr.constr list * 'a list list) list ->
- env_ar_params:Environ.env ->
- cumulative:bool ->
- poly:bool ->
- private_ind:bool ->
- finite:Declarations.recursivity_kind ->
- Entries.mutual_inductive_entry * UnivNames.universe_binders
+val interp_mutual_inductive_constr
+ : sigma:Evd.evar_map
+ -> template:bool option
+ -> udecl:UState.universe_decl
+ -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
+ -> indnames:Names.Id.t list
+ -> arities:EConstr.t list
+ -> arityconcl:(bool * EConstr.ESorts.t) option list
+ -> constructors:(Names.Id.t list * Constr.constr list * 'a list list) list
+ -> env_ar_params:Environ.env
+ (** Environment with the inductives and parameters in the rel_context *)
+ -> cumulative:bool
+ -> poly:bool
+ -> private_ind:bool
+ -> finite:Declarations.recursivity_kind
+ -> Entries.mutual_inductive_entry * UnivNames.universe_binders
(************************************************************************)
(** Internal API, exported for Record *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1ee6812f4e..ea10e06d02 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -411,7 +411,6 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
| Polymorphic_entry (nas, ctx) ->
true, Polymorphic_entry (nas, ctx)
in
- let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in
let binder_name =
match name with
| None ->
@@ -478,10 +477,9 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
mind_entry_inds = blocks;
mind_entry_private = None;
mind_entry_universes = univs;
- mind_entry_variance = variance;
+ mind_entry_cumulative = poly && cumulative;
}
in
- let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
let impls = List.map (fun _ -> paramimpls, []) record_data in
let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
~primitive_expected:!primitive_flag
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:25:46 +0000