		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. This deftreeops macro automates the generation of these specialized tree matching predicates.

In addition, this deftreeops macro also generates theorems about trees that satisfy the generated grammar-specific matching predicates.

We plan to extend this deftreeops macro to generate additional grammar-specific operations on trees.

General Form

(deftreeops *grammar*
            :prefix ...
  )

Inputs

*grammar*

Name of the constant that contains the grammar that the tree operations 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.

: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 p::cst, where p is the package of the application at hand and where cst stands for CST (Concrete Syntax Tree). If the application involves multiple gramamrs for different languages, a good choice for this symbol could be p::lang-cst, where lang indicates the language that the grammar refers to.
In the rest of this documentation page, let <prefix> be this symbol.

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 meant to be 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 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>-nonleaf-when-<rulename>

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-when-<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>-branches-match-alt-when-<rulename>

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>-alternatives-when-<rulename>

For each rule name defined in the grammar, a theorem saying that if a list of list of trees matches the alternation that defines the rule name then the list of list of trees matches one of the alternatives (each of which is a concatenation.

<prefix>-match-alt<i>-<rulename>

For each rule name defined in the grammar, and for each alternative <i> (starting from 1) that defines the rule name, a theorem saying that if a list of list of trees matches that alternative (which is a concatenation) then the list of list of trees has the same length as the concatenation and each list of trees matches the corresponding repetition of the concatenation. For now we only generate this theorem when the alternative is a singleton concatenation.

<prefix>-match-alt<i>-rep<j>-<rulename>

For each rule name defined in the grammar, for each alternative <i> (starting from 1) that defines the rule name, and for each repetition <j> (starting from 1) of that alternative, 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. For now we only generate this theorem when the repetition has a range of 1.

Subtopics

Deftreeops-implementation: Implementation of deftreeops.