infercumulativity: take less arguments

3 files changed, 27 insertions, 24 deletions

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index b19472dc99..3f2f9f4fc0 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -335,8 +335,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
         data, Some None
   in
 
-  (* TODO pass only the needed bits *)
-  let variance = InferCumulativity.infer_inductive env mie in
+  let variance = if not mie.mind_entry_cumulative then None
+    else match mie.mind_entry_universes with
+      | Monomorphic_entry _ ->
+        CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.")
+      | Polymorphic_entry (_,uctx) ->
+        let univs = Instance.to_array @@ UContext.instance uctx in
+        Some (InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds)
+  in
 
   (* Abstract universes *)
   let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 77abe6b410..211c909241 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -188,15 +188,12 @@ let infer_arity_constructor is_arity env variances arcn =
 
 open Entries
 
-let infer_inductive_core env params entries uctx =
-  let uarray = Instance.to_array @@ UContext.instance uctx in
-  if Array.is_empty uarray then raise TrivialVariance;
-  let env = Environ.push_context uctx env in
+let infer_inductive_core env univs entries =
+  if Array.is_empty univs then raise TrivialVariance;
   let variances =
     Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
-      LMap.empty uarray
+      LMap.empty univs
   in
-  let env, _ = Typeops.check_context env params in
   let variances = List.fold_left (fun variances entry ->
       let variances = infer_arity_constructor true
           env variances entry.mind_entry_arity
@@ -210,17 +207,8 @@ let infer_inductive_core env params entries uctx =
       | exception Not_found -> Invariant
       | IrrelevantI -> Irrelevant
       | CovariantI -> Covariant)
-    uarray
-
-let infer_inductive env mie =
-  let open Entries in
-  let params = mie.mind_entry_params in
-  let entries = mie.mind_entry_inds in
-  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)
+    univs
+
+let infer_inductive ~env_params univs entries =
+  try infer_inductive_core env_params univs entries
+  with TrivialVariance -> Array.make (Array.length univs) Invariant
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index 2bddfe21e2..a8f593c7f9 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -8,5 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
-  Univ.Variance.t array option
+val infer_inductive
+  : env_params:Environ.env
+  (** Environment containing the polymorphic universes and the
+     parameters. *)
+  -> Univ.Level.t array
+  (** Universes whose cumulativity we want to infer. *)
+  -> Entries.one_inductive_entry list
+  (** The inductive block data we want to infer cumulativity for.
+      NB: we ignore the template bool and the names, only the terms
+      are used. *)
+  -> Univ.Variance.t array