		Search-engine friendly clone of the ACL2 documentation.

Abnf

Deftreeops

Generate grammar-specific operations on trees.

Introduction

The ABNF semantics includes tree matching predicates (e.g. tree-match-element-p) that take the grammar as a parameter. Given a grammar, one can define tree matching predicates that are specialized to the grammar, i.e. that implicitly depend on the grammar.

The ABNF semantics also includes generic operations on trees, generated as part of the tree fixtype. Given a grammar, trees that match certain rule names and other ABNF syntactic entities have a much more restricted structure than generic trees. For instance, given a grammar rule of the form A = B C, a tree matching A always has two subtrees, one matching B and one matching C. Thus, given a grammar, one can define operations on trees that are specialized to the specific rules and structure of the grammar.

This deftreeops macro automates the generation of the aforementioned specialized tree matching predicates and operations, along with theorems about them. Currently we only generate operations (and accompanying theorems) for certain forms of the grammar rules, but we plan to extend this deftreeops macro to generate additional grammar-specific operations on trees, and theorems accompanying them. See the documentation below for details of the current support.

Each successful call of deftreeops adds an entry to a table called abnf::deftreeops-table. With deftreeops, we provide some companion macros to retrieve information from this table. These are documented in the `Companion Macros' section below.

General Form

(deftreeops *grammar*
            :prefix ...  ; no default
            :print  ...  ; default :result
  )

Inputs

*grammar*

Name of the constant that contains the grammar that the generated functions and theorems are specialized to.
This must be a symbol that is a named constant whose value is a grammar, i.e. a value of type rulelist. It could be a grammar introduced by defgrammar.
The grammar must be well-formed and closed.
If there is a previous successful call of deftreeops with the same *grammar* input, this call must be identical to that call, in which case it is redundant. If the calls differ, it is an error.

:prefix — no default

Specifies the prefix for the specialized tree operations.
It must be a symbol in a package different from the Common Lisp package and the keyword package.
A good choice for this symbol could be ::cst, where is the package of the application at hand and where cst stands for CST (Concrete Syntax Tree). If the application involves multiple grammars for different languages, a good choice for this symbol could be ::<lang>-cst, where <lang> indicates the language that the grammar refers to.
In the rest of this documentation page, let <prefix> be this symbol.

:print — default :result

Specifies what is printed on the screen.
It must be one of the following:
:error, to print only error output (if any).
:result, to print, besides any error output, also the results of deftreeops. This is the default value of the :print input. Since the results may consist of a large number of events, only their names are printed; the event themselves can be inspected via the macro deftreeops-show-event, described in the `Companion Macros' section below.
:info, to print, besides any error output and the results, also some additional information about the internal operation of deftreeops (Currently there is no difference between the :info and the :result outputs, but we plan to add :info outputs.).
:all, to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events. This could be a lot of output.
The errors are printed as error output. The results and the additional information are printed as comment output. The ACL2 output enabled by :print :all may consist of output of various kinds.
If :print is :error or :result or :info, deftreeops suppresses all kinds of outputs (via with-output) except for error and comment output. Otherwise, deftreeops does not suppress any output. However, the actual output depends on which outputs are enabled or not prior to the call of deftreeops, including any with-output with which the user may wrap the call of deftreeops.

Generated Events

The events are put in a defsection whose name is *grammar*-tree-operations (i.e. the symbol obtained by adding -tree-operations to the name of the constant whose value is the grammar), and whose only parent is the *grammar* symbol. That is, the generated section is a sub-topic of the XDOC topic for the grammar.

<prefix>-matchp
<prefix>-list-elem-matchp
<prefix>-list-rep-matchp
<prefix>-list-list-conc-matchp
<prefix>-list-list-alt-matchp

Tree matching predicates, specialized to *grammar*. The predicates are put in the same package as <prefix>.
Each predicate takes two arguments:
A tree (for the first one), or a list of trees (for the second and third one), or a list of lists of trees (for the fourth and fifth one).
An ACL2 string, which must be an ABNF concrete syntax representation of an element (for the first and second one), or a repetition (for the third one), or a concatenation (for the fourth one), or an alternation (for the fifth one).
Each predicate holds iff the (list of (list(s) of)) tree(s) is terminated and matches the element or repetition or concatenation or alternation. While in the semantics it makes sense to include non-terminated trees as potentially matching, for a specific grammar it normally makes sense to consider only terminated trees: this motivates the extra condition.
These generated predicates are actually macros, which use (subroutines of) the verified grammar parser to parse the ACL2 strings passed as second arguments into their ABNF abstract syntactic representation, and then expand to calls of the appropriate generic tree matching predicates in the semantics, passing the grammar as argument to them; the dependency on the grammar is implicit in the generated predicates. Note that the parsing of the strings happens at macro expansion time (i.e. at compile time), not at predicate call time (i.e. at run time).
There are some generated internal intermediate predicates that these macros expand into calls of, and it is these intermediate predicates that call the generic tree matching predicates from the semantics. These intermediate predicates are actual ACL2 functions, whose names are identical to the macros but with $ at the end. Macro aliases are also generated that link the macro names to the function names: this way, the predicates can be opened (in proofs) via their macro names.

