Merge PR #12653: Syntax for specifying cumulative inductives

Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot

8 files changed, 131 insertions, 29 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index bb26ce652e..597e55a39e 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,7 +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 interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+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,_) ->
+    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 ~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
@@ -429,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_cumulative = poly && cumulative;
+      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)) =
@@ -443,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.
@@ -485,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
 
@@ -563,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)
 
 
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 91e8f609d5..8bce884ba4 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -22,7 +22,7 @@ type uniform_inductive_flag =
 
 val do_mutual_inductive
   :  template:bool option
-  -> universe_decl_expr option
+  -> cumul_univ_decl_expr option
   -> (one_inductive_expr * decl_notation list) list
   -> cumulative:bool
   -> poly:bool
@@ -45,6 +45,7 @@ val interp_mutual_inductive_constr
   : sigma:Evd.evar_map
   -> template:bool option
   -> udecl:UState.universe_decl
+  -> variances:Entries.variance_entry
   -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
   -> indnames:Names.Id.t list
   -> arities:EConstr.t list
@@ -86,3 +87,13 @@ val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:
 (** [nparams] is the number of parameters which aren't treated as
     uniform, ie the length of params (including letins) where the env
     is [uniform params, inductives, params, binders]. *)
+
+val variance_of_entry
+  : cumulative:bool
+  -> variances:Entries.variance_entry
+  -> Entries.universes_entry
+  -> Entries.variance_entry option
+(** Will return None if non-cumulative, and resize if there are more
+    universes than originally specified.
+    If monomorphic, [cumulative] is treated as [false].
+*)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1c80d71ea5..1aff76114b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -194,6 +194,12 @@ let lname_of_lident : lident -> lname =
 let name_of_ident_decl : ident_decl -> name_decl =
   on_fst lname_of_lident
 
+let test_variance_ident =
+  let open Pcoq.Lookahead in
+  to_entry "test_variance_ident" begin
+    lk_kws ["=";"+";"*"] >> lk_ident
+  end
+
 }
 
 (* Gallina declarations *)
@@ -283,7 +289,7 @@ GRAMMAR EXTEND Gram
     [ [ l = universe_name; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
         r = universe_name -> { (l, ord, r) } ] ]
   ;
-  univ_decl :
+  univ_decl:
     [ [  "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
          cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
                 ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
@@ -296,10 +302,40 @@ GRAMMAR EXTEND Gram
            univdecl_extensible_constraints = snd cs } }
     ] ]
   ;
+  variance:
+    [ [ "+" -> { Univ.Variance.Covariant }
+      | "=" -> { Univ.Variance.Invariant }
+      | "*" -> { Univ.Variance.Irrelevant }
+    ] ]
+  ;
+  variance_identref:
+    [ [ id = identref -> { (id, None) }
+      | test_variance_ident; v = variance; id = identref -> { (id, Some v) }
+        (* We need this test to help the parser avoid the conflict
+           between "+" before ident (covariance) and trailing "+" (extra univs allowed) *)
+    ] ]
+  ;
+  cumul_univ_decl:
+    [ [  "@{" ; l = LIST0 variance_identref; ext = [ "+" -> { true } | -> { false } ];
+         cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
+                ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
+              | ext = [ "}" -> { true } | bar_cbrace -> { false } ] -> { ([], ext) } ]
+         ->
+         { let open UState in
+         { univdecl_instance = l;
+           univdecl_extensible_instance = ext;
+           univdecl_constraints = fst cs;
+           univdecl_extensible_constraints = snd cs } }
+    ] ]
+  ;
   ident_decl:
     [ [ i = identref; l = OPT univ_decl -> { (i, l) }
   ] ]
   ;
+  cumul_ident_decl:
+    [ [ i = identref; l = OPT cumul_univ_decl -> { (i, l) }
+  ] ]
+  ;
   finite_token:
     [ [ IDENT "Inductive" -> { Inductive_kw }
       | IDENT "CoInductive" -> { CoInductive }
@@ -345,7 +381,7 @@ GRAMMAR EXTEND Gram
       | -> { RecordDecl (None, []) } ] ]
   ;
   inductive_definition:
