Convert Gallina Extensions to use prodn

4 files changed, 153 insertions, 87 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 0b94b0d675..6332c4c81d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -337,7 +337,7 @@ class TacticNotationObject(NotationObject):
     """
     subdomain = "tacn"
     index_suffix = "(tactic)"
-    annotation = None
+    annotation = "Tactic"
 
 class AttributeNotationObject(NotationObject):
     """An attribute.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 5bf122078d..541717581c 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -313,6 +313,7 @@ closed_binder: [
 | REPLACE "{" name LIST1 name ":" lconstr "}"
 | WITH "{" LIST1 name type_cstr "}"
 | DELETE "{" name ":" lconstr  "}"
+| MOVETO implicit_binders "{" LIST1 name type_cstr "}"
 
 | DELETE "[" name "]"
 | DELETE "[" name LIST1 name "]"
@@ -320,9 +321,14 @@ closed_binder: [
 | REPLACE "[" name LIST1 name ":" lconstr "]"
 | WITH "[" LIST1 name type_cstr "]"
 | DELETE "[" name ":" lconstr  "]"
+| MOVETO implicit_binders "[" LIST1 name type_cstr "]"
 
 | REPLACE "(" Prim.name ":" lconstr "|" lconstr ")"
 | WITH "(" Prim.name ":" type "|" lconstr ")"
+
+| MOVETO generalizing_binder "`(" LIST1 typeclass_constraint SEP "," ")"
+| MOVETO generalizing_binder "`{" LIST1 typeclass_constraint SEP "," "}"
+| MOVETO generalizing_binder "`[" LIST1 typeclass_constraint SEP "," "]"
 ]
 
 name_colon: [
@@ -383,6 +389,16 @@ evar_instance: [
 | OPTINREF
 ]
 
+(* No constructor syntax, OPT [ "|" binders ] is not supported for Record *)
+record_definition: [
+| opt_coercion ident_decl binders OPT [ ":" type ] OPT [ identref ] "{" record_fields "}"  decl_notations
+]
+
+(* No record syntax, opt_coercion not supported for Variant, := ... required *)
+variant_definition: [
+| ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" decl_notations
+]
+
 gallina: [
 | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
 | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ]
@@ -390,8 +406,8 @@ gallina: [
 | REPLACE finite_token LIST1 inductive_definition SEP "with"
 | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 |   "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
-|   "Variant" inductive_definition LIST0 ( "with" inductive_definition )
-|   [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition )
+|   "Variant" variant_definition LIST0 ( "with" variant_definition )
+|   [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition )
 |   "Class" inductive_definition LIST0 ( "with" inductive_definition )
 | REPLACE "Fixpoint" LIST1 rec_definition SEP "with"
 | WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
@@ -411,7 +427,7 @@ constructor_list_or_record_decl: [
 
 record_fields: [
 | REPLACE record_field ";" record_fields
-| WITH LIST1 record_field SEP ";"
+| WITH LIST0 record_field SEP ";"
 | DELETE record_field
 | DELETE (* empty *)
 ]
@@ -487,16 +503,39 @@ functor_app_annot: [
 ]
 
 is_module_expr: [
+| REPLACE ":=" module_expr_inl LIST0 ext_module_expr
+| WITH ":=" LIST1 module_expr_inl SEP "<+"
 | OPTINREF
 ]
 
 is_module_type: [
+| REPLACE ":=" module_type_inl LIST0 ext_module_type
+| WITH ":=" LIST1 module_type_inl SEP "<+"
 | OPTINREF
 ]
 
 gallina_ext: [
 | REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
 | WITH "Arguments" smart_global LIST0 argument_spec_block    LIST0 [  "," LIST0 more_implicits_block ]                OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| REPLACE "Implicit" "Type" reserv_list
+| WITH "Implicit" [ "Type" | "Types" ] reserv_list
+| DELETE "Implicit" "Types" reserv_list
+
+(* Per @Zimmi48, the global (qualid) must be a simple identifier if def_body is present
+   Note that smart_global is "qualid | by_notation" and that
+   ident_decl is "ident OPT univ_decl"; move
+ *)
+| REPLACE "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ]
+| WITH "Canonical" OPT "Structure" ident_decl def_body
+| REPLACE "Canonical" OPT "Structure" by_notation
+| WITH "Canonical" OPT "Structure" smart_global
+
+| REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type
+| WITH "Include" "Type" LIST1 module_type_inl SEP "<+"
+
+| REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
+| WITH "Generalizable" [  [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ]
+
 ]
 
 (* lexer stuff *)
@@ -661,7 +700,6 @@ command: [
 | WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc )      (* funind plugin *)
 | REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
 | WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )      (* funind plugin *)
-
 ]
 
 only_parsing: [
@@ -736,6 +774,18 @@ all_attrs: [
 | LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
 
+legacy_attr: [
+| REPLACE "Local"
+| WITH [ "Local" | "Global" ]
+| DELETE "Global"
+| REPLACE "Polymorphic"
+| WITH [ "Polymorphic" | "Monomorphic" ]
+| DELETE "Monomorphic"
+| REPLACE "Cumulative"
+| WITH [ "Cumulative" | "NonCumulative" ]
+| DELETE "NonCumulative"
+]
+
 vernacular: [
 | LIST0 ( OPT all_attrs [ command | tactic ] "." )
 ]
@@ -761,6 +811,7 @@ inductive_definition: [
 | WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations
 ]
 
+(* note that constructor -> identref constructor_type *)
 constructor_list_or_record_decl: [
 | DELETE "|" LIST1 constructor SEP "|"
 | REPLACE identref constructor_type "|" LIST1 constructor SEP "|"
@@ -777,6 +828,16 @@ record_binder: [
 | DELETE name
 ]
 
+of_module_type: [
+| (* empty *)
+| OPTINREF
+]
+
+simple_reserv: [
+| REPLACE LIST1 identref ":" lconstr
+| WITH LIST1 identref ":" type
+]
+
 in_clause: [
 | DELETE in_clause'
 | REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ
@@ -802,6 +863,12 @@ decl_notations: [
 | OPTINREF
 ]
 
+module_expr: [
+| REPLACE module_expr_atom
+| WITH LIST1 module_expr_atom
+| DELETE module_expr module_expr_atom
+]
+
 SPLICE: [
 | noedit_mode
 | command_entry
@@ -935,8 +1002,14 @@ SPLICE: [
 | record_fields
 | constructor_type
 | record_binder
+| export_token
+| reserv_tuple
+| inst
 | opt_coercion
 | opt_constructors_or_fields
+| is_module_type
+| is_module_expr
+| module_expr
 ] (* end SPLICE *)
 
 RENAME: [
@@ -979,7 +1052,6 @@ RENAME: [
 | appl_arg arg
 | rec_definition fix_definition
 | corec_definition cofix_definition
-| inst evar_binding
 | univ_instance univ_annot
 | simple_assum_coe assumpt
 | of_type_with_opt_coercion of_type
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 2fabf92b7f..241cf48cf1 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -430,17 +430,21 @@ lstring: [
 ]
 
 integer: [
-| NUMERAL
-| test_minus_nat "-" NUMERAL
+| bigint
 ]
 
 natural: [
-| NUMERAL
+| bignat
 | _natural
 ]
 
 bigint: [
 | NUMERAL
+| test_minus_nat "-" NUMERAL
+]
+
+bignat: [
+| NUMERAL
 ]
 
 bar_cbrace: [
@@ -2516,7 +2520,7 @@ field_mods: [
 
 numnotoption: [
 |
-| "(" "warning" "after" bigint ")"
-| "(" "abstract" "after" bigint ")"
+| "(" "warning" "after" bignat ")"
+| "(" "abstract" "after" bignat ")"
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index c3634466cc..2d933e8f8a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -96,11 +96,7 @@ term_projection: [
 term_evar: [
 | "?[" ident "]"
 | "?[" "?" ident "]"
-| "?" ident OPT ( "@{" LIST1 evar_binding SEP ";" "}" )
-]
-
-evar_binding: [
-| ident ":=" term
+| "?" ident OPT ( "@{" LIST1 ( ident ":=" term ) SEP ";" "}" )
 ]
 
 dangling_pattern_extension_rule: [
@@ -185,12 +181,9 @@ attr_value: [
 ]
 
 legacy_attr: [
-| "Local"
-| "Global"
-| "Polymorphic"
-| "Monomorphic"
-| "Cumulative"
-| "NonCumulative"
+| [ "Local" | "Global" ]
+| [ "Polymorphic" | "Monomorphic" ]
+| [ "Cumulative" | "NonCumulative" ]
 | "Private"
 | "Program"
 ]
@@ -285,13 +278,21 @@ binder: [
 | name
 | "(" LIST1 name ":" type ")"
 | "(" name OPT ( ":" type ) ":=" term ")"
+| implicit_binders
+| generalizing_binder
 | "(" name ":" type "|" term ")"
+| "'" pattern0
+]
+
+implicit_binders: [
 | "{" LIST1 name OPT ( ":" type ) "}"
 | "[" LIST1 name OPT ( ":" type ) "]"
+]
+
+generalizing_binder: [
 | "`(" LIST1 typeclass_constraint SEP "," ")"
 | "`{" LIST1 typeclass_constraint SEP "," "}"
 | "`[" LIST1 typeclass_constraint SEP "," "]"
-| "'" pattern0
 ]
 
 typeclass_constraint: [
@@ -371,8 +372,8 @@ gallina: [
 | "Let" ident def_body
 | "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 | "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
-| "Variant" inductive_definition LIST0 ( "with" inductive_definition )
-| [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition )
+| "Variant" variant_definition LIST0 ( "with" variant_definition )
+| [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition )
 | "Class" inductive_definition LIST0 ( "with" inductive_definition )
 | "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
 | "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
@@ -490,15 +491,6 @@ delta_flag: [
 | OPT "-" "[" LIST1 smart_qualid "]"
 ]
 
-smart_qualid: [
-| qualid
-| by_notation
-]
-
-by_notation: [
-| string OPT [ "%" ident ]
-]
-
 strategy_flag: [
 | LIST1 red_flags
 | delta_flag
@@ -551,17 +543,12 @@ finite_token: [
 | "Class"
 ]
 
-inductive_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
-]
-
-constructors_or_record: [
-| OPT "|" LIST1 constructor SEP "|"
-| OPT ident "{" LIST1 record_field SEP ";" "}"
+variant_definition: [
+| ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" OPT decl_notations
 ]
 
-constructor: [
-| ident LIST0 binder OPT of_type
+record_definition: [
+| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations
 ]
 
 record_field: [
@@ -574,6 +561,19 @@ field_body: [
 | LIST0 binder ":=" term
 ]
 
+inductive_definition: [
+| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
+]
+
+constructors_or_record: [
+| OPT "|" LIST1 constructor SEP "|"
+| OPT ident "{" LIST0 record_field SEP ";" "}"
+]
+
+constructor: [
+| ident LIST0 binder OPT of_type
+]
+
 cofix_definition: [
 | ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
@@ -599,24 +599,24 @@ sort_family: [
 ]
 
 gallina_ext: [
-| "Module" OPT export_token ident LIST0 module_binder of_module_type OPT is_module_expr
-| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT is_module_type
-| "Declare" "Module" OPT export_token ident LIST0 module_binder ":" module_type_inl
+| "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder OPT of_module_type OPT ( ":=" LIST1 module_expr_inl SEP "<+" )
+| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
+| "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
 | "Section" ident
 | "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
-| "Require" OPT export_token LIST1 qualid
-| "From" qualid "Require" OPT export_token LIST1 qualid
+| "Require" OPT [ "Import" | "Export" ] LIST1 qualid
+| "From" qualid "Require" OPT [ "Import" | "Export" ] LIST1 qualid
 | "Import" LIST1 qualid
 | "Export" LIST1 qualid
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
-| "Include" "Type" module_type_inl LIST0 ( "<+" module_type_inl )
+| "Include" "Type" LIST1 module_type_inl SEP "<+"
 | "Transparent" LIST1 smart_qualid
 | "Opaque" LIST1 smart_qualid
 | "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ]
-| "Canonical" OPT "Structure" qualid OPT [ OPT univ_decl def_body ]
-| "Canonical" OPT "Structure" by_notation
+| "Canonical" OPT "Structure" ident_decl def_body
+| "Canonical" OPT "Structure" smart_qualid
 | "Coercion" qualid OPT univ_decl def_body
 | "Identity" "Coercion" ident ":" class ">->" class
 | "Coercion" qualid ":" class ">->" class
@@ -627,9 +627,8 @@ gallina_ext: [
 | "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 "," ]
-| "Implicit" "Type" reserv_list
-| "Implicit" "Types" reserv_list
-| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ]
+| "Implicit" [ "Type" | "Types" ] reserv_list
+| "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
 | "Export" "Set" LIST1 ident option_setting
 | "Export" "Unset" LIST1 ident
 ]
@@ -645,13 +644,8 @@ hint_info: [
 |
 ]
 
-export_token: [
-| "Import"
-| "Export"
-]
-
 module_binder: [
-| "(" OPT export_token LIST1 ident ":" module_type_inl ")"
+| "(" OPT [ "Import" | "Export" ] LIST1 ident ":" module_type_inl ")"
 ]
 
 module_type_inl: [
@@ -659,6 +653,11 @@ module_type_inl: [
 | module_type OPT functor_app_annot
 ]
 
+functor_app_annot: [
+| "[" "inline" "at" "level" num "]"
+| "[" "no" "inline" "]"
+]
+
 module_type: [
 | qualid
 | "(" module_type ")"
@@ -671,9 +670,9 @@ with_declaration: [
 | "Module" qualid ":=" qualid
 ]
 
-functor_app_annot: [
-| "[" "inline" "at" "level" num "]"
-| "[" "no" "inline" "]"
+module_expr_atom: [
+| qualid
+| "(" LIST1 module_expr_atom ")"
 ]
 
 of_module_type: [
@@ -681,27 +680,18 @@ of_module_type: [
 | LIST0 ( "<:" module_type_inl )
 ]
 
-is_module_type: [
-| ":=" module_type_inl LIST0 ( "<+" module_type_inl )
+module_expr_inl: [
+| "!" LIST1 module_expr_atom
+| LIST1 module_expr_atom OPT functor_app_annot
 ]
 
-module_expr_atom: [
+smart_qualid: [
 | qualid
-| "(" module_expr ")"
-]
-
-module_expr: [
-| module_expr_atom
-| module_expr module_expr_atom
-]
-
-is_module_expr: [
-| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl )
+| by_notation
 ]
 
-module_expr_inl: [
-| "!" module_expr
-| module_expr OPT functor_app_annot
+by_notation: [
+| string OPT [ "%" ident ]
 ]
 
 argument_spec_block: [
@@ -750,16 +740,12 @@ instance_name: [
 ]
 
 reserv_list: [
-| LIST1 reserv_tuple
+| LIST1 ( "(" simple_reserv ")" )
 | simple_reserv
 ]
 
-reserv_tuple: [
-| "(" simple_reserv ")"
-]
-
 simple_reserv: [
-| LIST1 ident ":" term
+| LIST1 ident ":" type
 ]
 
 command: [
@@ -1049,6 +1035,10 @@ dirpath: [
 | dirpath field_ident
 ]
 
+bignat: [
+| numeral
+]
+
 locatable: [
 | smart_qualid
 | "Term" smart_qualid
@@ -1117,8 +1107,8 @@ ltac_production_item: [
 ]
 
 numnotoption: [
-| "(" "warning" "after" num ")"
-| "(" "abstract" "after" num ")"
+| "(" "warning" "after" bignat ")"
+| "(" "abstract" "after" bignat ")"
 ]
 
 mlname: [