<prefix>-<rulename>-nonleaf

For each rule name defined in the grammar: a theorem saying that a tree that matches the rule name is a non-leaf tree.

<prefix>-<rulename>-rulename

For each rule name defined in the grammar: a theorem saying that a tree that matches the rule name has exactly that rule name.

<prefix>-<rulename>-branches-match-alt

For each rule name defined in the grammar: a theorem saying that if a tree matches the rule name then its branches match the alternation that defines the rule name.

<prefix>-<rulename>-concs

For each rule name defined in the grammar: a theorem saying that if a list of lists of trees matches the alternation that defines the rule name then the list of lists of trees matches one of the concatenations in the alternation. This is a disjunctive theorem, unless the alternation consists of just one concatenation.

<prefix>-<rulename>-conc-equivs

For each rule name defined in the grammar by an alternation of two or more concatenations satisfying one of the conditions listed below, a theorem stating equivalences between (i) the branches (of a tree matching the rule name) matching each concatenation and (ii) some term over the branches that discriminates among the concatenations that define the rule name; there is an equivalence for each concatenation, and the theorem consists of the conjunction of the equivalences. This theorem is a conjunction of equivalences, one for each concatenation that defines the rule name.
The aforementioned conditions on the alternation of two or more concatenations are any of the following (if neither are satisfied, this theorem is not generated):
The alternation consists of two or more concatenations each of which is a singleton, each consisting of a repetition with range 1 whose element is a rule name.
The alternation consists of exactly two concatenations, one of which is a singleton of a repetition with range 1 whose element is a character value notation, and the other is a singleton of a repetition with range 1 whose element is a rule name.

<prefix>-<rulename>-conc?

For each rule name defined in the grammar by an alternation of two or more concatenations: a function that, given a tree matching the rule name, returns a positive integer indicating the concatenation matched by the subtrees, in the order in which the concatenation appears in the alternation, numbered starting from 1 for the first concatenation. If a rule name is defined by multiple rules (the first one non-incremental, the other ones incremental), the order of the concatenations indicated by the integer returned by this function is lexicographic, based first on the order of the rules and then on the order of the concatenations within each rule. The generated function is accompanied by the following theorems:
<prefix>-<rulename>-conc?-possibilities, which asserts that the result of the function is one of the numbers 1, ..., n, where n is the number of concatenations that form the alternation that defines the rule name. This is a disjunctive theorem.
<prefix>-<rulename>-conc?--iff-match-conc, for each concatenation (numbered starting from 1) in the alternation that defines the rule name, which asserts that the function returns iff the subtrees match the concatenation.
fty::deffixequiv theorems for the function.

<prefix>-<rulename>-conc

For each rule name defined in the grammar by an alternation of one concatenation: a function that, given a tree matching the rule name, returns the list of lists of subtrees of the tree. The generated function is accompanied by the following theorems:
<prefix>-<rulename>-conc-match, which asserts that the result of the function matches the concatenation.
fty::deffixequiv theorems for the function.

<prefix>-<rulename>-conc

For each rule name defined in the grammar by an alternation of two or more concatenations, such that each concatenation is a singleton of a singleton repetition of a rule name element, and for each concatenation (numbered starting from 1) in the alternation: a function that, given a tree matching the rule name whose subtrees match the concatenation (expressed via <prefix>-<rulename>-conc? above), returns the list of lists of subtrees of the tree. The generated function is accompanied by the following theorems:
<prefix>-<rulename>-conc-match, which asserts that the result of the function matches the concatenation .
fty::deffixequiv theorems for the function.

<prefix>-<rulename>-conc-matching

For each rule name defined in the grammar by an alternation of one concatenation, such that the concatenation consists of one repetition: a theorem saying that if a list of lists of trees matches that concatenation then the list of lists of trees has the same length as the concatenation and each list of trees matches the corresponding repetition of the concatenation.

<prefix>-<rulename>-conc-matching

