Restrict-implementation
Implementation of restrict.
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.
- restriction 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.
- undefined 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.
- 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-to-new-name is the homonymous input to the event macro.
- old-to-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.
- new-to-old-name is the homonymous input to the event macro.
- new-to-old-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.
- hints 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.
- new is the homonymous function symbol described in the user documentation.
- old-to-new is the homonymous theorem symbol described in the user documentation.
- new-to-old is the homonymous theorem symbol described in the user documentation.
- stub? is the stub called ?f in the documentation
if old is a reflexive function,
or nil otherwise.
- appcond-thm-names is an alist
from the keywords that identify the applicability conditions
to the corresponding generated theorem names.
- old-unnorm is the name of the generated theorem
that installs the non-normalized definition of the target function.
- new-unnorm is the name of the generated theorem
that installs the non-normalized definition of the new function.
- 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
- Restrict-event-generation
- Event generation performed by restrict.
- Restrict-fn
- Check redundancy,
process the inputs, and
generate the event to submit.
- Restrict-macro-definition
- Definition of the restrict macro.
- Restrict-input-processing
- Input processing performed by restrict.
