Introduce PolyFlags to gather flags for polymorphic defs

dev/ci/user-overlays/21419-mattam82-sort-poly-flags.sh

@@ -0,0 +1,11 @@
+overlay equations https://github.com/mattam82/Coq-Equations sort-poly-flags 21419
+overlay rewriter https://github.com/mattam82/rewriter sort-poly-flags 21419
+overlay smtcoq https://github.com/mattam82/smtcoq sort-poly-flags 21419
+overlay mtac2 https://github.com/mattam82/Mtac2 sort-poly-flags 21419
+overlay elpi https://github.com/mattam82/coq-elpi sort-poly-flags 21419
+overlay simple_io https://github.com/mattam82/coq-simple-io sort-poly-flags 21419
+overlay paramcoq https://github.com/mattam82/paramcoq sort-poly-flags 21419
+overlay waterproof https://github.com/mattam82/coq-waterproof sort-poly-flags 21419
+overlay itauto https://gitlab.inria.fr/sozeau/itauto sort-poly-flags 21419
+overlay metarocq https://github.com/mattam82/metacoq sort-poly-flags 21419
+overlay quickchick https://github.com/mattam82/quickchick sort-poly-flags 21419

dev/top_printers.dbg

@@ -82,6 +82,7 @@ install_printer Top_printers.ppuniverse_context_set
 install_printer Top_printers.ppuniverse_subst
 install_printer Top_printers.ppuniverse_opt_subst
 install_printer Top_printers.ppqvar_subst
+install_printer Top_printers.pppoly_flags
 install_printer Top_printers.ppuniverse_level_subst
 install_printer Top_printers.ppustate
 install_printer Top_printers.ppconstraints

dev/top_printers.ml

@@ -299,6 +299,7 @@ let ppuniverse_subst l = pp (UnivSubst.pr_universe_subst Level.raw_pr l)
 let ppuniverse_opt_subst l = pp (UnivFlex.pr Level.raw_pr l)
 let ppqvar_subst l = pp (UVars.pr_quality_level_subst QVar.raw_pr l)
 let ppuniverse_level_subst l = pp (UVars.pr_universe_level_subst Level.raw_pr l)
+let pppoly_flags f = pp (PolyFlags.pr f)
 let ppustate l = pp (UState.pr l)
 let ppconstraints c = pp (UnivConstraints.pr Level.raw_pr c)
 let ppqconstraints c = pp (ElimConstraints.pr prqvar c)

dev/top_printers.mli

@@ -162,6 +162,7 @@ val ppaucontext : UVars.AbstractContext.t -> unit
 val ppuniverse_context_set : PConstraints.ContextSet.t -> unit
 val ppuniverse_subst : UnivSubst.universe_subst -> unit
 val ppuniverse_opt_subst : UState.universe_opt_subst -> unit
+val pppoly_flags : PolyFlags.t -> unit
 val ppqvar_subst : Sorts.Quality.t Sorts.QVar.Map.t -> unit
 val ppuniverse_level_subst : UVars.universe_level_subst -> unit
 val ppustate : UState.t -> unit

doc/changelog/08-vernac-commands-and-options/21419-sort-poly-flags-Changed.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  Generalized universe polymorphism flag structure (ML API change)
+  (`#21419 <https://github.com/rocq-prover/rocq/pull/21419>`_,
+  by Matthieu Sozeau).

doc/plugin_tutorial/tuto1/src/g_tuto1.mlg

@@ -136,8 +136,8 @@ END
  * then we call another function. We define this function in
  * the Simple_declare module.
  *
- * The line #[ poly = Attributes.polymorphic ] says that this command accepts
- * polymorphic attributes.
+ * The line #[ poly = Attributes.poly_def ] says that this command accepts
+ * universe polymorphism attributes for definitions.
  * @SkySkimmer: Here, poly is what the result is bound to in the
  * rule's code. Multiple attributes may be used separated by ;, and we have
  * punning so foo is equivalent to foo = foo.
@@ -151,7 +151,7 @@ END
  * as a side-effect (CLASSIFIED AS SIDEFF).
  *)
 VERNAC COMMAND EXTEND MyDefine CLASSIFIED AS SIDEFF
