Solve-implementation
Implementation of solve.
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.
- method is the homonymous input to the event macro.
- method-rules is the homonymous input to the event macro.
- solution-name is the homonymous input to the event macro.
- solution-enable is the homonymous input to the event macro.
- solution-guard is the homonymous input to the event macro.
- solution-guard-hints is the homonymous input to the event macro.
- solution-body is the homonymous input to the event macro.
- solution-hints 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.
- ?f is the homonymous function symbol described in the user documentation.
- x1...xn is the list of variable symbols x1, ..., xn
described in the user documentation.
- matrix is the term matrix<(?f x1 ... xn)>
described in the user documentation.
- f is the homonymous function symbol described in the user documentation.
- f-existsp is a boolean indicating whether f already exists
(as opposed to being generated).
- f-body is the obtained body of the solution function f,
when this function is generated.
- solution-theorem is the name of the locally generated theorem
asserting the correctness of the solution.
- 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
- Solve-event-generation
- Event generation performed by solve.
- Solve-fn
- Check redundancy, process the inputs, and generate the event.
- Solve-input-processing
- Input processing performed by solve.
- Solve-macro-definition
- Definition of the solve macro.
- Solve-call-ACL2-rewriter
- Call the ACL2 rewriter on the matrix of old.
