Syntax for specifying cumulative inductives

1 files changed, 23 insertions, 10 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 6b37958ab3..597e55a39e 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,13 +367,26 @@ 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 variance_of_entry ~cumulative = function
-  | Monomorphic_entry _ -> None
+let check_trivial_variances variances =
+  Array.iter (function
+      | None | Some Univ.Variance.Invariant -> ()
+      | Some _ ->
+        CErrors.user_err
+          Pp.(strbrk "Universe variance was specified but this inductive will not be cumulative."))
+    variances
+
+let variance_of_entry ~cumulative ~variances uctx =
+  match uctx with
+  | Monomorphic_entry _ -> check_trivial_variances variances; None
   | Polymorphic_entry (nas,_) ->
-    Some (Array.map (fun _ -> None) nas)
-(* TODO syntax to have non-None elements *)
+    if not cumulative then begin check_trivial_variances variances; None end
+    else
+      let lvs = Array.length variances in
+      let lus = Array.length nas in
+      assert (lvs <= lus);
+      Some (Array.append variances (Array.make (lus - lvs) None))
 
-let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+let interp_mutual_inductive_constr ~sigma ~template ~udecl ~variances ~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
@@ -435,13 +448,13 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = uctx;
       mind_entry_template = is_template;
-      mind_entry_variance = variance_of_entry ~cumulative uctx;
+      mind_entry_variance = variance_of_entry ~cumulative ~variances uctx;
     }
   in
   mind_ent, Evd.universe_binders sigma
 
 let interp_params env udecl uparamsl paramsl =
-  let sigma, udecl = interp_univ_decl_opt env udecl in
+  let sigma, udecl, variances = interp_cumul_univ_decl_opt env udecl in
   let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
     interp_context_evars ~program_mode:false env sigma uparamsl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
@@ -449,7 +462,7 @@ let interp_params env udecl uparamsl paramsl =
   in
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
-  userimpls, useruimpls, impls, udecl)
+  userimpls, useruimpls, impls, udecl, variances)
 
 (* When a hole remains for a param, pretend the param is uniform and
    do the unification.
@@ -491,7 +504,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   (* In case of template polymorphism, we need to compute more constraints *)
   let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
 
-  let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl) =
+  let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl, variances) =
     interp_params env0 udecl uparamsl paramsl
   in
 
@@ -569,7 +582,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
             userimpls @ impls) cimpls)
       indimpls cimpls
   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
+  let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~variances ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
   (mie, pl, impls)