-| #[ poly = Attributes.polymorphic ] [ "MyDefine" ident(i) ":=" constr(e) ] ->
+| #[ poly = Attributes.poly_def ] [ "MyDefine" ident(i) ":=" constr(e) ] ->
    {
      let env = Global.env () in
      let sigma = Evd.from_env env in
@@ -205,7 +205,7 @@ END
  * [![opaque_access]] is equivalent to [STATE opaque_access] but is specific to that parsing rule.
  *)
 VERNAC COMMAND EXTEND DefineLookup CLASSIFIED AS SIDEFF
-| #[ poly = Attributes.polymorphic ] ![opaque_access] [ "DefineLookup" ident(i) ":=" constr(e) ] ->
+| #[ poly = Attributes.poly_def ] ![opaque_access] [ "DefineLookup" ident(i) ":=" constr(e) ] ->
    { fun ~opaque_access ->
      let env = Global.env () in
      let sigma = Evd.from_env env in

doc/plugin_tutorial/tuto1/src/simple_declare.mli

@@ -1,4 +1,4 @@
 open Names
 
 val declare_definition :
-    poly:bool -> Id.t -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t
+  poly:PolyFlags.t -> Id.t -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t

engine/evd.ml

@@ -1023,7 +1023,7 @@ let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes
 
 let check_univ_decl_early ~poly ~with_obls sigma udecl terms =
   let () =
-    if with_obls && not poly &&
+    if with_obls && not @@ PolyFlags.univ_poly poly &&
        (not udecl.UState.univdecl_extensible_instance
         || not udecl.UState.univdecl_extensible_constraints)
     then

engine/evd.mli

@@ -625,13 +625,13 @@ val universes : evar_map -> UGraph.t
     [PConstraints.ContextSet.to_context]. *)
 val to_universe_context : evar_map -> UVars.UContext.t
 
-val univ_entry : poly:bool -> evar_map -> UState.named_universes_entry
+val univ_entry : poly:PolyFlags.t -> evar_map -> UState.named_universes_entry
 
-val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> UState.named_universes_entry
+val check_univ_decl : poly:PolyFlags.t -> evar_map -> UState.universe_decl -> UState.named_universes_entry
 
 (** An early check of compatibility of the universe declaration before
     starting to build a declaration interactively *)
-val check_univ_decl_early : poly:bool -> with_obls:bool -> evar_map -> UState.universe_decl -> Constr.t list -> unit
+val check_univ_decl_early : poly:PolyFlags.t -> with_obls:bool -> evar_map -> UState.universe_decl -> Constr.t list -> unit
 
 val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map

engine/polyFlags.ml

@@ -0,0 +1,40 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type t = {
+  univ_poly : bool;
+  collapse_sort_variables : bool;
+  cumulative : bool;
+}
+
+let make ~univ_poly ~collapse_sort_variables ~cumulative =
+  if cumulative && not univ_poly then
+    CErrors.user_err Pp.(str "Cannot have cumulative but not universe polymorphic constructions");
+  if not collapse_sort_variables && not univ_poly then
+    CErrors.user_err Pp.(str "Sort metavariables must be collapsed to Type in universe monomorphic constructions");
+  { collapse_sort_variables; univ_poly; cumulative }
+
+let default = { collapse_sort_variables = true; univ_poly = false; cumulative = false }
+let of_univ_poly b = { default with univ_poly = b }
+
+let collapse_sort_variables x = x.collapse_sort_variables
+let univ_poly x = x.univ_poly
+let cumulative x = x.cumulative
+
+let pr f =
+  let open Pp in
+  str "{ univ_poly = " ++ bool f.univ_poly ++ spc () ++
+  str "; cumulative = " ++ bool f.cumulative ++ spc () ++
+  str "; collapse_sort_variables = " ++ bool f.collapse_sort_variables ++ spc () ++
+  str "}"
+
+(* Used to have distinguished default behaviors when treating assumptions/axioms, definitions or inductives *)
+type construction_kind =
+  Assumption | Definition | Inductive

engine/polyFlags.mli

