Add "& T" syntax for anonymous binder "(_ : T)" and "of _ & _ & _" syntax for constructors

doc/changelog/02-specification-language/21611-of-ampersand.rst

@@ -0,0 +1,7 @@
+- **Added:**
+  new syntactic sugars `& T` for anonymous binders `(_ : T)`
+  and `of T & ... & T` for anonymous binders in constructors, enabling the
+  `Variant t := C1 of a & b & c | C2 x y of P x & Q y.` syntax.
+  This adds the new reserved keyword `of`
+  (`#21611 <https://github.com/rocq-prover/rocq/pull/21611>`_,
+  by Pierre Roux).

doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst

@@ -0,0 +1,5 @@
+- **Removed:**
+  the `of T` syntax for anonymous binders outside of constructors,
+  use `& T` instead
+  (`#21611 <https://github.com/rocq-prover/rocq/pull/21611>`_,
+  by Pierre Roux).

doc/sphinx/language/core/assumptions.rst

@@ -20,6 +20,7 @@ Binders
    | @generalizing_binder
    | ( @name : @type %| @term )
    | ' @pattern0
+   | & @term99
 
 Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix`
 *bind* variables. A binding is represented by an identifier. If the binding
@@ -38,6 +39,8 @@ variable can be introduced at the same time. It is also possible to give
 the type of the variable as follows:
 :n:`(@ident : @type := @term)`.
 
+:n:`& @term99` is syntactic sugar for the anonymous binder :n:`(_ : @term99)`.
+
 `(x : T | P)` is syntactic sugar for `(x : @Corelib.Init.Specif.sig _ (fun x : T => P))`,
 which would more typically be written `(x : {x : T | P})`.
 Since `(x : T | P)` uses `sig` directly,

doc/sphinx/language/core/basic.rst

@@ -189,7 +189,7 @@ Keywords
 
     _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
     SProp Set Theorem Type Variable as at cofix else end
-    fix for forall fun if in let match return then where with
+    fix for forall fun if in let match of return then where with
 
   The following are keywords defined in notations or plugins loaded in the :term:`prelude`::
 

doc/sphinx/language/core/inductive.rst

@@ -32,7 +32,7 @@ Inductive types
 
    .. prodn::
       inductive_definition ::= @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } := {? {? %| } {+| @constructor } } {? @decl_notations }
-      constructor ::= {* #[ {+, @attribute } ] } @ident {* @binder } {? @of_type_inst }
+      constructor ::= {* #[ {+, @attribute } ] } @ident {* @binder } {? of {+& @term99 } } {? @of_type_inst }
 
    Defines one or more
    inductive types and its constructors.  Rocq generates
@@ -100,6 +100,9 @@ Inductive types
    Constructor :n:`@ident`\s can come with :n:`@binder`\s, in which case
    the actual type of the constructor is :n:`forall {* @binder }, @type`.
 
+   :n:`{? of {+& @term99 } }`
+     `of T1 & ... & Tn` is syntactic sugar for anonymous binders `(_ : T1) ... (_ : Tn)`.
+
    .. exn:: Non strictly positive occurrence of @ident in @type.
 
       The types of the constructors have to satisfy a *positivity

doc/tools/docgram/common.edit_mlg

@@ -1457,8 +1457,8 @@ assumpt: [
 ]
 
 constructor_type: [
-| REPLACE binders [ of_type_inst lconstr | ]
-| WITH binders OPT of_type_inst
+| REPLACE constructor_binders [ of_type_inst lconstr | ]
+| WITH constructor_binders OPT of_type_inst
 ]
 
 (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
@@ -2299,6 +2299,7 @@ SPLICE: [
 | preident
 | lpar_id_coloneq
 | binders
+| constructor_binders
 | check_module_types
 | decl_sep
 | function_fix_definition (* loses funind annotation *)

doc/tools/docgram/fullGrammar

@@ -348,6 +348,7 @@ closed_binder: [
 | "`{" LIST1 typeclass_constraint SEP "," "}"
 | "`[" LIST1 typeclass_constraint SEP "," "]"
 | "'" pattern0
