Defarbrec-implementation
Implementation of defarbrec.
The implementation functions have formal parameters
consistently named as follows:
- state is the ACL2's state.
- wrld is the ACL2's world.
- ctx is the context used for errors.
- fn,
x1...xn,
body,
update-names,
terminates-name,
measure-name,
nonterminating,
print, and
show-only
are the homonymous inputs to defarbrec
(where x1...xn is for the input (x1 ... xn))
before being processed.
These formal parameters have no types because they may be any values.
- call is the call of defarbrec supplied by the user.
- call$ is the result of removing
:print and :show-only from call.
- fn$,
x1...xn$,
update-names$,
terminates-name$,
measure-name$,
nonterminating$,
print$, and
show-only$
are the results of processing
the homonymous (without the $) inputs to defarbrec.
Some are identical to the corresponding inputs,
but they have types implied by their successful validation,
performed when they are processed.
- terminates-witness-name is the name of the witness function
generated along with the termination testing predicate,
via defun-sk.
- terminated-rewrite-name is the name of the rewrite rule
generated along with the termination testing predicate,
via defun-sk.
- xi...xn$ is a suffix of x1...xn$,
while cdring down the list in a recursion.
- body$ is the unnormalized body that defines
the program-mode function temporarily recorded in the world.
It is a translated term.
- test is the exit test of the program-mode function.
- updates is the list of
argument updates in the recursive call of the program-mode function.
- k is a variable that counts the number of iterated argument udpates,
used as a formal parameter of the iterated argument update functions,
as a bound variable of the termination testing predicate,
and as a formal parameter of the measure function.
It is also used in generated local lemmas.
- l is another variable that counts
the number of iterated argument udpates,
used in generated local lemmas.
- update-fns-lemma-name is
the name of the generated local lemma
about the iterated argument update functions.
- measure-fn-natp-lemma-name is
the name of the first generated local lemma
about the generated measure function.
- measure-fn-end-lemma-name is
the name of the second generated local lemma
about the generated measure function.
- measure-fn-min-lemma-name is
the name of the third generated local lemma
about the generated measure function.
- names-to-avoid is a list of symbols already committed
to use for some functions and theorems to be generated;
symbols to use for additional functions and theorems to be generated
must be therefore distinct from them.
- expansion is the encapsulate
generated by defarbrec.
The parameters of implementation functions that are not listed above
are described in, or clear from, those functions' documentation.
Subtopics
- Defarbrec-event-generation
- Event generation performed by defarbrec.
- Defarbrec-input-processing
- Input processing performed by defarbrec.
- Defarbrec-check-redundancy
- Check if a call of defarbrec is redundant.
- Defarbrec-fn
- Check redundancy,
process the inputs,
and generate the event to submit.
- Defarbrec-table
- Table of defarbrec functions.
- Defarbrec-macro-definition
- Definition of the defarbrec macro.