@@ -0,0 +1,42 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type t
+(** Set of flags for universe polymorphism, implicit sort polymorphism and cumulativity.
+    Note that implicit sort polymorphism (not collapsing sort variables to Type) and
+    cumulativity only make sense for constructions that are already polymorphic.
+    This invariant is ensured by the smart constructor below.
+ *)
+
+(** Raises a user error if [univ_poly = false] and either [collapse_sort_variables = false] or [cumulative = true]. *)
+val make : univ_poly:bool -> collapse_sort_variables:bool -> cumulative:bool -> t
+
+(** The [default] is monomorphic:
+    [univ_poly] and [cumulative] are [false], [collapse_sort_variables] is [true] *)
+val default : t
+
+(** Only sets the universe [univ_poly] flag.
+    Use with care, this probably indicates that the code does not handle
+    [cumulative] constructions when it should. Code relying on elaboration should
+    also support the [collapse_sort_variables] flag. *)
+val of_univ_poly : bool -> t
+
+(** Accessors *)
+val univ_poly : t -> bool
+val collapse_sort_variables : t -> bool
+val cumulative : t -> bool
+
+(** Pretty print *)
+val pr : t -> Pp.t
+
+(** Used to have distinguished default behaviors when treating assumptions/axioms,
+    definitions or inductives *)
+type construction_kind =
+  Assumption | Definition | Inductive

engine/proofview.mli

@@ -157,7 +157,7 @@ type +'a tactic
     {!Logic_monad.TacticFailure}*)
 val apply
   :  name:Names.Id.t
-  -> poly:bool
+  -> poly:PolyFlags.t
   -> Environ.env
   -> 'a tactic
   -> proofview
@@ -449,7 +449,7 @@ val tclTIMEOUT  : int   -> 'a tactic -> 'a tactic
 val tclTIME : string option -> 'a tactic -> 'a tactic
 
 (** Internal, don't use. *)
-val tclProofInfo : (Names.Id.t * bool) tactic
+val tclProofInfo : (Names.Id.t * PolyFlags.t) tactic
 [@@ocaml.deprecated "(8.10) internal, don't use"]
 
 (** {7 Unsafe primitives} *)

engine/proofview_monad.ml

@@ -176,7 +176,7 @@ module P = struct
   type s = proofview * Environ.env
 
   (** Recording info trace (true) or not. *)
-  type e = { trace: bool; name : Names.Id.t; poly : bool }
+  type e = { trace: bool; name : Names.Id.t; poly : PolyFlags.t }
 
   (** Status (safe/unsafe) * shelved goals * given up *)
   type w = bool

engine/proofview_monad.mli

@@ -97,7 +97,7 @@ module P : sig
   val wprod : w -> w -> w
 
   (** Recording info trace (true) or not. *)
-  type e = { trace: bool; name : Names.Id.t; poly : bool }
+  type e = { trace: bool; name : Names.Id.t; poly : PolyFlags.t }
 
   type u = Info.state
 

engine/uState.ml

@@ -481,7 +481,7 @@ let check_mono_sort_constraints uctx =
 let univ_entry ~poly uctx =
   let (binders, _) = uctx.names in
   let entry =
-    if poly then Polymorphic_entry (context uctx)
+    if PolyFlags.univ_poly poly then Polymorphic_entry (context uctx)
     else
       let uctx = check_mono_sort_constraints uctx in
       Monomorphic_entry uctx
@@ -1153,7 +1153,7 @@ let check_poly_univ_decl uctx decl =
 let check_univ_decl ~poly uctx decl =
   let (binders, _) = uctx.names in
   let entry =
-    if poly then Polymorphic_entry (check_poly_univ_decl uctx decl)
+    if PolyFlags.univ_poly poly then Polymorphic_entry (check_poly_univ_decl uctx decl)
     else Monomorphic_entry (check_mono_univ_decl uctx decl)
   in
   entry, binders

engine/uState.mli

@@ -89,7 +89,7 @@ val context : t -> UVars.UContext.t
 
 type named_universes_entry = universes_entry * UnivNames.universe_binders
 
-val univ_entry : poly:bool -> t -> named_universes_entry
+val univ_entry : poly:PolyFlags.t -> t -> named_universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
 val universe_binders : t -> UnivNames.universe_binders
@@ -261,7 +261,7 @@ val default_univ_decl : universe_decl
    When polymorphic, the universes corresponding to
    [decl.univdecl_instance] come first in the order defined by that
    list. *)