-    [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
+    [ [ oc = opt_coercion; id = cumul_ident_decl; indpar = binders;
         extrapar = OPT [ "|"; p = binders -> { p } ];
         c = OPT [ ":"; c = lconstr -> { c } ];
         lc=opt_constructors_or_fields; ntn = decl_notations ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index bef9e29ac2..9d86ea90e6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -744,6 +744,11 @@ let explain_bad_relevance env =
 let explain_bad_invert env =
   strbrk "Bad case inversion (maybe a bugged tactic)."
 
+let explain_bad_variance env sigma ~lev ~expected ~actual =
+  str "Incorrect variance for universe " ++ Termops.pr_evd_level sigma lev ++
+  str": expected " ++ Univ.Variance.pr expected ++
+  str " but cannot be less restrictive than " ++ Univ.Variance.pr actual ++ str "."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -788,6 +793,7 @@ let explain_type_error env sigma err =
   | DisallowedSProp -> explain_disallowed_sprop ()
   | BadRelevance -> explain_bad_relevance env
   | BadInvert -> explain_bad_invert env
+  | BadVariance {lev;expected;actual} -> explain_bad_variance env sigma ~lev ~expected ~actual
 
 let pr_position (cl,pos) =
   let clpos = match cl with
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0e660bf20c..442269ebda 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -68,10 +68,18 @@ let pr_univ_name_list = function
   | Some l ->
     str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
 
+let pr_variance_lident (lid,v) =
+  let v = Option.cata Univ.Variance.pr (mt()) v in
+  v ++ pr_lident lid
+
 let pr_univdecl_instance l extensible =
   prlist_with_sep spc pr_lident l ++
   (if extensible then str"+" else mt ())
 
+let pr_cumul_univdecl_instance l extensible =
+  prlist_with_sep spc pr_variance_lident l ++
+  (if extensible then str"+" else mt ())
+
 let pr_univdecl_constraints l extensible =
   if List.is_empty l && extensible then mt ()
   else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++
@@ -85,9 +93,20 @@ let pr_universe_decl l =
     str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
     pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
 
+let pr_cumul_univ_decl l =
+  let open UState in
+  match l with
+  | None -> mt ()
+  | Some l ->
+    str"@{" ++ pr_cumul_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
+    pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+
 let pr_ident_decl (lid, l) =
   pr_lident lid ++ pr_universe_decl l
 
+let pr_cumul_ident_decl (lid, l) =
+  pr_lident lid ++ pr_cumul_univ_decl l
+
 let string_of_fqid fqid =
   String.concat "." (List.map Id.to_string fqid)
 
@@ -848,7 +867,7 @@ let pr_vernac_expr v =
     let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) =
       hov 0 (
         str key ++ spc() ++
-        (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
+        (if coe then str"> " else str"") ++ pr_cumul_ident_decl iddecl ++
         pr_and_type_binders_arg indupar ++
         pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
         pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
diff --git a/vernac/record.ml b/vernac/record.ml
index 891d7fcebe..583164a524 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -190,11 +190,12 @@ type tc_result =
   (* Part relative to closing the definitions *)
   * UnivNames.universe_binders
   * Entries.universes_entry
+  * Entries.variance_entry
   * Constr.rel_context
   * DataR.t list
 
 (* ps = parameter list *)
-let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_result =
+let typecheck_params_and_fields def poly udecl ps (records : DataI.t list) : tc_result =
   let env0 = Global.env () in
   (* Special case elaboration for template-polymorphic inductives,
      lower bound on introduced universes is Prop so that we do not miss
@@ -202,7 +203,7 @@ let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_res
   let is_template =
     List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in
   let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
-  let sigma, decl = Constrintern.interp_univ_decl_opt env0 pl in
+  let sigma, decl, variances = Constrintern.interp_cumul_univ_decl_opt env0 udecl in
   let () = List.iter check_parameters_must_be_named ps in
   let sigma, (impls_env, ((env1,newps), imps)) =
     Constrintern.interp_context_evars ~program_mode:false env0 sigma ps in
@@ -256,7 +257,7 @@ let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_res
   let ubinders = Evd.universe_binders sigma in
   let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
   let () = List.iter (iter_constr ce) (List.rev newps) in
-  template, imps, ubinders, univs, newps, ans
+  template, imps, ubinders, univs, variances, newps, ans
 
 type record_error =
   | MissingProj of Id.t * Id.t list
@@ -525,7 +526,7 @@ let declare_structure_entry o =
   - prepares and declares the corresponding record projections, mainly taken care of by
     [declare_projections]
 *)
-let declare_structure ~cumulative finite ~ubind ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
+let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
   let nparams = List.length params in
   let poly, ctx =
     match univs with
@@ -568,7 +569,7 @@ let declare_structure ~cumulative finite ~ubind ~univs paramimpls params templat
       mind_entry_private = None;
       mind_entry_universes = univs;
       mind_entry_template = template;
-      mind_entry_cumulative = poly && cumulative;
+      mind_entry_variance = ComInductive.variance_of_entry ~cumulative ~variances univs;
     }
   in
   let impls = List.map (fun _ -> paramimpls, []) record_data in
@@ -633,7 +634,8 @@ let build_class_constant ~univs ~rdata field implfs params paramimpls coers bind
   } in
   [cref, [m]]
 
-let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name =
+let build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
+    fields params paramimpls coers id idbuild binder_name =
   let record_data =
     { Data.id
     ; idbuild
@@ -641,7 +643,7 @@ let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields para
     ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields
     ; rdata
     } in
-  let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs paramimpls
+  let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs ~variances paramimpls
       params template ~kind:Decls.Method ~name:[|binder_name|] [record_data]
   in
   let map ind =
@@ -677,7 +679,7 @@ let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields para
   2. declare the class, using the information from 1. in the form of [Classes.typeclass]
 
   *)
-let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params
+let declare_class def ~cumulative ~ubind ~univs ~variances id idbuild paramimpls params
     rdata template ?(kind=Decls.StructureComponent) coers =
   let implfs =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -694,7 +696,8 @@ let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params
       let binder = {binder with binder_name=Name binder_name} in
       build_class_constant ~rdata ~univs field implfs params paramimpls coers binder id proj_name
     | _ ->
-      build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name
+      build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
+        fields params paramimpls coers id idbuild binder_name
   in
   let univs, params, fields =
     match univs with
@@ -852,7 +855,8 @@ let class_struture ~cumulative ~template ~ubind ~impargs ~univs ~params def reco
   declare_class def ~cumulative ~ubind ~univs name.CAst.v idbuild
     impargs params rdata template coers
 
-let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data =
+let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~params ~finite
+    records data =
   let adjust_impls impls = impargs @ [CAst.make None] @ impls in
   let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in
   (* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *)
@@ -866,30 +870,36 @@ let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~fini
     { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers }
   in
   let data = List.map2 map data records in
-  let inds = declare_structure ~cumulative finite ~ubind ~univs impargs params template data in
+  let inds = declare_structure ~cumulative finite ~ubind ~univs ~variances
+      impargs params template data
+  in
   List.map (fun ind -> GlobRef.IndRef ind) inds
 
 (** [fs] corresponds to fields and [ps] to parameters; [coers] is a
     list telling if the corresponding fields must me declared as coercions
     or subinstances. *)
-let definition_structure udecl kind ~template ~cumulative ~poly finite (records : Ast.t list) =
+let definition_structure udecl kind ~template ~cumulative ~poly
+    finite (records : Ast.t list) : GlobRef.t list =
   let () = check_unique_names records in
   let () = check_priorities kind records in
   let ps, data = extract_record_data records in
-  let auto_template, impargs, ubind, univs, params, data =
+  let auto_template, impargs, ubind, univs, variances, params, data =
     (* In theory we should be able to use
        [Notation.with_notation_protection], due to the call to
        Metasyntax.set_notation_for_interpretation, however something
        is messing state beyond that.
     *)
     Vernacstate.System.protect (fun () ->
-      typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in
+        typecheck_params_and_fields (kind = Class true) poly udecl ps data) ()
+  in
   let template = template, auto_template in
   match kind with
   | Class def ->
-    class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs def records data
+    class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs ~variances
+      def records data
   | Inductive_kw | CoInductive | Variant | Record | Structure ->
-    regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data
+    regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~params ~finite
+      records data
 
 module Internal = struct
   type nonrec projection_flags = projection_flags = {
diff --git a/vernac/record.mli b/vernac/record.mli
index ffcae2975e..7a40af048c 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -24,7 +24,7 @@ module Ast : sig
 end
 
 val definition_structure
-  :  universe_decl_expr option
+  :  cumul_univ_decl_expr option
   -> inductive_kind
   -> template:bool option
   -> cumulative:bool
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 6a9a74144f..defb0691c0 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -189,8 +189,9 @@ type inductive_params_expr = local_binder_expr list * local_binder_expr list opt
 (** If the option is nonempty the "|" marker was used *)
 
 type inductive_expr =
-  ident_decl with_coercion * inductive_params_expr * constr_expr option *
-    constructor_list_or_record_decl_expr
+  cumul_ident_decl with_coercion
+  * inductive_params_expr * constr_expr option
+  * constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
   lident * inductive_params_expr * constr_expr option * constructor_expr list