Schemalg-implementation
Implementation of schemalg.
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.
- old is the homonymous input to the event macro
if it has no type;
otherwise, it is the (possibly different) typed value
resulting from processing that input.
- schema is the homonymous input to the event macro.
- list-input is the homonymous input to the event macro.
- oset-input is the homonymous input to the event macro.
- cdr-output is the homonymous input to the event macro.
- tail-output is the homonymous input to the event macro.
- fvar-0-name is the homonymous input to the event macro.
- fvar-1-name is the homonymous input to the event macro.
- fvar-2-name is the homonymous input to the event macro.
- algo-name is the homonymous input to the event macro.
- algo-enable is the homonymous input to the event macro.
- spec-0-name is the homonymous input to the event macro.
- spec-0-enable is the homonymous input to the event macro.
- spec-1-name is the homonymous input to the event macro.
- spec-1-enable is the homonymous input to the event macro.
- spec-2-name is the homonymous input to the event macro.
- spec-2-enable is the homonymous input to the event macro.
- equal-algo-name is the homonymous input to the event macro.
- equal-algo-enable is the homonymous input to the event macro.
- new-name is the homonymous input to the event macro.
- new-enable is the homonymous input to the event macro
if it has no type;
otherwise, it is the (possibly different) typed value
resulting from processing that input.
- old-if-new-name is the homonymous input to the event macro.
- old-if-new-enable is the homonymous input to the event macro
if it has no type;
otherwise, it is the (possibly different) typed value
resulting from processing that input.
- verify-guards is the homonymous input to the event macro
if it has no type;
otherwise, it is the (possibly different) typed value
resulting from processing that input.
- print is the homonymous input to the event macro.
- show-only is the homonymous input to the event macro.
- call is the call of the event macro.
- x-x1...xn is the list of variable symbols (x x1 ... xn)
described in the user documentation.
- x-a1...am is the list of terms (x a1<x1,...,xn> ... am<x1,...,xn>)
described in the user documentation.
- x-z1...zm is the list of variable symbols (x z1 ... zm)
described in the user documentation.
- x is the homonymous variable symbol described in the user documentation.
- y is the variable symbol specified by the :cdr-output input.
- out is a variable symbol used as
the last formal parameter of iorel.
- iorel is the lambda expression
(lambda (x x1 ... xn out) iorel<x,x1,...,xn,out>)
described in the user documentation,
except that the variable y in the user documentation
is replaced with the variable symbol in out.
- ?f is the homonymous function symbol described in the user documentation.
- ?f1...?fp is the list of function symbols ?f1, ..., ?fp
described in the user documentation.
- ?g is the homonymous function symbol described in the user documentation.
- ?g0 is the homonymous function symbol described in the user documentation.
- ?g1 is the homonymous function symbol described in the user documentation.
- ?h is the homonymous function symbol described in the user documentation.
- algo is the function symbol algo[?f1]...[?fp]
described in the user documentation.
- spec1...specq is the list of
function symbols spec1, ..., specq
described in the user documentation.
- spec-0 is the function symbol old-0[?g] or old-0[?g0],
based on whether schema is
:divconq-list-0-1 or :divconq-list-0-1-2,
described in the user documentation.
- spec-1 is the function symbol old-1[?h] or old-1[?g1],
based on whether schema is
:divconq-list-0-1 or :divconq-list-0-1-2,
described in the user documentation.
- equal-algo is the function symbol equal[?f][algo[?f1]...[?fp]]
described in the user documentation.
- new is the homonymous function symbol described in the user documentation.
- old-if-new is the homonymous theorem symbol described in the user documentation.
- names-to-avoid is a cumulative list of names of generated events,
used to ensure the absence of name clashes in the generated events.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
Subtopics
- Schemalg-event-generation
- Event generation performed by schemalg.
- Schemalg-fn
- Check redundancy, process the inputs, and generate the event.
- Schemalg-macro-definition
- Definition of the schemalg macro.
- Schemalg-input-processing
- Input processing performed by schemalg.