-val check_univ_decl : poly:bool -> t -> universe_decl -> named_universes_entry
+val check_univ_decl : poly:PolyFlags.t -> t -> universe_decl -> named_universes_entry
 val check_univ_decl_rev : t -> universe_decl -> t * UVars.UContext.t
 val check_uctx_impl : fail:(Pp.t -> unit) -> t -> t -> unit
 

interp/constrintern.ml

@@ -2925,12 +2925,12 @@ let interp_constr_evars_gen_impls ?(flags=Pretyping.all_no_fail_flags) env sigma
   let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
   sigma, (c, imps)
 
-let interp_constr_evars_impls ?(program_mode=false) env sigma ?(impls=empty_internalization_env) c =
-  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+let interp_constr_evars_impls ?(program_mode=false) ?(poly = PolyFlags.default) env sigma ?(impls=empty_internalization_env) c =
+  let flags = { Pretyping.all_no_fail_flags with program_mode ; poly } in
   interp_constr_evars_gen_impls ~flags env sigma ~impls WithoutTypeConstraint c
 
-let interp_casted_constr_evars_impls ?(program_mode=false) env evdref ?(impls=empty_internalization_env) c typ =
-  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+let interp_casted_constr_evars_impls ?(program_mode=false) ?(poly = PolyFlags.default) env evdref ?(impls=empty_internalization_env) c typ =
+  let flags = { Pretyping.all_no_fail_flags with program_mode ; poly } in
   interp_constr_evars_gen_impls ~flags env evdref ~impls (OfType typ) c
 
 let interp_type_evars_impls ?(flags=Pretyping.all_no_fail_flags) env sigma ?(impls=empty_internalization_env) c =
@@ -3056,14 +3056,14 @@ let push_auto_implicit env sigma t int_env id =
   let imps = compute_internalization_data env sigma ~silent:false id var_info.var_intern_typ t imps in (* add automatic implicit arguments to manual ones *)
   { int_env with impls = Id.Map.add id imps int_env.impls }
 
-let interp_context_evars_gen ?(program_mode=false) ?(unconstrained_sorts = false) ?(impl_env=empty_internalization_env) ?(autoimp_enable=true) ~dump env sigma make_decl push_decl bl =
+let interp_context_evars_gen ?(program_mode=false) ?(unconstrained_sorts = false) ?(poly = PolyFlags.default) ?(impl_env=empty_internalization_env) ?(autoimp_enable=true) ~dump env sigma make_decl push_decl bl =
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let ids =
     (* We assume all ids around are parts of the prefix of the current
        context being interpreted *)
      extract_ids env in
   let int_env = default_internalization_env ids (bound_univs sigma) impl_env in
-  let flags = { Pretyping.all_no_fail_flags with program_mode; unconstrained_sorts } in
+  let flags = { Pretyping.all_no_fail_flags with program_mode; unconstrained_sorts; poly } in
   let (int_env, (env, sigma, bl, impls, locs)) =
     List.fold_left
       (fun (int_env, acc) b ->
@@ -3094,13 +3094,13 @@ let interp_context_evars_gen ?(program_mode=false) ?(unconstrained_sorts = false
   in
   sigma, (int_env.impls, ((env, bl), List.rev impls, locs))
 
-let interp_named_context_evars ?program_mode ?unconstrained_sorts ?impl_env ?autoimp_enable env sigma bl =
+let interp_named_context_evars ?program_mode ?unconstrained_sorts ?poly ?impl_env ?autoimp_enable env sigma bl =
   let extract_name ?loc = function Name id -> id | Anonymous -> user_err ?loc Pp.(str "Unexpected anonymous variable.") in
   let make_decl ?loc = Context.Named.Declaration.of_rel_decl (extract_name ?loc) in
-  interp_context_evars_gen ?program_mode ?unconstrained_sorts  ?impl_env ?autoimp_enable ~dump:false env sigma make_decl EConstr.push_named bl
+  interp_context_evars_gen ?program_mode ?unconstrained_sorts ?poly ?impl_env ?autoimp_enable ~dump:false env sigma make_decl EConstr.push_named bl
 
-let interp_context_evars ?program_mode ?unconstrained_sorts ?impl_env env sigma bl =
-  interp_context_evars_gen ?program_mode ?unconstrained_sorts ?impl_env ~autoimp_enable:false ~dump:true env sigma (fun ?loc d -> d) EConstr.push_rel bl
+let interp_context_evars ?program_mode ?unconstrained_sorts ?poly ?impl_env env sigma bl =
+  interp_context_evars_gen ?program_mode ?unconstrained_sorts ?poly ?impl_env ~autoimp_enable:false ~dump:true env sigma (fun ?loc d -> d) EConstr.push_rel bl
 
 (** Local universe and constraint declarations. *)
 

interp/constrintern.mli

@@ -169,11 +169,11 @@ val interp_type_evars : ?program_mode:bool -> env -> evar_map ->
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-val interp_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
+val interp_constr_evars_impls : ?program_mode:bool -> ?poly:PolyFlags.t -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
   evar_map * (constr * Impargs.manual_implicits)
 
-val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
+val interp_casted_constr_evars_impls : ?program_mode:bool -> ?poly:PolyFlags.t -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> types ->
   evar_map * (constr * Impargs.manual_implicits)
 
@@ -217,14 +217,14 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map *
 *)
 
 val interp_context_evars :
-  ?program_mode:bool -> ?unconstrained_sorts:bool -> ?impl_env:internalization_env ->
+  ?program_mode:bool -> ?unconstrained_sorts:bool -> ?poly:PolyFlags.t -> ?impl_env:internalization_env ->
   env -> evar_map -> local_binder_expr list ->
   evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits * Loc.t option list))
 
 (** Interpret named contexts *)
 
 val interp_named_context_evars :
