inferCumulativity: shortcut for all-Invariant inductives

pretyping/inferCumulativity.ml

@@ -12,41 +12,44 @@ open Reduction
 open Declarations
 open Constr
 open Univ
+open Variance
 open Util
 
+type inferred = IrrelevantI | CovariantI
+
 (** Throughout this module we modify a map [variances] from local
-   universes to [Variance.t]. It starts as a trivial mapping to
-   [Irrelevant] and every time we encounter a local universe we
-   restrict it accordingly. *)
+    universes to [inferred]. It starts as a trivial mapping to
+    [Irrelevant] and every time we encounter a local universe we
+    restrict it accordingly.
+    [Invariant] universes are removed from the map.
+*)
+exception TrivialVariance
+
+let maybe_trivial variances =
+  if LMap.is_empty variances then raise TrivialVariance
+  else variances
 
 let infer_level_eq u variances =
-  if LMap.mem u variances
-  then LMap.set u Variance.Invariant variances
-  else variances
+  maybe_trivial (LMap.remove u variances)
 
 let infer_level_leq u variances =
-  match LMap.find u variances with
-  | exception Not_found -> variances
-  | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances
+  (* can only set Irrelevant -> Covariant so nontrivial *)
+  LMap.update u (function
+      | None -> None
+      | Some CovariantI as x -> x
+      | Some IrrelevantI -> Some CovariantI)
+    variances
 
 let infer_generic_instance_eq variances u =
   Array.fold_left (fun variances u -> infer_level_eq u variances)
     variances (Instance.to_array u)
 
-let variance_pb cv_pb var =
-  let open Variance in
-  match cv_pb, var with
-  | _, Irrelevant -> Irrelevant
-  | _, Invariant -> Invariant
-  | CONV, Covariant -> Invariant
-  | CUMUL, Covariant -> Covariant
-
 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)
+      match cv_pb, varu with
+      | _, Irrelevant -> variances
+      | _, Invariant | CONV, Covariant -> infer_level_eq u variances
+      | CUMUL, Covariant -> infer_level_leq u variances)
     variances mind_variance (Instance.to_array u)
 
 let infer_inductive_instance cv_pb env variances ind nargs u =
@@ -182,6 +185,32 @@ let infer_arity_constructor is_arity env variances arcn =
      i is irrelevant, j is invariant. *)
   if not is_arity then infer_term CUMUL env variances codom else variances
 
+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 variances =
+    Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
+      LMap.empty uarray
+  in
+  let env, params = 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
+      in
+      List.fold_left (infer_arity_constructor false env)
+        variances entry.mind_entry_lc)
+      variances
+      entries
+  in
+  Array.map (fun u -> match LMap.find u variances with
+      | exception Not_found -> Invariant
+      | IrrelevantI -> Irrelevant
+      | CovariantI -> Covariant)
+    uarray
+
 let infer_inductive env mie =
   let open Entries in
   let { mind_entry_params = params;
@@ -195,27 +224,11 @@ let infer_inductive env mie =
         | 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 =
-        Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
-          LMap.empty uarray
-      in
-      let env, params = 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
-          in
-          List.fold_left (infer_arity_constructor false env)
-            variances entry.mind_entry_lc)
-          variances
-          entries
-      in
-      let variances = Array.map (fun u -> LMap.find u variances) uarray in
-      Some variances
+      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) Variance.Irrelevant
+  | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant