Merge PR #10614: Update the Gallina grammar in doc, "Terms" section

Ack-by: Zimmi48

2 files changed, 251 insertions, 99 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index a047bab421..ae0afc7819 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -79,14 +79,6 @@ To build an object of type :token:`ident`, one should provide the constructor
        Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
        Check half.
 
-.. FIXME: move this to the main grammar in the spec chapter
-
-.. _record-named-fields-grammar:
-
-  .. productionlist::
-    record_term : {| [`field_def` ; … ; `field_def`] |}
-    field_def : `ident` [`binders`] := `term`
-
 Alternatively, the following syntax allows creating objects by using named fields, as
 shown in this grammar. The fields do not have to be in any particular order, nor do they have
 to be all present if the missing ones can be inferred or prompted for
@@ -163,10 +155,11 @@ available:
 
 .. _record_projections_grammar:
 
-  .. productionlist:: terms
-     projection : `term` `.` ( `qualid` )
-          : `term` `.` ( `qualid` `arg` … `arg` )
-          : `term` `.` ( @`qualid` `term` … `term` )
+  .. insertgram term_projection term_projection
+
+  .. productionlist:: coq
+     term_projection : `term0` .( `qualid` `args_opt` )
+                     : `term0` .( @ `qualid` `term1_list_opt` )
 
   Syntax of Record projections
 
@@ -591,7 +584,7 @@ Advanced recursive functions
 
 The following experimental command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``:
 
-.. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term
+.. cmd:: Function @ident {* @binder} { @fixannot } : @type := @term
 
    This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper
    for several ways of defining a function *and other useful related
@@ -600,16 +593,11 @@ The following experimental command is available when the ``FunInd`` library has
    The meaning of this declaration is to define a function ident,
    similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must
    be given (unless the function is not recursive), but it might not
-   necessarily be *structurally* decreasing. The point of the :n:`{ @decrease_annot }` annotation
+   necessarily be *structurally* decreasing. The point of the :n:`{ @fixannot }` annotation
    is to name the decreasing argument *and* to describe which kind of
    decreasing criteria must be used to ensure termination of recursive
    calls.
 
-   .. productionlist::
-      decrease_annot : struct `ident`
-                     : measure `term` `ident`
-                     : wf `term` `ident`
-
 The ``Function`` construction also enjoys the ``with`` extension to define
 mutually recursive definitions. However, this feature does not work
 for non structurally recursive functions.
@@ -874,7 +862,7 @@ Sections create local contexts which can be shared across multiple definitions.
       :name: Let Fixpoint
       :undocumented:
 
-   .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}
+   .. cmdv:: Let CoFixpoint @ident @fix_body {* with @fix_body}
       :name: Let CoFixpoint
       :undocumented:
 
@@ -2323,6 +2311,18 @@ Printing universes
 Existential variables
 ---------------------
 
+.. insertgram term_evar evar_binding
+
+.. productionlist:: coq
+   term_evar : ?[ `ident` ]
+             : ?[ ?`ident` ]
+             : ?`ident` `evar_bindings_opt`
+   evar_bindings_opt : @{ `evar_bindings_semi` }
+                     : `empty`
+   evar_bindings_semi : `evar_bindings_semi` ; `evar_binding`
+                      : `evar_binding`
+   evar_binding : `ident` := `term`
+
 |Coq| terms can include existential variables which represents unknown
 subterms to eventually be replaced by actual subterms.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 94e9ccf0d4..3cc101d06b 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -52,7 +52,7 @@ Comments
   They can contain any character. However, embedded :token:`string` literals must be
   correctly closed. Comments are treated as blanks.
 
