# Grammar extraction tool for documentation

`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it
into `.rst` files.  The tool inserts `prodn` directives for  grammar productions.
It also updates `tacn` and `cmd` directives when they can be unambiguously matched to
productions of the grammar (in practice, that's probably almost always).
`tacv` and `cmdv` directives are not updated because matching them appears to require
human judgement.  `doc_grammar` generates a few files that may be useful to
developers and documentors.

The mlg grammars present several challenges to generating an accurate grammar
for documentation purposes:

* The 30+ mlg files don't define an overall order in which nonterminals should
  appear in a complete grammar.

* Even within a single mlg file, nonterminals and productions are often given
  in an order that's much different from what a reader of the documentation would
  expect.  In a small number of cases, changing the order in the mlg would change
  how some inputs are parsed, in particular when the order determines how to distinguish
  otherwise ambiguous inputs.

  Strictly speaking, that means our grammar is not a context free grammar even though
  we gloss over that distinction in the documentation.

* For a few nonterminals, some productions are only available if certain plugins
  are activated (e.g. SSR).  Readers should be informed about these.

* Some limited parts of the grammar are defined in OCaml, including lookahead symbols
  like `test_bracket_ident` and references to nonterminals in other files using
  qualified names such as `Prim.ident`.  A few symbols are defined multiple times,
  such as `scope` and `orient`.

## What the tool does

1.  The tool reads all the `mlg` files and generates `fullGrammar`, which includes
    all the grammar without the actions for each production or the OCaml code.  This
    file is provided as a convenience to make it easier to examine the (mostly)
    unprocessed grammar of the mlg files with less clutter.  This step includes two
    transformations that rename some nonterminal symbols:

    First, nonterminals that use levels (`"5" RIGHTA` below) are modified, for example:

    ```
    ltac_expr:
      [ "5" RIGHTA
        [ te = binder_tactic -> { te } ]
      [ "4"   ...
    ```

    becomes

    ```
    tactic_expr5: [
    | binder_tactic
    | tactic_expr4
    ]
    ```

    Second, nonterminals that are local to an .mlg will be renamed, if necessary, to
    make them unique.  For example, `strategy_level` is defined as a local nonterminal
    in both `g_prim.mlg` and in `extraargs.mlg`.  The nonterminal defined in the former
    remains `strategy_level` because it happens to be processed before the latter,
    in which the nonterminal is renamed to `EXTRAARGS_strategy_level` to make the local
    symbol unique.

    Nonterminals listed after `GLOBAL:` are global; otherwise they are local.

    References to renamed symbols are updated with the modified names.

2.  The tool applies grammar editing operations specified by `common.edit_mlg` to
    generate `editedGrammar`.

3. `orderedGrammar` gives the desired order for nonterminals and individual productions
    in the documented grammar.  Developers should edit this file only to reorder lines.
    `doc_grammar` updates `orderedGrammar` so it has the same set of nonterminals and productions
    as `editedGrammar` while retaining the previous ordering.  Since the position of
    new or renamed nonterminals is unspecified, they tend to show up in the wrong
    place in `orderedGrammar`, therefore users should review the output and make
    appropriate adjustments to the order.

    The update process removes manually-added comments from `orderedGrammar` while
    automatically-generated comments will be regenerated.

4.  The tool updates the `.rst` files.  Comments in the form
    `.. insertprodn <first nt> <last nt>` indicate inserting the productions for a
    range of nonterminals.  `.. cmd::` and `.. tacn::` directives are updated using
    prefixes in the form `[a-zA-Z0-9_ ]+` from the directive and the
    grammar.  If there is unique match in the grammar, the directive is updated, if needed.
    Multiple matches or no match gives an error message.

5.  For reference, the tool generates `prodnGrammar`, which has the entire grammar in the form of `prodns`.

6.  If requested by command-line arguments, the tool generates `prodnCommands`
    (for commands) and `prodnTactics` (for tactics).
    The former lists all commands that are under `command` in `orderedGrammar` and
    compares it to the `:cmd:` and `:cmdv:` given in the rst files.  The latter
    lists all tactics that are under `simple_tactic` in the grammar and compares it
    to the `:tacn:` and `:tacv:`.  The tags at the beginning of each line mean:

    - (no tag) - the grammar and the rst match exactly and uniquely
    - `-` - a grammar production that can't be matched to an rst file entry
    - `+` - an rst entry that doesn't match a grammar production
    - `v` - the rst entry is a `:cmdv:` or `:tacv:`
    - `?` - the match between the grammar and the rst files is not unique

## How to use the tool

* `make doc_gram` updates `fullGrammar`.

* `make doc_gram_verify` verifies that `fullGrammar`, `orderedGrammar` and `*.rst`
  are consistent with the `.mlg` files.  This is for use by CI.

* `make doc_gram_rsts` updates the `*Grammar` and `.rst` files.

* `make doc_gram_rsts DOCGRAMWARN=1` will additionally print warnings.

Changes to `fullGrammar`, `orderedGrammar` and the `.rsts` should be checked in to git.
The `prodn*` and other `*Grammar` files should not.

### Command line arguments

The executable takes a list of `.mlg` and `.rst` files as arguments.  The tool
inserts the grammar into the `.rsts` as specified by comments in those files.
The order of the `.mlg` files affects the order of nonterminals and productions in
`fullGrammar`.  The order doesn't matter for the `.rst` files.

Specifying the `-verify` command line argument avoids updating any of the files,
but verifies that the current files are consistent.  This setting is meant for
use in CI; it will be up to each developer to include the changes to `*Grammar` and
the `.rst` files in their PRs when they've changed the grammar.

Other command line arguments:

* `-check-tacs` causes generation of `prodnTactics`

* `-check-cmds` causes generation of `prodnCommands`

* `-no-warn` suppresses printing of some warning messages

* `-no-update` puts updates to `fullGrammar` and `orderedGrammar` into new files named
  `*.new`, leaving the originals unmodified.  For use in Dune.

* `-short` limits processing to updating/verifying only the `fullGrammar` file

* `-verbose` prints more messages about the grammar

* `-verify` described above

### Grammar editing scripts

The grammar editing script `common.edit_mlg` is similar in format to `.mlg` files but stripped
of all OCaml features.  This is an easy way to include productions to match or add without
writing another parser.  The `DOC_GRAMMAR` token at the beginning of each file
signals the use of the streamlined syntax.

The edit file has a series of items in the form of productions.  Items are applied
in the order they appear.  There are two types of editing operations:

* Global edits - edit rules that apply to the entire grammar in a single operation.
  These are identified by using specific reserved names as the non-terminal name.

* Local edits - edit rules that apply to the productions of a single non-terminal.
  The rule is a local edit if the non-terminal name isn't reserved.  Individual
  productions within a local edit that begin with a different set of reserved names
  edit existing productions.  For  example `binders: [ | DELETE Pcoq.Constr.binders ]`
  deletes the production `binders: [ | Pcoq.Constr.binders]`

Productions that don't begin with a reserved name are added to the grammar,
such as `empty: [ | ]`, which adds a new non-terminal `empty` with an
empty production on the right-hand side.

Another example: `LEFTQMARK: [ | "?" ]` is a local edit that treats `LEFTQMARK` as
the name of a non-terminal and adds a production for it.  (We know that LEFTQMARK
is a token but doc_grammar does not.)  `SPLICE: [ | LEFTQMARK ]` requests replacing all
uses of `LEFTQMARK` anywhere in the grammar with its productions and removing the
non-terminal.  The combined effect of these two is to replace all uses of
`LEFTQMARK` with `"?"`.

Here are the current operations.  They are likely to be refined as we learn
what operations are most useful while we update the mlg files and documentation:

### Global edits

`DELETE` - deletes the specified non-terminals anywhere in the grammar.  Each
should appear as a separate production.  Useful for removing non-terminals that
only do lookahead that shouldn't be in the documentation.

`RENAME` - each production specifies an (old name, new name) pair of
non-terminals to rename.

`SPLICE` - requests replacing all uses of the nonterminals anywhere in the
grammar with its productions and removing the non-terminal. Each should appear
as a separate production.  (Doesn't work recursively; splicing for both
`A: [ | B ]` and `B: [ | C ]` must be done in separate SPLICE operations.)

`OPTINREF` - applies the local `OPTINREF` edit to every nonterminal

### Local edits

`DELETE <production>` - removes the specified production from the grammar

`EDIT <production>` - modifies the specified production using the following tags
that appear in the specified production:

* `USE_NT <name>` LIST* - extracts LIST* as new nonterminal with the specified
  new non-terminal name

* `ADD_OPT <grammar symbol>` - looks for a production that matches the specified
  production **without** `<grammar_symbol>`.  If found, both productions are
  replaced with single production with `OPT <grammar_symbol>`

  The current version handles a single USE_NT or ADD_OPT per EDIT.  These symbols
  may appear in the middle of the production given in the EDIT.

`APPENDALL <symbols>` - inserts <symbols> at the end of every production in
<edited_nt>.

`INSERTALL <symbols>` - inserts <symbols> at the beginning of every production in
<edited_nt>.

`REPLACE` - (2 sequential productions) - removes `<oldprod>` and
  inserts `<newprod>` in its place.

```
| REPLACE <oldprod>
| WITH <newprod>
```

`COPYALL <destination>` - creates a new nonterminal `<destination>` and copies
all the productions in the nonterminal to `<destination>`.

`MOVETO <destination> <production>` - moves the production to `<destination>` and,
 if needed, creates a new production <edited_nt> -> \<destination>.

`MOVEALLBUT <destination>` - moves all the productions in the nonterminal to `<destination>`
*except* for the productions following the `MOVEALLBUT` production in the edit script
(terminated only by the closing `]`).

`OPTINREF` - verifies that <edited_nt> has an empty production.  If so, it removes
the empty production and replaces all references to <edited_nt> throughout the
grammar with `OPT <edited_nt>`

`PRINT` <nonterminal> - prints the nonterminal definition at that point in
  applying the edits.  Most useful when the edits get a bit complicated to follow.

`(any other nonterminal name)` - adds a new production (and possibly a new nonterminal)
to the grammar.

### `.rst` file updates

`doc_grammar` updates `.rst` files where it sees the following 3 lines

```
.. insertprodn <start> <end>

.. prodn::
```

The end of the existing `prodn` is recognized by a blank line.

### Tagging productions

`doc_grammar` tags the origin of productions from plugins that aren't automatically
loaded.  In grammar files, they appear as `(* XXX plugin *)`.  In rsts, productions
generated by `.. insertprodn` will include where relevant three spaces as (a delimiter)
and a tag name after each production, which Sphinx will show on the far right-hand side
of the production.

The origin of a production can be specified explicitly in `common.edit_mlg` with the
`TAG name` appearing at the end of a production.  `name` must be in quotes if it
contains whitespace characters.  Some edit operations preserve the
tags, but others, such as `REPLACE ... WITH ...` do not.

A mapping from filenames to tags (e.g. "g_ltac2.mlg" is "Ltac2") is hard-coded as is
filtering to avoid showing tags for, say, Ltac2 productions from appearing on every
production in that chapter.

If desired, this mechanism could be extended to tag certain productions as deprecated,
perhaps in conjunction with a coqpp change.