Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

4 files changed, 34 insertions, 35 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index aa30ed8d2e..bb163ddaee 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -468,17 +468,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
           let mind = Environ.lookup_mind mi env in
           let open Declarations in
-          begin match mind.mind_universes with
-            | Monomorphic_ind _ -> assert false
-            | Polymorphic_ind _ -> check_strict evd u u'
-            | Cumulative_ind cumi ->
+          begin match mind.mind_variance with
+            | None -> check_strict evd u u'
+            | Some variances ->
               let nparamsaplied = Stack.args_size sk in
               let nparamsaplied' = Stack.args_size sk' in
               let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
               if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
               then check_strict evd u u'
               else
-                compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u'
+                compare_cumulative_instances evd variances u u'
           end
       | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
       | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
@@ -488,10 +487,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
           let mind = Environ.lookup_mind mi env in
           let open Declarations in
-          begin match mind.mind_universes with
-            | Monomorphic_ind _ -> assert false
-            | Polymorphic_ind _ -> check_strict evd u u'
-            | Cumulative_ind cumi ->
+          begin match mind.mind_variance with
+            | None -> check_strict evd u u'
+            | Some variances ->
               let nparamsaplied = Stack.args_size sk in
               let nparamsaplied' = Stack.args_size sk' in
               let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ff552c7caf..2c4ca46343 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -453,12 +453,7 @@ let build_branch_type env sigma dep p cs =
 let compute_projections env (kn, i as ind) =
   let open Term in
   let mib = Environ.lookup_mind kn env in
-  let u = match mib.mind_universes with
-  | Monomorphic_ind _ -> Instance.empty
-  | Polymorphic_ind auctx -> make_abstract_instance auctx
-  | Cumulative_ind acumi ->
-    make_abstract_instance (ACumulativityInfo.univ_context acumi)
-  in
+  let u = make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
   let x = match mib.mind_record with
   | NotRecord | FakeRecord ->
     anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index b5a6ba6be5..bf8a38a353 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -41,33 +41,31 @@ let variance_pb cv_pb var =
   | CONV, Covariant -> Invariant
   | CUMUL, Covariant -> Covariant
 
-let infer_cumulative_ind_instance cv_pb cumi variances u =
+let infer_cumulative_ind_instance cv_pb mind_variance variances u =
   Array.fold_left2 (fun variances varu u ->
       match LMap.find u variances with
       | exception Not_found -> variances
       | varu' ->
         LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
-    variances (ACumulativityInfo.variance cumi) (Instance.to_array u)
+    variances mind_variance (Instance.to_array u)
 
 let infer_inductive_instance cv_pb env variances ind nargs u =
   let mind = Environ.lookup_mind (fst ind) env in
-  match mind.mind_universes with
-  | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
-  | Polymorphic_ind _ -> infer_generic_instance_eq variances u
-  | Cumulative_ind cumi ->
+  match mind.mind_variance with
+  | None -> infer_generic_instance_eq variances u
+  | Some mind_variance ->
     if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
     then infer_generic_instance_eq variances u
-    else infer_cumulative_ind_instance cv_pb cumi variances u
+    else infer_cumulative_ind_instance cv_pb mind_variance variances u
 
 let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
   let mind = Environ.lookup_mind mi env in
-  match mind.mind_universes with
-  | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
-  | Polymorphic_ind _ -> infer_generic_instance_eq variances u
-  | Cumulative_ind cumi ->
+  match mind.mind_variance with
+  | None -> infer_generic_instance_eq variances u
+  | Some _ ->
     if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
     then infer_generic_instance_eq variances u
-    else infer_cumulative_ind_instance CONV cumi variances u
+    else variances (* constructors are convertible at common supertype *)
 
 let infer_sort cv_pb variances s =
   match cv_pb with
@@ -189,12 +187,14 @@ let infer_inductive env mie =
   let { mind_entry_params = params;
         mind_entry_inds = entries; } = mie
   in
-  let univs =
-    match mie.mind_entry_universes with
-    | Monomorphic_ind_entry _
-    | Polymorphic_ind_entry _ as univs -> univs
-    | Cumulative_ind_entry (nas, cumi) ->
-      let uctx = CumulativityInfo.univ_context cumi 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
       let uarray = Instance.to_array @@ UContext.instance uctx in
       let env = Environ.push_context uctx env in
       let variances =
@@ -212,6 +212,10 @@ let infer_inductive env mie =
           entries
       in
       let variances = Array.map (fun u -> LMap.find u variances) uarray in
-      Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances))
+      Some variances
   in
-  { mie with mind_entry_universes = univs }
+  { 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) Variance.Irrelevant
diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli
index a0c8d339ac..6e5bf30f6b 100644
--- a/pretyping/inferCumulativity.mli
+++ b/pretyping/inferCumulativity.mli
@@ -10,3 +10,5 @@
 
 val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
   Entries.mutual_inductive_entry
+
+val dummy_variance : Entries.universes_entry -> Univ.Variance.t array