+| "&" term99
 ]
 
 one_open_binder: [
@@ -1135,8 +1136,12 @@ assumpt: [
 | LIST1 ident_decl of_type lconstr
 ]
 
+constructor_binders: [
+| binders OPT [ "of" LIST1 term99 SEP "&" ]
+]
+
 constructor_type: [
-| binders [ of_type_inst lconstr | ]
+| constructor_binders [ of_type_inst lconstr | ]
 ]
 
 constructor: [

doc/tools/docgram/orderedGrammar

@@ -405,6 +405,7 @@ binder: [
 | generalizing_binder
 | "(" name ":" type "|" term ")"
 | "'" pattern0
+| "&" term99
 ]
 
 implicit_binders: [
@@ -572,7 +573,7 @@ inductive_definition: [
 ]
 
 constructor: [
-| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident LIST0 binder OPT of_type_inst
+| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident LIST0 binder OPT [ "of" LIST1 term99 SEP "&" ] OPT of_type_inst
 ]
 
 import_categories: [

parsing/g_constr.mlg

@@ -508,7 +508,9 @@ GRAMMAR EXTEND Gram
         { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (MaxImplicit, b), t)) tc }
       | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
         { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (NonMaxImplicit, b), t)) tc }
-      | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } ] ]
+      | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] }
+      | "&"; c = term LEVEL "99" ->
+        { [CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)] } ] ]
   ;
   one_open_binder:
     [ [ na = name -> { (pat_of_name na, Explicit) }

plugins/ssr/ssrvernac.mlg

@@ -116,14 +116,6 @@ GRAMMAR EXTEND Gram
   ] ];
 END
 
-GRAMMAR EXTEND Gram
-  GLOBAL: closed_binder;
-  closed_binder: TOP [
-    [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" ->
-      { [CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)] }
-  ] ];
-END
-
 (** Vernacular commands: Prenex Implicits *)
 
 (* This should really be implemented as an extension to the implicit   *)

test-suite/output/PrintKeywords.out

@@ -83,6 +83,7 @@ if
 in
 let
 match
+of
 return
 then
 using

test-suite/prerequisite/ssr_mini_mathcomp.v

@@ -695,7 +695,7 @@ Structure type := Pack {sort; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
 Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
+Definition clone c & phant_id class c := @Pack T c T.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
@@ -798,7 +798,7 @@ Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
 Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
+Definition clone c & phant_id class c := @Pack T c T.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
@@ -948,7 +948,7 @@ Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
 Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
+Definition clone c & phant_id class c := @Pack T c T.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 

theories/Corelib/Classes/CMorphisms.v

@@ -437,7 +437,7 @@ Section GenericInstances.
     Proper R' (m x).
   Proof. simpl_crelation. Qed.
 
-  Class Params {A} (of : A) (arity : nat).
+  Class Params {A} (from : A) (arity : nat).
 
   Lemma flip_respectful {A B} (R : crelation A) (R' : crelation B) :
     relation_equivalence (flip (R ==> R')) (flip R ==> flip R').

theories/Corelib/Classes/Morphisms.v

@@ -538,7 +538,7 @@ Class PartialApplication.
 
 CoInductive normalization_done : Prop := did_normalization.
 
-Class Params {A : Type} (of : A) (arity : nat).
+Class Params {A : Type} (from : A) (arity : nat).
 #[global] Instance eq_pars : Params (@eq) 1 := {}.
 #[global] Instance iff_pars : Params (@iff) 0 := {}.
 #[global] Instance impl_pars : Params (@impl) 0 := {}.

theories/Corelib/ssr/ssreflect.v

@@ -231,7 +231,7 @@ Variant put vT sT (v1 v2 : vT) (s : sT) : Prop := Put.
 
 Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
 
-Definition get_by vT sT of sT -> vT := @get vT sT.
+Definition get_by vT sT & sT -> vT := @get vT sT.
 
 End TheCanonical.
 

vernac/g_vernac.mlg

@@ -639,9 +639,17 @@ GRAMMAR EXTEND Gram
         { (oc,(idl,c)) } ] ]
   ;
 
+  constructor_binders:
+    [ [ l1 = binders; l2 = OPT [ "of"; l = LIST1 term LEVEL "99" SEP "&" -> { l } ] ->
+        { let anon c =
+            let n = CAst.make ?loc:c.CAst.loc Anonymous in
+            CLocalAssum ([n], None, Default Explicit, c) in
+          l1 @ List.map anon (Option.default [] l2) } ] ]
+  ;
+
   constructor_type:
-    [[ l = binders;
-      t= [ coe = of_type_inst; c = lconstr ->
+    [[ l = constructor_binders;
+       t = [ coe = of_type_inst; c = lconstr ->
                     { fun l attr id -> ((attr, fst coe, snd coe),(id,mkProdCN ~loc l c)) }
             |  ->
                  { fun l attr id -> ((attr,NoCoercion,NoInstance),(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None)))) } ]