Move essential vocabulary and syntax conventions to section on basics.

3 files changed, 104 insertions, 41 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 6111eaa160..c7e3ee18ad 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -179,7 +179,10 @@ case_item: [
 ]
 
 binder_constr: [
+| MOVETO term_forall_or_fun "forall" open_binders "," operconstr200
+| MOVETO term_forall_or_fun "fun" open_binders "=>" operconstr200
 | MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
+| MOVETO term_if "if" operconstr200 as_return_type "then" operconstr200 "else" operconstr200
 | MOVETO term_fix "let" "fix" fix_decl "in" operconstr200
 | MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200
 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
@@ -203,8 +206,10 @@ term_let: [
 ]
 
 atomic_constr: [
-(* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
-(* | DELETE string *)
+| MOVETO qualid_annotated global univ_instance
+| MOVETO primitive_notations NUMERAL
+| MOVETO primitive_notations string
+| MOVETO term_evar "_"
 | REPLACE "?" "[" ident "]"
 | WITH "?[" ident "]"
 | MOVETO term_evar "?[" ident "]"
@@ -243,7 +248,21 @@ operconstr100: [
 | MOVETO term_cast operconstr99 ":>"
 ]
 
+constr: [
+| REPLACE "@" global univ_instance
+| WITH "@" qualid_annotated
+| MOVETO term_explicit "@" qualid_annotated
+]
+
 operconstr10: [
+(* Separate this LIST0 in the nonempty and the empty case *)
+(* The empty case is covered by constr *)
+| REPLACE "@" global univ_instance LIST0 operconstr9
+| WITH "@" qualid_annotated LIST1 operconstr9
+| REPLACE operconstr9
+| WITH constr
+| MOVETO term_application operconstr9 LIST1 appl_arg
+| MOVETO term_application "@" qualid_annotated LIST1 operconstr9
 (* fixme: add in as a prodn somewhere *)
 | MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
 | DELETE dangling_pattern_extension_rule
@@ -259,6 +278,7 @@ operconstr1: [
 | WITH    operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *)
 | REPLACE operconstr0 "%" IDENT
 | WITH operconstr0 "%" scope_key
+| MOVETO term_scope operconstr0 "%" scope_key
 | MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
 | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
 ]
@@ -268,6 +288,10 @@ operconstr0: [
 | DELETE "{" binder_constr "}"
 | REPLACE "{|" record_declaration bar_cbrace
 | WITH "{|" LIST0 field_def bar_cbrace
+| MOVETO term_record "{|" LIST0 field_def bar_cbrace
+| MOVETO term_generalizing "`{" operconstr200 "}"
+| MOVETO term_generalizing "`(" operconstr200 ")"
+| MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
 ]
 
 fix_decls: [
@@ -1132,7 +1156,7 @@ assumption_token: [
 | WITH [ "Variable" | "Variables" ]
 ]
 
-all_attrs: [
+attributes: [
 | LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
 
@@ -1696,7 +1720,6 @@ RENAME: [
 | univ_instance univ_annot
 | simple_assum_coe assumpt
 | of_type_with_opt_coercion of_type
-| attribute attr
 | attribute_value attr_value
 | constructor_list_or_record_decl constructors_or_record
 | record_binder_body field_body
@@ -1807,12 +1830,12 @@ control_command: [ ]
 query_command: [ ] (* re-add since previously spliced *)
 
 sentence: [
-| OPT all_attrs command "."
-| OPT all_attrs OPT ( num ":" ) query_command "."
-| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ]
+| OPT attributes command "."
+| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT toplevel_selector ltac_expr [ "." | "..." ]
 | control_command
 ]
 
-vernacular: [
+document: [
 | LIST0 sentence
 ]
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 98f826cd29..6d4c33f7be 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -50,7 +50,7 @@ let default_args = {
   verify = false;
 }
 
-let start_symbols = ["vernacular"]
+let start_symbols = ["document"]
 let tokens = [ "bullet"; "string"; "unicode_id_part"; "unicode_letter" ]
 
 (* translated symbols *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 2a30c03dd2..df4e5a22e3 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -15,10 +15,9 @@ ltac_use_default: [
 ]
 
 term: [
-| "forall" open_binders "," term
-| "fun" open_binders "=>" term
+| term_forall_or_fun
 | term_let
-| "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
+| term_if
 | term_fix
 | term_cofix
 | term100
@@ -30,44 +29,39 @@ term100: [
 ]
 
 term10: [
-| term1 LIST1 arg
-| "@" qualid OPT univ_annot LIST0 term1
-| term1
-]
-
-arg: [
-| "(" ident ":=" term ")"
-| term1
+| term_application
+| one_term
 ]
 
 one_term: [
+| term_explicit
 | term1
-| "@" qualid OPT univ_annot
 ]
 
 term1: [
 | term_projection
-| term0 "%" scope_key
+| term_scope
 | term0
 ]
 
 term0: [
-| qualid OPT univ_annot
+| qualid_annotated
 | sort
-| numeral
-| string
-| "_"
+| primitive_notations
 | term_evar
 | term_match
+| term_record
+| term_generalizing
+| term_ltac
 | "(" term ")"
-| "{|" LIST0 field_def "|}"
-| "`{" term "}"
-| "`(" term ")"
-| "ltac" ":" "(" ltac_expr ")"
 ]
 
-field_def: [
-| qualid LIST0 binder ":=" term
+qualid_annotated: [
+| qualid OPT univ_annot
+]
+
+term_ltac: [
+| "ltac" ":" "(" ltac_expr ")"
 ]
 
 term_projection: [
@@ -75,7 +69,12 @@ term_projection: [
 | term0 ".(" "@" qualid LIST0 ( term1 ) ")"
 ]
 
+term_scope: [
+| term0 "%" scope_key
+]
+
 term_evar: [
+| "_"
 | "?[" ident "]"
 | "?[" "?" ident "]"
 | "?" ident OPT ( "@{" LIST1 ( ident ":=" term ) SEP ";" "}" )
@@ -85,6 +84,25 @@ dangling_pattern_extension_rule: [
 | "@" "?" ident LIST1 ident
 ]
 
+term_application: [
+| term1 LIST1 arg
+| "@" qualid_annotated LIST1 term1
+]
+
+arg: [
+| "(" ident ":=" term ")"
+| term1
+]
+
+term_explicit: [
+| "@" qualid_annotated
+]
+
+primitive_notations: [
+| numeral
+| string
+]
+
 assumption_token: [
 | [ "Axiom" | "Axioms" ]
 | [ "Conjecture" | "Conjectures" ]
@@ -158,14 +176,14 @@ where: [
 | "before" ident
 ]
 
-vernacular: [
+document: [
 | LIST0 sentence
 ]
 
 sentence: [
-| OPT all_attrs command "."
-| OPT all_attrs OPT ( num ":" ) query_command "."
-| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ]
+| OPT attributes command "."
+| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT toplevel_selector ltac_expr [ "." | "..." ]
 | control_command
 ]
 
@@ -178,17 +196,17 @@ query_command: [
 tacticals: [
 ]
 
-all_attrs: [
-| LIST0 ( "#[" LIST0 attr SEP "," "]" ) LIST0 legacy_attr
+attributes: [
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
 
-attr: [
+attribute: [
 | ident OPT attr_value
 ]
 
 attr_value: [
 | "=" string
-| "(" LIST0 attr SEP "," ")"
+| "(" LIST0 attribute SEP "," ")"
 ]
 
 legacy_attr: [
@@ -267,6 +285,10 @@ cofix_body: [
 | ident LIST0 binder OPT ( ":" type ) ":=" term
 ]
 
+term_if: [
+| "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
+]
+
 term_let: [
 | "let" name OPT ( ":" type ) ":=" term "in" term
 | "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
@@ -275,6 +297,11 @@ term_let: [
 | "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term
 ]
 
+term_forall_or_fun: [
+| "forall" open_binders "," term
+| "fun" open_binders "=>" term
+]
+
 open_binders: [
 | LIST1 name ":" term
 | LIST1 binder
@@ -312,6 +339,11 @@ typeclass_constraint: [
 | name ":" OPT "!" term
 ]
 
+term_generalizing: [
+| "`{" term "}"
+| "`(" term ")"
+]
+
 term_cast: [
 | term10 "<:" term
 | term10 "<<:" term
@@ -467,7 +499,7 @@ record_definition: [
 ]
 
 record_field: [
-| LIST0 ( "#[" LIST0 attr SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
 ]
 
 field_body: [
@@ -476,6 +508,14 @@ field_body: [
 | LIST0 binder ":=" term
 ]
 
+term_record: [
+| "{|" LIST0 field_def "|}"
+]
+
+field_def: [
+| qualid LIST0 binder ":=" term
+]
+
 inductive_definition: [
 | OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]