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

3 files changed, 31 insertions, 2 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 235310660b..977cbbccf2 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -15,8 +15,11 @@ open Libnames
 
 (** [constr_expr] is the abstract syntax tree produced by the parser *)
 type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
+type cumul_univ_decl_expr =
+  ((lident * Univ.Variance.t option) list, Glob_term.glob_constraint list) UState.gen_universe_decl
 
 type ident_decl = lident * universe_decl_expr option
+type cumul_ident_decl = lident * cumul_univ_decl_expr option
 type name_decl = lname * universe_decl_expr option
 
 type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 02c3c047d5..0eb915561e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2648,13 +2648,34 @@ let interp_univ_decl env decl =
   let binders : lident list = decl.univdecl_instance in
   let evd = Evd.from_env ~binders env in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
-  let decl = { univdecl_instance = binders;
+  let decl = {
+    univdecl_instance = binders;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
     univdecl_constraints = cstrs;
-    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+  }
   in evd, decl
 
+let interp_cumul_univ_decl env decl =
+  let open UState in
+  let binders = List.map fst decl.univdecl_instance in
+  let variances = Array.map_of_list snd decl.univdecl_instance in
+  let evd = Evd.from_ctx (UState.from_env ~binders env) in
+  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+  let decl = {
+    univdecl_instance = binders;
+    univdecl_extensible_instance = decl.univdecl_extensible_instance;
+    univdecl_constraints = cstrs;
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+  }
+  in
+  evd, decl, variances
+
 let interp_univ_decl_opt env l =
   match l with
   | None -> Evd.from_env env, UState.default_univ_decl
   | Some decl -> interp_univ_decl env decl
+
+let interp_cumul_univ_decl_opt env = function
+  | None -> Evd.from_env env, UState.default_univ_decl, [| |]
+  | Some decl -> interp_cumul_univ_decl env decl
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9037ed5414..0de6c3e89d 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -204,3 +204,8 @@ val interp_univ_decl : Environ.env -> universe_decl_expr ->
 
 val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
                        Evd.evar_map * UState.universe_decl
+
+val interp_cumul_univ_decl_opt : Environ.env -> cumul_univ_decl_expr option ->
+  Evd.evar_map * UState.universe_decl * Entries.variance_entry
+(** BEWARE the variance entry needs to be adjusted by
+   [ComInductive.variance_of_entry] if the instance is extensible. *)