Expdata-implementation
Implementation of expdata.
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,
surjmaps,
predicate,
new-name,
new-enable,
old-to-new-name,
old-to-new-enable,
new-to-old-name,
new-to-old-enable,
newp-of-new-name,
newp-of-new-enable,
verify-guards,
untranslate,
hints,
print, and
show-only
are the homonymous inputs to expdata,
before being validated.
These formal parameters have no types because they may be any values.
- old$,
predicate$,
new-enable$,
old-to-new-enable$,
new-to-old-enable$,
newp-of-new-enable$,
verify-guards$,
untranslate$,
hints$,
print$, and
show-only$
are the result of processing
the homonymous inputs (without the $).
Some are identical to the corresponding inputs,
but they have types implied by their successful validation,
performed when they are processed.
- new$ is the result of processing new-name.
- old-to-new$ is the result of processing old-to-new-name.
- new-to-old$ is the result of processing new-to-old-name.
- newp-of-new$ is the result of processing newp-of-new-name.
- m is the number of results of old.
- arg-surjmaps is an alist
from formal arguments of old
to surjective mapping records that specify
how the associated formal arguments must be transformed.
There are never duplicate keys.
When input processing is complete,
the keys are exactly all the formal arguments of old, in order.
arg-surjmaps results from processing surjmaps.
- res-surjmaps is an alist
from positive integers from 1 to m
to surjective mapping records that specify
how the result with the associated (1-based) indices
must be transformed.
There are never duplicate keys.
When input processing is complete:
if some results are transformed,
the keys are exactly all the integers from 1 to m, in order;
if no results are transformed,
the alist is nil.
res-surjmaps results from processing surjmaps.
- appcond-thm-names is an alist
from the applicability condition keywords
to the corresponding theorem names.
- old-fn-unnorm-name is the name of the theorem
that installs the non-normalized definition of the old function.
- new-fn-unnorm-name is the name of the theorem
that installs the non-normalized definition of the new function.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
Subtopics
- Expdata-event-generation
- Event generation performed by expdata.
- Expdata-fn
- Check redundancy,
process the inputs, and
generate the event to submit.
- Expdata-input-processing
- Input processing performed by expdata.
- Expdata-macro-definition
- Definition of the expdata macro.
