Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg files and insert it into .rst files

Ack-by: Zimmi48
Ack-by: gares
Ack-by: ppedrot

1 files changed, 220 insertions, 0 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
new file mode 100644
index 0000000000..ea94e21ff3
--- /dev/null
+++ b/doc/tools/docgram/common.edit_mlg
@@ -0,0 +1,220 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Defines additional productions and edits for use in documentation.  Not compiled into Coq *)
+
+DOC_GRAMMAR
+
+(* additional nts to be spliced *)
+
+LEFTQMARK: [
+| "?"
+]
+
+SPLICE: [
+| LEFTQMARK
+]
+
+hyp: [
+| var
+]
+
+tactic_then_gen: [
+| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
+| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
+]
+
+SPLICE: [
+| hyp
+| identref
+| pattern_ident (* depends on previous LEFTQMARK splice todo: improve *)
+| constr_eval  (* splices as multiple prods *)
+| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
+| Prim.name
+| ltac_selector
+| Constr.ident
+| tactic_then_locality  (* todo: cleanup *)
+| attribute_list
+]
+
+RENAME: [
+  (* map missing names for rhs *)
+| _binders binders
+| Constr.constr term
+| Constr.constr_pattern constr_pattern
+| Constr.global global
+| Constr.lconstr lconstr
+| Constr.lconstr_pattern lconstr_pattern
+| G_vernac.query_command query_command
+| G_vernac.section_subset_expr section_subset_expr
+| nonsimple_intropattern intropattern
+| Pltac.tactic tactic
+| Pltac.tactic_expr ltac_expr
+| Prim.ident ident
+| Prim.reference reference
+| Pvernac.Vernac_.main_entry vernac_control
+| Tactic.tactic tactic
+| tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic_expr5 ltac_expr
+| tactic_expr4 ltac_expr4
+| tactic_expr3 ltac_expr3
+| tactic_expr2 ltac_expr2
+| tactic_expr1 ltac_expr1
+| tactic_expr0 ltac_expr0
+
+  (* elementary renaming/OCaml-defined productions *)
+| clause clause_dft_concl
+| in_clause' in_clause
+| l_constr lconstr  (* todo: should delete the production *)
+
+  (* SSR *)
+| G_vernac.def_body def_body
+| Pcoq.Constr.constr term
+| Prim.by_notation by_notation
+| Prim.identref ident
+| Prim.natural natural
+| Vernac.rec_definition rec_definition
+
+  (* rename on lhs *)
+| intropatterns intropattern_list_opt
+| Constr.closed_binder closed_binder
+
+  (* historical name *)
+| constr term
+]
+
+DELETE: [
+| check_for_coloneq
+| impl_ident_head
+| local_test_lpar_id_colon
+| lookup_at_as_comma
+| only_starredidentrefs
+| test_bracket_ident
+| test_lpar_id_coloneq
+| test_lpar_id_rpar
+| test_lpar_idnum_coloneq
+| test_show_goal
+
+  (* SSR *)
+(* | ssr_null_entry *)
+| ssrtermkind  (* todo: rename as "test..." *)
+| term_annotation  (* todo: rename as "test..." *)
+| test_idcomma
+| test_nohidden
+| test_not_ssrslashnum
+| test_ssr_rw_syntax
+| test_ssreqid
+| test_ssrfwdid
+| test_ssrseqvar
+| test_ssrslashnum00
+| test_ssrslashnum01
+| test_ssrslashnum10
+| test_ssrslashnum11
+| test_ident_no_do
+| ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
+| ssrseqdir
+]
+
+ident: [
+| DELETE IDENT ssr_null_entry
+]
+
+natural: [
+| DELETE _natural
+]
+
+
+  (* added productions *)
+
+empty: [  (* todo: (bug) this is getting converted to empty -> empty *)
+|
+]
+
+lpar_id_coloneq: [
+| "(" IDENT; ":="
+]
+
+name_colon: [
+| IDENT; ":"
+| "_" ":"  (* todo: should "_" be a keyword or an identifier? *)
+]
+
+int: [ (* todo: probably should be NUMERAL *)
+| integer
+]
+
+command_entry: [
+| noedit_mode
+]
+
+binders: [
+| DELETE Pcoq.Constr.binders  (* todo: not sure why there are 2 "binders:" *)
+]
+
+(* edits to simplify *)
+
+ltac_expr1: [
+| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
+]
+
+match_context_list: [
+| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
+]
+
+match_hyps: [
+| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern
+| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern
+| DELETE name ":=" match_pattern
+]
+
+match_list: [
+| EDIT ADD_OPT "|" LIST1 match_rule SEP "|"
+]
+
+
+selector_body: [
+| REPLACE range_selector_or_nth  (* depends on whether range_selector_or_nth is deleted first *)
+| WITH LIST1 range_selector SEP ","
+]
+
+range_selector_or_nth: [
+| DELETENT
+]
+
+simple_tactic: [
+| DELETE "intros"
+| REPLACE "intros" ne_intropatterns
+| WITH "intros" intropattern_list_opt
+| DELETE "eintros"
+| REPLACE "eintros" ne_intropatterns
+| WITH "eintros" intropattern_list_opt
+]
+
+intropattern_list_opt: [
+| DELETE LIST0 intropattern
+| intropattern_list_opt intropattern
+| empty
+]
+
+
+ne_intropatterns: [
+| DELETENT  (* todo: don't use DELETENT for this *)
+]
+
+
+or_and_intropattern: [
+| DELETE "()"
+| DELETE "(" simple_intropattern ")"
+| REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
+|   WITH  "(" LIST0 simple_intropattern SEP "," ")"
+| EDIT "[" USE_NT intropattern_or LIST1 intropattern_list_opt SEP "|" "]"
+]