Deftreeops-implementation
Implementation of deftreeops.
The implementation functions have arguments and results
consistently named as follows
(unless otherwise stated, explicitly or implicitly,
in the functions):
- state is the ACL2 state.
- wrld is the ACL2 world.
- ctx is the context used for errors.
- grammar is the homonymous input to the event macro.
- prefix is the homonymous input to the event macro.
- print is the homonymous input to the event macro.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
The generation of the functions and theorems happens in two passes:
- In the first pass, we go through all the rules of the grammar
and generate
a deftreeops-rulename-info-alist,
a deftreeops-numrange-info-alist, and
a deftreeops-charval-info-alist,
which mainly contain information about
the names of the functions and theorems to be generated,
along with some additional information.
- In the second pass, we go through the alists built in the first pass,
and we generate all the events for the functions and theorems.
The names and additional information in the alists
provide the means for the events to reference each other as needed.
Care is taken to generate the events so that
there are no forward references, as required in ACL2.
The generated events are returned as separate sequences,
in order to put analogous events next to each other.
The alists of information created in the first pass
are also stored in the deftreeops table,
via an event generated along with the functions and theorems.
The table also stores an alist of the generated events as values
with the names of the events as keys.
This way, the information about the generated functions and theorems
can be easily accessed, interactively or programmatically.
In the documentation below,
we say `defining alternation of a rule name'
instead of `defining alternation of a rule'.
In ABNF, a well-formed grammar may have more than one rule for the same rule name,
with the rules after the first one being incremental ones.
Thus, by `defining alternation of a rule name' we mean
the alternation consisting of all the concatenations in
the alternations in the rules for the rule name,
in the order in which they appear in the grammar,
as returned by lookup-rulename.
Subtopics
- Deftreeops-event-generation
- Event generation performed by deftreeops.
- Deftreeops-info
- Information about the events generated by deftreeops.
- Deftreeops-process-inputs-and-gen-everything
- Process the inputs and generate the events.
- Deftreeops-fn
- Event expansion of deftreeops.
- Deftreeops-table
- Table of deftreeops calls.
- Deftreeops-input-processing
- Input processing performed by deftreeops.
- Deftreeops-macro-definition
- Definition of deftreeops.
