Merge PR #11027: Cleanup post #10647 (expose comind universe handling)

Reviewed-by: ppedrot

7 files changed, 15 insertions, 95 deletions

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