For each rule name defined in the grammar by an alternation of two or more concatenations, and for each concatenation (numbered starting from 1) in the alternation, such that the concatenation consists of one repetition: a theorem saying that if a list of lists of trees matches that concatenation then the list of lists of trees has the same length as the concatenation and each list of trees matches the corresponding repetition of the concatenation.

<prefix>-<rulename>-conc-rep

For each rule name defined in the grammar by an alternation of one concatenation, such that the concatenation consists of one repetition: a function that, given a tree matching the rule name, returns the list of trees corresponding to the repetition. The generated function is accompanied by the following theorems:
<prefix>-<rulename>-conc-rep-match, which asserts that the result of the function matches the repetition.
fty::deffixequiv theorems for the function.

<prefix>-<rulename>-conc-rep

For each rule name defined in the grammar by an alternation of two or more concatenations, and for each concatenation (numbered starting from 1) in the alternation, such that the concatenation consists of one repetition: a function that, given a tree matching the rule name, returns the list of trees corresponding to the repetition. The generated function is accompanied by the following theorems:
<prefix>-<rulename>-conc-rep-match, which asserts that the result of the function matches the repetition.
fty::deffixequiv theorems for the function.

<prefix>-<rulename>-conc-rep-matching

For each rule name defined in the grammar by an alternation of one concatenation, such that the concatenation consists of one repetition, such that the repetition has a range of 1: a theorem saying that if a list of trees matches that repetition then the list of trees has a length within the range of the repetition and each tree matches the element of the repetition.

<prefix>-<rulename>-conc-rep-matching

For each rule name defined in the grammar by an alternation of two or more concatenations, and for each concatenation (numbered starting from 1) in the alternation that defines the rule name, such that the concatenation consists of one repetition, such that the repetition has a range of 1: a theorem saying that if a list of trees matches that repetition then the list of trees has a length within the range of the repetition and each tree matches the element of the repetition.

<prefix>-<rulename>-conc-rep-elem

For each rule name defined in the grammar by an alternation of one concatenation, such that the concatenation consists of one repetition, such that the repetition has a range of 1: a function that, given a tree matching the rule name, returns the tree corresponding to the element of the repetition. The generated function is accompanied by the following theorems:
<prefix>-<rulename>-conc-rep-elem-match, which asserts that the result of the function matches the rule name of the element.
fty::deffixequiv theorems for the function.

<prefix>-<rulename>-conc-rep-elem

For each rule name defined in the grammar by an alternation of two or more concatenations, and for each concatenation (numbered starting from 1) in the alternation, such that the concatenation consists of one repetition, such that the repetition has a range of 1, and such that the element of the repetition is a rule name: a function that, given a tree matching the rule name, returns the tree corresponding to the element of the repetition. The generated function is accompanied by the following theorems:
<prefix>-<rulename>-conc-rep-elem-match, which asserts that the result of the function matches the rule name of the element.
fty::deffixequiv theorems for the function.

<prefix>-%<min>-<max>-nat

For each numeric range notation that appears in the grammar, of the form %<min>-<max> where is d or x or b (the base), <min> is the minimum of the range (in base ), and <max> is the maximum of the range (in base ), a function that, given a tree matching the numeric range, returns the natural number that is the (unique) leaf of the tree. In the name of this generated function, the <min> and <max> part are expressed in digits in the base indicated by , with unnecessary leading zeros. The generated function is accompanied by the following theorem:
<prefix>-%<min>-<max>-nat-bounds, which asserts that the natural number returned by the function has <min> as lower bound and <max> as upper bound. This theorem is generated as a linear rule.
fty::deffixequiv theorems for the function.

For each character value notation that appears in the grammar, of the form "<chars" or %i"<chars>" or %s"<chars>" where <chars> is a sequence of one or more characters, a theorem saying that a tree that matches the character values notation is a terminal leaf tree.

Companion Macros

Each successful call of deftreeops adds an entry to the abnf::deftreeops-table table. The table is indexed by the *grammar* inputs of the calls. Each entry stores information calculated from the grammar, including all the events generated. See deftreeops-table in the implementation for details.

ACL2 already provides facilities to inspect table and their entries. We provide a macro

(deftreeops-show-info *grammar*)

which prints the value in the table associated to *grammar*. Note that this can be a large value.

We also provide a macro

(deftreeops-show-event *grammar* name)

which prints the event form with name name generated by a call of deftreeops on *grammar*. This may be generally more useful to a user than the previous macro.

Subtopics

Deftreeops-implementation: Implementation of deftreeops.
Deftreeops-show-event: Show the event with a given name from the deftreeops table associated to a given grammar constant name.
Deftreeops-show-info: Show the information from the deftreeops table associated to a given grammar constant name.