		Search-engine friendly clone of the ACL2 documentation.

Abnf

Defgrammar

Build an ACL2 representation of an ABNF grammar from a file.

Introduction

This macro calls the verified grammar parser on the specified file, applies the abstractor on the resulting concrete syntax tree of the grammar to obtain an abstract syntax tree of the grammar, and introduces a named constant for this abstract syntax tree. This provides an ACL2 representation of the grammar, which has a formal semantics and which is amenable to operations, parser generation, etc.

Besides introducing the named constant, this macro can also (attempt to) prove certain properties of the grammar, under user control.

This macro also generates an XDOC topic for the named constant, which includes any generated events.

Currently the implementation of this macro does not perform very thorough input validation. This will be improved in the future.

General Form

(defgrammar *name*
            :file ...
            :untranslate ...
            :well-formed ...
            :closed ...
            :parents ...
            :short ...
            :long ...
  ///
  <other events>
  )

Inputs

*name*

Name of the named constant introduced by this macro.
It must be a valid constant name.
This is defined as the abstract syntax tree of the grammar read from the file specified by the :file input. See the `Generated Events' section for details.

:file — no default

Path of the file that contains the grammar.
This should be normally a file with extension .abnf, which for example is recognized and syntax-highlighted by GitHub, but this extension is not a requirement. The extension (whether .abnf or not) must be specified.
The lines in the file must be terminated by a carriage return and line feed, as required by the ABNF grammar of ABNF. On Unix systems (e.g. Linux and macOS), this can be accomplished by writing the file in Emacs, setting the buffer's end-of-line to carriage return and line feed by calling set-buffer-file-coding-system with dos, and saving the file. If the file is under a version control system like git, it should be forced to be treated as a text file with CRLF end-of-line (e.g. see [books]/kestrel/abnf/notation/.gitattributes), to avoid turning carriage returns and line feeds into just line feeds across Windows and Unix platforms.
This must be an ACL2 string that is a file path. The path may be absolute, or relative to the connected book directory.

:untranslate — default nil

Specifies whether the constant should be untranslated in output.
It must be one of the following:
t, to untranslate the constant in output. In this case, defgrammar generates and add-const-to-untranslate-preprocess event, which modifies ACL2's untranslation to ``shrink'' the quoted value of the named constant introduced by defgrammar into the name of the constant. As the abstract syntax tree of a grammar may be relatively large, this keeps the ACL2 output more readable and efficient to print in Emacs.
nil, to not untranslate the constant in output. In this case, defgrammar does not generate any add-const-to-untranslate-preprocess event, and ACL2's untranslation is unmodified.
It is normally advisable to untranslate the constant in output.

:well-formed — default nil

Specifies whether defgrammar should generate a theorem saying that the grammar is well-formed.
It must be one of the following:
t, to generate the theorem.
nil, to not generate the theorem.
See the `Generated Events' section for the details of this theorem.
It is normally expected for a grammar to be well-formed.

:closed — default nil

Specifies whether defgrammar should generate a theorem saying that the grammar is closed.
It must be one of the following:
t, to generate the theorem.
nil, to not generate the theorem.
See the `Generated Events' section for the details of this theorem.
A grammar may or may not be closed: it could a component of a larger grammar, which is closed even though not all of its components are

:parents
:short
:long

These, if present, are added to the XDOC topic generated by defgrammar.
These are evaluated by defgrammar, making it possible to use XDOC constructors.

<other-events>

Optionally, the defgrammar can include other events preceded by ///, which must follow all the above inputs.

Generated Events

*name*

The named constant.
This uses make-event to call parse-grammar-from-file and then abstract-rulelist, obtaining a value that is used as a quoted constant to define the named constant.

The add-const-to-untranslate-preprocess event.

This is generated iff the :untranslate input is t.

rulelist-wfp-of-*name*

The theorem asserting that the grammar is well-formed:
(rulelist-wfp *name*)
This is generated iff the :well-formed input is t.

rulelist-closedp-of-*name*

The theorem asserting that the grammar is closed:
(rulelist-closedp *name*)
This is generated iff the :closed input is t.

<other-events>

If specified, these are put after all the above events.

All these events are inside a defsection whose name is *name* and whose parent list, short string, and long string are the ones specified in the respective inputs.

Redundancy

A call of defgrammar is redundant if and only if it is identical to a previous successful call of defgrammar with the exact same arguments.

Subtopics

Defgrammar-implementation: Implementation of defgrammar.