Merge PR #11718: Convert syntax extensions chapter to prodn

Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: cpitclaudel

3 files changed, 159 insertions, 87 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 700170b3c6..6111eaa160 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -224,10 +224,18 @@ IDENT: [
 | ident
 ]
 
-scope: [
+scope_key: [
+| IDENT
+]
+
+scope_name: [
 | IDENT
 ]
 
+scope: [
+| scope_name | scope_key
+]
+
 operconstr100: [
 | MOVETO term_cast operconstr99 "<:" operconstr200
 | MOVETO term_cast operconstr99 "<<:" operconstr200
@@ -250,7 +258,7 @@ operconstr1: [
 | REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
 | WITH    operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *)
 | REPLACE operconstr0 "%" IDENT
-| WITH operconstr0 "%" scope
+| WITH operconstr0 "%" scope_key
 | MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
 | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
 ]
@@ -376,7 +384,7 @@ pattern10: [
 
 pattern1: [
 | REPLACE pattern0 "%" IDENT
-| WITH pattern0 "%" scope
+| WITH pattern0 "%" scope_key
 ]
 
 pattern0: [
@@ -879,9 +887,14 @@ bar_cbrace: [
 ]
 
 printable: [
+| REPLACE "Scope" IDENT
+| WITH "Scope" scope_name
+| REPLACE "Visibility" OPT IDENT
+| WITH "Visibility" OPT scope_name
 | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
 | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string
 | DELETE "Term" smart_global OPT univ_name_list  (* readded in commands *)
+
 | INSERTALL "Print"
 ]
 
@@ -1012,27 +1025,60 @@ command: [
 | REPLACE "Print" smart_global OPT univ_name_list
 | WITH "Print" OPT "Term" smart_global OPT univ_name_list
 
-]
+| REPLACE "Declare" "Scope" IDENT
+| WITH "Declare" "Scope" scope_name
+
+(* odd that these are in command while other notation-related ones are in syntax *)
+| REPLACE "Numeral" "Notation" reference reference reference ":" ident numnotoption
+| WITH "Numeral" "Notation" reference reference reference ":" scope_name numnotoption
+| REPLACE "String" "Notation" reference reference reference ":" ident
+| WITH "String" "Notation" reference reference reference ":" scope_name
 
-option_setting: [
-| OPTINREF
 ]
 
-only_parsing: [
+option_setting: [
 | OPTINREF
 ]
 
 syntax: [
+| REPLACE "Open" "Scope" IDENT
+| WITH "Open" "Scope" scope
+| REPLACE "Close" "Scope" IDENT
+| WITH "Close" "Scope" scope
+| REPLACE "Delimit" "Scope" IDENT; "with" IDENT
+| WITH "Delimit" "Scope" scope_name; "with" scope_key
+| REPLACE "Undelimit" "Scope" IDENT
+| WITH "Undelimit" "Scope" scope_name
+| REPLACE "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
+| WITH "Bind" "Scope" scope_name; "with" LIST1 class_rawexpr
 | REPLACE "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
-| WITH    "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ]
+| WITH    "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
 | REPLACE "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
-| WITH    "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ]
+| WITH    "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
 | REPLACE "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
 | WITH    "Reserved" "Infix" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
 | REPLACE "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
 | WITH    "Reserved" "Notation" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
 ]
 
+syntax_modifier: [
+| DELETE "in" "custom" IDENT
+| REPLACE "in" "custom" IDENT; "at" "level" natural
+| WITH "in" "custom" IDENT OPT ( "at" "level" natural )
+| REPLACE IDENT; "," LIST1 IDENT SEP "," "at" level
+| WITH LIST1 IDENT SEP "," "at" level
+]
+
+syntax_extension_type: [
+| REPLACE "strict" "pattern" "at" "level" natural
+| WITH "strict" "pattern" OPT ( "at" "level" natural )
+| DELETE "strict" "pattern"
+| DELETE "pattern"
+| REPLACE "pattern" "at" "level" natural
+| WITH "pattern" OPT ( "at" "level" natural )
+| DELETE "constr"    (* covered by another prod *)
+]
+
 numnotoption: [
 | OPTINREF
 ]
@@ -1407,12 +1453,12 @@ positive_search_mark: [
 
 by_notation: [
 | REPLACE ne_string OPT [ "%" IDENT ]
-| WITH ne_string OPT [ "%" scope ]
+| WITH ne_string OPT [ "%" scope_key ]
 ]
 
 scope_delimiter: [
 | REPLACE "%" IDENT
-| WITH "%" scope
+| WITH "%" scope_key
 ]
 
 (* Don't show these details *)
@@ -1422,6 +1468,23 @@ DELETE: [
 | register_type_token
 ]
 
+
+decl_notation: [
+| REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
+| WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ]
+]
+
+
+only_parsing: [
+| OPTINREF
+]
+
+ltac_production_item: [
+| REPLACE ident "(" ident OPT ltac_production_sep ")"
+| WITH ident OPT ( "(" ident OPT ltac_production_sep ")" )
+| DELETE ident
+]
+
 SPLICE: [
 | noedit_mode
 | bigint
@@ -1588,6 +1651,7 @@ SPLICE: [
 | searchabout_queries
 | locatable
 | scope_delimiter
+| bignat
 | one_import_filter_name
 ] (* end SPLICE *)
 
@@ -1640,6 +1704,12 @@ RENAME: [
 | smart_global smart_qualid
 | searchabout_query search_item
 | option_table setting_name
+| argument_spec_block arg_specs
+| more_implicits_block implicits_alt
+| arguments_modifier args_modifier
+| constr_as_binder_kind binder_interp
+| syntax_extension_type explicit_subentry
+| numnotoption numeral_modifier
 ]
 
 (* todo: positive_search_mark is a lousy name for OPT "-" *)
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index f00fda0e8c..98f826cd29 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1771,11 +1771,13 @@ let process_rst g file args seen tac_prods cmd_prods =
     "doc/sphinx/language/core/records.rst";
     "doc/sphinx/language/core/sections.rst";
     "doc/sphinx/language/extensions/implicit-arguments.rst";
+    "doc/sphinx/language/extensions/arguments-command.rst";
     "doc/sphinx/language/using/libraries/funind.rst";
 
     "doc/sphinx/language/gallina-specification-language.rst";
     "doc/sphinx/language/gallina-extensions.rst";
-    "doc/sphinx/proof-engine/vernacular-commands.rst"
+    "doc/sphinx/proof-engine/vernacular-commands.rst";
+    "doc/sphinx/user-extensions/syntax-extensions.rst"
   ]
   in
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index e71c80f829..2a30c03dd2 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -47,7 +47,7 @@ one_term: [
 
 term1: [
 | term_projection
-| term0 "%" scope
+| term0 "%" scope_key
 | term0
 ]
 
@@ -343,7 +343,7 @@ pattern10: [
 ]
 
 pattern1: [
-| pattern0 "%" scope
+| pattern0 "%" scope_key
 | pattern0
 ]
 
@@ -372,14 +372,6 @@ fix_definition: [
 | ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
 
-decl_notations: [
-| "where" decl_notation LIST0 ( "and" decl_notation )
-]
-
-decl_notation: [
-| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ]
-]
-
 thm_token: [
 | "Theorem"
 | "Lemma"
@@ -571,43 +563,52 @@ smart_qualid: [
 ]
 
 by_notation: [
-| string OPT [ "%" scope ]
+| string OPT [ "%" scope_key ]
+]
+
+argument_spec: [
+| OPT "!" name OPT ( "%" scope_key )
 ]
 
-argument_spec_block: [
+arg_specs: [
 | argument_spec
 | "/"
 | "&"
-| "(" LIST1 argument_spec ")" OPT ( "%" scope )
-| "[" LIST1 argument_spec "]" OPT ( "%" scope )
-| "{" LIST1 argument_spec "}" OPT ( "%" scope )
-]
-
-argument_spec: [
-| OPT "!" name OPT ( "%" scope )
+| "(" LIST1 argument_spec ")" OPT ( "%" scope_key )
+| "[" LIST1 argument_spec "]" OPT ( "%" scope_key )
+| "{" LIST1 argument_spec "}" OPT ( "%" scope_key )
 ]
 
-more_implicits_block: [
+implicits_alt: [
 | name
 | "[" LIST1 name "]"
 | "{" LIST1 name "}"
 ]
 
-arguments_modifier: [
+args_modifier: [
 | "simpl" "nomatch"
 | "simpl" "never"
 | "default" "implicits"
-| "clear" "bidirectionality" "hint"
 | "clear" "implicits"
 | "clear" "scopes"
-| "clear" "scopes" "and" "implicits"
-| "clear" "implicits" "and" "scopes"
+| "clear" "bidirectionality" "hint"
 | "rename"
 | "assert"
 | "extra" "scopes"
+| "clear" "scopes" "and" "implicits"
+| "clear" "implicits" "and" "scopes"
 ]
 
 scope: [
+| scope_name
+| scope_key
+]
+
+scope_name: [
+| ident
+]
+
+scope_key: [
 | ident
 ]
 
@@ -629,7 +630,6 @@ simple_reserv: [
 
 command: [
 | "Goal" term
-| "Declare" "Scope" ident
 | "Pwd"
 | "Cd" OPT string
 | "Load" OPT "Verbose" [ string | ident ]
@@ -669,8 +669,8 @@ command: [
 | "Print" "Hint" "*"
 | "Print" "HintDb" ident
 | "Print" "Scopes"
-| "Print" "Scope" ident
-| "Print" "Visibility" OPT ident
+| "Print" "Scope" scope_name
+| "Print" "Visibility" OPT scope_name
 | "Print" "Implicit" smart_qualid
 | "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
 | "Print" "Assumptions" smart_qualid
@@ -728,6 +728,7 @@ command: [
 | "Hint" hint OPT ( ":" LIST1 ident )
 | "Comments" LIST0 comment
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
+| "Declare" "Scope" scope_name
 | "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
 | "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr )
 | "Solve" "Obligation" int OPT ( "of" ident ) "with" ltac_expr
@@ -821,8 +822,8 @@ command: [
 | "Print" "Rings"      (* setoid_ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
-| "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption
-| "String" "Notation" qualid qualid qualid ":" ident
+| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
+| "String" "Notation" qualid qualid qualid ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
 | assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
@@ -871,19 +872,19 @@ command: [
 | "Existing" "Instance" qualid OPT hint_info
 | "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
 | "Existing" "Class" qualid
-| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| "Arguments" smart_qualid LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
 | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
 | "Set" setting_name OPT [ int | string ]
 | "Unset" setting_name
-| "Open" "Scope" ident
-| "Close" "Scope" ident
-| "Delimit" "Scope" ident "with" ident
-| "Undelimit" "Scope" ident
-| "Bind" "Scope" ident "with" LIST1 class
-| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
+| "Open" "Scope" scope
+| "Close" "Scope" scope
+| "Delimit" "Scope" scope_name "with" scope_key
+| "Undelimit" "Scope" scope_name
+| "Bind" "Scope" scope_name "with" LIST1 class
+| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
 | "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
-| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
+| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
 | "Format" "Notation" string string string
 | "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
 | "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
@@ -940,10 +941,6 @@ dirpath: [
 | LIST0 ( ident "." ) ident
 ]
 
-bignat: [
-| numeral
-]
-
 setting_name: [
 | LIST1 ident
 ]
@@ -956,7 +953,7 @@ comment: [
 
 search_item: [
 | one_term
-| string OPT ( "%" scope )
+| string OPT ( "%" scope_key )
 ]
 
 univ_name_list: [
@@ -987,13 +984,7 @@ tacdef_body: [
 
 ltac_production_item: [
 | string
-| ident "(" ident OPT ( "," string ) ")"
-| ident
-]
-
-numnotoption: [
-| "(" "warning" "after" bignat ")"
-| "(" "abstract" "after" bignat ")"
+| ident OPT ( "(" ident OPT ( "," string ) ")" )
 ]
 
 int_or_id: [
@@ -1033,6 +1024,11 @@ field_mod: [
 | "completeness" one_term      (* setoid_ring plugin *)
 ]
 
+numeral_modifier: [
+| "(" "warning" "after" numeral ")"
+| "(" "abstract" "after" numeral ")"
+]
+
 hints_path: [
 | "(" hints_path ")"
 | hints_path "*"
@@ -1050,46 +1046,50 @@ class: [
 | smart_qualid
 ]
 
-level: [
-| "level" num
-| "next" "level"
-]
-
 syntax_modifier: [
 | "at" "level" num
-| "in" "custom" ident
-| "in" "custom" ident "at" "level" num
+| "in" "custom" ident OPT ( "at" "level" num )
+| LIST1 ident SEP "," "at" level
+| ident "at" level OPT binder_interp
+| ident explicit_subentry
+| ident binder_interp
 | "left" "associativity"
 | "right" "associativity"
 | "no" "associativity"
-| "only" "printing"
 | "only" "parsing"
+| "only" "printing"
 | "format" string OPT string
-| ident "," LIST1 ident SEP "," "at" level
-| ident "at" level OPT constr_as_binder_kind
-| ident constr_as_binder_kind
-| ident syntax_extension_type
 ]
 
-constr_as_binder_kind: [
-| "as" "ident"
-| "as" "pattern"
-| "as" "strict" "pattern"
-]
-
-syntax_extension_type: [
+explicit_subentry: [
 | "ident"
 | "global"
 | "bigint"
+| "strict" "pattern" OPT ( "at" "level" num )
 | "binder"
-| "constr"
-| "constr" OPT ( "at" level ) OPT constr_as_binder_kind
-| "pattern"
-| "pattern" "at" "level" num
-| "strict" "pattern"
-| "strict" "pattern" "at" "level" num
 | "closed" "binder"
-| "custom" ident OPT ( "at" level ) OPT constr_as_binder_kind
+| "constr" OPT ( "at" level ) OPT binder_interp
+| "custom" ident OPT ( "at" level ) OPT binder_interp
+| "pattern" OPT ( "at" "level" num )
+]
+
+binder_interp: [
+| "as" "ident"
+| "as" "pattern"
+| "as" "strict" "pattern"
+]
+
+level: [
+| "level" num
+| "next" "level"
+]
+
+decl_notations: [
+| "where" decl_notation LIST0 ( "and" decl_notation )
+]
+
+decl_notation: [
+| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" scope_name ]
 ]
 
 simple_tactic: [