-Identifiers and field identifiers
+Identifiers
   Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and
   ``'``, that do not start with a digit or ``'``.  That is, they are
   recognized by the following grammar (except that the string ``_`` is reserved;
@@ -60,7 +60,6 @@ Identifiers and field identifiers
 
   .. productionlist:: coq
      ident             : `first_letter`[`subsequent_letter`…`subsequent_letter`]
-     field             : .`ident`
      first_letter      : a..z ∣ A..Z ∣ _ ∣ `unicode_letter`
      subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part`
 
@@ -71,10 +70,6 @@ Identifiers and field identifiers
   symbols and non-breaking space. :production:`unicode_id_part`
   non-exhaustively includes symbols for prime letters and subscripts.
 
-  Field identifiers, written :token:`field`, are identifiers prefixed by
-  `.` (dot) with no blank between the dot and the identifier. They are used in
-  the syntax of qualified identifiers.
-
 Numerals
   Numerals are sequences of digits with an optional fractional part
   and exponent, optionally preceded by a minus sign. :token:`int` is an integer;
@@ -144,62 +139,50 @@ presentation of Cic is given in Chapter :ref:`calculusofinductiveconstructions`.
 are given in Chapter :ref:`extensionsofgallina`. How to customize the syntax
 is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
 
-.. productionlist:: coq
-   term             : forall `binders` , `term`
-                    : fun `binders` => `term`
-                    : fix `fix_bodies`
-                    : cofix `cofix_bodies`
-                    : let `ident` [`binders`] [: `term`] := `term` in `term`
-                    : let fix `fix_body` in `term`
-                    : let cofix `cofix_body` in `term`
-                    : let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term`
-                    : let ' `pattern` [in `term`] := `term` [`return_type`] in `term`
-                    : if `term` [`dep_ret_type`] then `term` else `term`
-                    : `term` : `term`
-                    : `term` <: `term`
-                    : `term` :>
-                    : `term` -> `term`
-                    : `term` `arg` … `arg`
-                    : @ `qualid` [`term` … `term`]
-                    : `term` % `ident`
-                    : match `match_item` , … , `match_item` [`return_type`] with
-                    :   [[|] `equation` | … | `equation`] end
-                    : `qualid`
-                    : `sort`
-                    : `num`
-                    : _
-                    : ( `term` )
-   arg              : `term`
-                    : ( `ident` := `term` )
-   binders          : `binder` … `binder`
-   binder           : `name`
-                    : ( `name` … `name` : `term` )
-                    : ( `name` [: `term`] := `term` )
-                    : ' `pattern`
-   name             : `ident` | _
-   qualid           : `ident` | `qualid` `field`
-   sort             : SProp | Prop | Set | Type
-   fix_bodies       : `fix_body`
-                    : `fix_body` with `fix_body` with … with `fix_body` for `ident`
-   cofix_bodies     : `cofix_body`
-                    : `cofix_body` with `cofix_body` with … with `cofix_body` for `ident`
-   fix_body         : `ident` `binders` [`annotation`] [: `term`] := `term`
-   cofix_body       : `ident` [`binders`] [: `term`] := `term`
-   annotation       : { struct `ident` }
-   match_item       : `term` [as `name`] [in `qualid` [`pattern` … `pattern`]]
-   dep_ret_type     : [as `name`] `return_type`
-   return_type      : return `term`
-   equation         : `mult_pattern` | … | `mult_pattern` => `term`
-   mult_pattern     : `pattern` , … , `pattern`
-   pattern          : `qualid` `pattern` … `pattern`
-                    : @ `qualid` `pattern` … `pattern`
-                    : `pattern` as `ident`
-                    : `pattern` % `ident`
-                    : `qualid`
-                    : _
-                    : `num`
-                    : ( `pattern` | … | `pattern` )
+.. insertgram term binders_opt
 
+.. productionlist:: coq
+   term : forall `open_binders` , `term`
+        : fun `open_binders` => `term`
+        : `term_let`
+        : if `term` `as_return_type_opt` then `term` else `term`
+        : `term_fix`
+        : `term100`
+   term100 : `term_cast`
+           : `term10`
+   term10 : `term1` `args`
+          : @ `qualid` `universe_annot_opt` `term1_list_opt`
+          : `term1`
+   args : `args` `arg`
+        : `arg`
+   arg : ( `ident` := `term` )
+       : `term1`
+   term1_list_opt : `term1_list_opt` `term1`
+                  : `empty`
+   empty :
+   term1 : `term_projection`
+         : `term0` % `ident`
+         : `term0`
+   args_opt : `args`
+            : `empty`
+   term0 : `qualid` `universe_annot_opt`
+         : `sort`
+         : `numeral`
+         : `string`
+         : _
+         : `term_evar`
+         : `term_match`
+         : ( `term` )
+         : {| `fields_def` |}
+         : `{ `term` }
+         : `( `term` )
+         : ltac : ( `ltac_expr` )
+   fields_def : `field_def` ; `fields_def`
+              : `field_def`
+              : `empty`
+   field_def : `qualid` `binders_opt` := `term`
+   binders_opt : `binders`
+               : `empty`
 
 Types
 -----
@@ -213,6 +196,13 @@ of types inside the syntactic class :token:`term`.
 Qualified identifiers and simple identifiers
 --------------------------------------------
 
+.. insertgram qualid field
+
+.. productionlist:: coq
+   qualid : `qualid` `field`
+          : `ident`
+   field : .`ident`
+
 *Qualified identifiers* (:token:`qualid`) denote *global constants*
 (definitions, lemmas, theorems, remarks or facts), *global variables*
 (parameters or axioms), *inductive types* or *constructors of inductive
@@ -220,11 +210,15 @@ types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset
 of qualified identifiers. Identifiers may also denote *local variables*,
 while qualified identifiers do not.
 
-Numerals
---------
+Field identifiers, written :token:`field`, are identifiers prefixed by
+`.` (dot) with no blank between the dot and the identifier.
+
 
-Numerals have no definite semantics in the calculus. They are mere
-notations that can be bound to objects through the notation mechanism
+Numerals and strings
+--------------------
+
+Numerals and strings have no predefined semantics in the calculus. They are
+merely notations that can be bound to objects through the notation mechanism
 (see Chapter :ref:`syntaxextensionsandinterpretationscopes` for details).
 Initially, numerals are bound to Peano’s representation of natural
 numbers (see :ref:`datatypes`).
@@ -243,6 +237,35 @@ numbers (see :ref:`datatypes`).
 Sorts
 -----
 
+.. insertgram sort universe_level
+
+.. productionlist:: coq
+   sort : Set
+        : Prop
+        : SProp
+        : Type
+        : Type @{ _ }
+        : Type @{ `universe` }
+   universe : max ( `universe_exprs_comma` )
+            : `universe_expr`
+   universe_exprs_comma : `universe_exprs_comma` , `universe_expr`
+                        : `universe_expr`
+   universe_expr : `universe_name` `universe_increment_opt`
+   universe_name : `qualid`
+                 : Set
+                 : Prop
+   universe_increment_opt : + `num`
+                          : `empty`
+   universe_annot_opt : @{ `universe_levels_opt` }
+                      : `empty`
+   universe_levels_opt : `universe_levels_opt` `universe_level`
+                       : `empty`
+   universe_level : Set
+                  : Prop
+                  : Type
+                  : _
+                  : `qualid`
+
 There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set`  and :g:`Type`.
 
 -  :g:`SProp` is the universe of *definitionally irrelevant
@@ -266,6 +289,35 @@ More on sorts can be found in Section :ref:`sorts`.
 Binders
 -------
 
+.. insertgram open_binders exclam_opt
+
+.. productionlist:: coq
+   open_binders : `names` : `term`
+                : `binders`
+   names : `names` `name`
+         : `name`
+   name : _
+        : `ident`
+   binders : `binders` `binder`
+           : `binder`
+   binder : `name`
+          : ( `names` : `term` )
+          : ( `name` `colon_term_opt` := `term` )
+          : { `name` }
+          : { `names` `colon_term_opt` }
+          : `( `typeclass_constraints_comma` )
+          : `{ `typeclass_constraints_comma` }
+          : ' `pattern0`
+          : ( `name` : `term` | `term` )
+   typeclass_constraints_comma : `typeclass_constraints_comma` , `typeclass_constraint`
+                               : `typeclass_constraint`
+   typeclass_constraint : `exclam_opt` `term`
+                        : { `name` } : `exclam_opt` `term`
+                        : `name` : `exclam_opt` `term`
+   exclam_opt : !
+              : `empty`
+
+
 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
 variable is not used in the expression, the identifier can be replaced by the
@@ -291,8 +343,8 @@ the case of a single sequence of bindings sharing the same type (e.g.:
 
 .. index:: fun ... => ...
 
-Abstractions
-------------
+Abstractions: fun
+-----------------
 
 The expression :n:`fun @ident : @type => @term` defines the
 *abstraction* of the variable :token:`ident`, of type :token:`type`, over the term
@@ -313,8 +365,8 @@ Section :ref:`let-in`).
 
 .. index:: forall
 
-Products
---------
+Products: forall
+----------------
 
 The expression :n:`forall @ident : @type, @term` denotes the
 *product* of the variable :token:`ident` of type :token:`type`, over the term :token:`term`.
@@ -359,6 +411,14 @@ Section :ref:`explicit-applications`).
 Type cast
 ---------
 
+.. insertgram term_cast term_cast
+
+.. productionlist:: coq
+   term_cast : `term10` <: `term`
+             : `term10` <<: `term`
+             : `term10` : `term`
+             : `term10` :>
+
 The expression :n:`@term : @type` is a type cast expression. It enforces
 the type of :token:`term` to be :token:`type`.
 
@@ -384,6 +444,22 @@ guess the missing piece of information.
 Let-in definitions
 ------------------
 
+.. insertgram term_let names_comma
+
+.. productionlist:: coq
+   term_let : let `name` `colon_term_opt` := `term` in `term`
+            : let `name` `binders` `colon_term_opt` := `term` in `term`
+            : let `single_fix` in `term`
+            : let `names_tuple` `as_return_type_opt` := `term` in `term`
+            : let ' `pattern` := `term` `return_type_opt` in `term`
+            : let ' `pattern` in `pattern` := `term` `return_type` in `term`
+   colon_term_opt : : `term`
+                  : `empty`
+   names_tuple : ( `names_comma` )
+               : ()
+   names_comma : `names_comma` , `name`
+               : `name`
+
 :n:`let @ident := @term in @term’`
 denotes the local binding of :token:`term` to the variable
 :token:`ident` in :token:`term`’. There is a syntactic sugar for let-in
@@ -392,8 +468,60 @@ stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
 
 .. index:: match ... with ...
 
-Definition by case analysis
----------------------------
+Definition by cases: match
+--------------------------
+
+.. insertgram term_match record_pattern
+
+.. productionlist:: coq
+   term_match : match `case_items_comma` `return_type_opt` with `or_opt` `eqns_or_opt` end
+   case_items_comma : `case_items_comma` , `case_item`
+                    : `case_item`
+   return_type_opt : `return_type`
+                   : `empty`
+   as_return_type_opt : `as_name_opt` `return_type`
+                      : `empty`
+   return_type : return `term100`
+   case_item : `term100` `as_name_opt` `in_opt`
+   as_name_opt : as `name`
+               : `empty`
+   in_opt : in `pattern`
+          : `empty`
+   or_opt : |
+          : `empty`
+   eqns_or_opt : `eqns_or`
+               : `empty`
+   eqns_or : `eqns_or` | `eqn`
+           : `eqn`
+   eqn : `patterns_comma_list_or` => `term`
+   patterns_comma_list_or : `patterns_comma_list_or` | `patterns_comma`
+                          : `patterns_comma`
+   patterns_comma : `patterns_comma` , `pattern`
+                  : `pattern`
+   pattern : `pattern10` : `term`
+           : `pattern10`
+   pattern10 : `pattern1` as `name`
+             : `pattern1_list`
+             : @ `qualid` `pattern1_list_opt`
+             : `pattern1`
+   pattern1_list : `pattern1_list` `pattern1`
+                 : `pattern1`
+   pattern1_list_opt : `pattern1_list`
+                     : `empty`
+   pattern1 : `pattern0` % `ident`
+            : `pattern0`
+   pattern0 : `qualid`
+            : {| `record_patterns_opt` |}
+            : _
+            : ( `patterns_or` )
+            : `numeral`
+            : `string`
+   patterns_or : `patterns_or` | `pattern`
+               : `pattern`
+   record_patterns_opt : `record_patterns_opt` ; `record_pattern`
+                       : `record_pattern`
+                       : `empty`
+   record_pattern : `qualid` := `pattern`
 
 Objects of inductive types can be destructured by a case-analysis
 construction called *pattern matching* expression. A pattern matching
@@ -403,11 +531,11 @@ to apply specific treatments accordingly.
 This paragraph describes the basic form of pattern matching. See
 Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
 of the general form. The basic form of pattern matching is characterized
-by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a
+by a single :token:`case_item` expression, a :token:`patterns_comma` restricted to a
 single :token:`pattern` and :token:`pattern` restricted to the form
 :n:`@qualid {* @ident}`.
 
-The expression match ":token:`term`:math:`_0` :token:`return_type` with
+The expression match ":token:`term`:math:`_0` :token:`return_type_opt` with
 :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|`
 :token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a
 *pattern matching* over the term :token:`term`:math:`_0` (expected to be
@@ -417,10 +545,10 @@ expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid`
 :token:`ident` where :token:`qualid` must denote a constructor. There should be
 exactly one branch for every constructor of :math:`I`.
 
-The :token:`return_type` expresses the type returned by the whole match
+The :token:`return_type_opt` expresses the type returned by the whole match
 expression. There are several cases. In the *non dependent* case, all
-branches have the same type, and the :token:`return_type` is the common type of
-branches. In this case, :token:`return_type` can usually be omitted as it can be
+branches have the same type, and the :token:`return_type_opt` is the common type of
+branches. In this case, :token:`return_type_opt` can usually be omitted as it can be
 inferred from the type of the branches [2]_.
 
 In the *dependent* case, there are three subcases. In the first subcase,
@@ -520,8 +648,30 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`).
    single: fix
    single: cofix
 
-Recursive functions
--------------------
+Recursive and co-recursive functions: fix and cofix
+---------------------------------------------------
+
+.. insertgram term_fix term1_extended_opt
+
+.. productionlist:: coq
+   term_fix : `single_fix`
+            : `single_fix` with `fix_bodies` for `ident`
+   single_fix : fix `fix_body`
+              : cofix `fix_body`
+   fix_bodies : `fix_bodies` with `fix_body`
+              : `fix_body`
+   fix_body : `ident` `binders_opt` `fixannot_opt` `colon_term_opt` := `term`
+   fixannot_opt : `fixannot`
+                : `empty`
+   fixannot : { struct `ident` }
+            : { wf `term1_extended` `ident` }
+            : { measure `term1_extended` `ident_opt` `term1_extended_opt` }
+   term1_extended : `term1`
+                  : @ `qualid` `universe_annot_opt`
+   ident_opt : `ident`
+             : `empty`
+   term1_extended_opt : `term1_extended`
+                      : `empty`
 
 The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:``
 :token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` ``with … with``
@@ -547,6 +697,8 @@ syntax: :n:`let fix @ident @binders := @term in` stands for
 The Vernacular
 ==============
 
+.. insertgramXX vernac ident_opt2
+
 .. productionlist:: coq
    decorated-sentence : [ `decoration` … `decoration` ] `sentence`
    sentence           : `assumption`
@@ -568,7 +720,7 @@ The Vernacular
    ind_body           : `ident` [`binders`] : `term` :=
                       : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]]
    fixpoint           : Fixpoint `fix_body` with … with `fix_body` .
-                      : CoFixpoint `cofix_body` with … with `cofix_body` .
+                      : CoFixpoint `fix_body` with … with `fix_body` .
    assertion          : `assertion_keyword` `ident` [`binders`] : `term` .
    assertion_keyword  : Theorem | Lemma
                       : Remark | Fact