-  ?program_mode:bool -> ?unconstrained_sorts:bool -> ?impl_env:internalization_env -> ?autoimp_enable:bool ->
+  ?program_mode:bool -> ?unconstrained_sorts:bool -> ?poly:PolyFlags.t -> ?impl_env:internalization_env -> ?autoimp_enable:bool ->
   env -> evar_map -> local_binder_expr list ->
   evar_map * (internalization_env * ((env * named_context) * Impargs.manual_implicits * Loc.t option list))
 

interp/modintern.ml

@@ -136,6 +136,9 @@ let interp_with_decl env base kind = function
     let sigma, udecl = interp_univ_decl_opt env udecl in
     let c, ectx = interp_constr env sigma c in
     let poly = lookup_polymorphism env base kind fqid in
+    let poly =
+      PolyFlags.of_univ_poly poly (* MS: FIXME: no sortpoly/cumulative support *)
+    in
     begin match fst (UState.check_univ_decl ~poly ectx udecl) with
       | UState.Polymorphic_entry ctx ->
         let inst, ctx = UVars.abstract_universes ctx in

plugins/derive/derive.ml

@@ -44,7 +44,7 @@ let rec fill_assumptions env sigma = function
 let start_deriving ~atts bl suchthat name : Declare.Proof.t =
 
   let scope, _local, poly, program_mode, user_warns, typing_flags, using, clearbody =
-    atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
+    atts.scope, atts.locality, atts.poly,  atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
   if program_mode then CErrors.user_err (Pp.str "Program mode not supported.");
 
   let env = Global.env () in
@@ -56,7 +56,8 @@ let start_deriving ~atts bl suchthat name : Declare.Proof.t =
   let locs = List.rev locs in
   let sigma, env', ctx' = fill_assumptions env sigma ctx' in
   let sigma = Evd.shelve sigma (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma))) in
-  let sigma, (suchthat, impargs) = Constrintern.interp_type_evars_impls env' sigma ~impls:impls_env suchthat in
+  let flags = { Pretyping.all_no_fail_flags with poly } in
+  let sigma, (suchthat, impargs) = Constrintern.interp_type_evars_impls ~flags env' sigma ~impls:impls_env suchthat in
   (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
   let goals =
     let open Proofview in
@@ -69,7 +70,7 @@ let start_deriving ~atts bl suchthat name : Declare.Proof.t =
             aux (EConstr.push_named d env) sigma ctx)) in
     aux env sigma ctx' in
   let kind = Decls.(IsDefinition Definition) in
-  let info = Declare.Info.make ~poly:(Attributes.is_universe_polymorphism ()) ~kind () in
+  let info = Declare.Info.make ~poly ~kind () in
   let extract_manual = function Some Impargs.{ impl_pos = (na,_,_); impl_expl = Manual; impl_max } -> Some (na, impl_max) | _ -> None in
   let cinfo =
     let open Declare.CInfo in