Tailrec-implementation
Implementation of tailrec.
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,
variant,
domain,
new-name,
new-enable,
wrapper,
wrapper-name,
wrapper-enable,
old-to-new-name,
old-to-new-enable,
new-to-old-name,
new-to-old-enable,
old-to-wrapper-name,
old-to-wrapper-enable,
wrapper-to-old-name,
wrapper-to-old-enable,
verify-guards,
hints,
print, and
show-only
are the homonymous inputs to tailrec,
before being processed.
These formal parameters have no types because they may be any values.
- wrapper-name-present,
wrapper-enable-present,
old-to-new-name-present,
old-to-new-enable-present,
new-to-old-name-present,
new-to-old-enable-present,
old-to-wrapper-name-present,
old-to-wrapper-enable-present
wrapper-to-old-name-present, and
wrapper-to-old-enable-present
are boolean flags indicating whether the corresponding inputs
(whose name is obtained by removing -present from these)
are present (i.e. supplied by the user) or not.
- call is the call to tailrec supplied by the user.
- old$,
variant$,
domain$,
new-name$,
new-enable$,
wrapper$,
wrapper-name$,
wrapper-enable$,
old-to-new-name$,
old-to-new-enable$,
new-to-old-name$,
new-to-old-enable$,
old-to-wrapper-name$,
wrapper-to-old-name$,
verify-guards$,
hints$,
print$, and
show-only$
are the results of processing
the homonymous inputs (without the $) to tailrec.
Some are identical to the corresponding inputs,
but they have types implied by their successful validation,
performed when they are processed.
- test is the term test<x1,...,xn> described in the documentation.
- base is the term base<x1,...,xn> described in the documentation.
- rec-branch is the recursive branch of the target function,
namely the term combine<nonrec<x1,...,xn>,
(old update-x1<x1,...,xn>
...
update-xn<x1,...,xn>)>
described in the documentation.
- nonrec is the term nonrec<x1,...,xn>
described in the documentation.
- updates is the list of terms
update-x1<x1,...,xn>, ..., update-xn<x1,...,xn>
described in the documentation.
- r is the homonymous fresh variable described in the documentation.
- q is the homonymous fresh variable described in the documentation.
- combine-nonrec is the term combine<nonrec<x1,...,xn>,r>
described in the documentation.
- combine is the term combine<q,r> described in the documentation.
- a is the homonymous accumulator variable
described in the documentation.
- verbose is a flag saying
whether to print certain informative messages or not.
- appcond-thm-names is an alist
from the keywords that identify the applicability conditions
to the corresponding generated theorem names.
- old-unnorm-name is the name of the generated theorem
that installs the non-normalized definition of the target function.
- new-unnorm-name is the name of the generated theorem
that installs the non-normalized definition of the new function.
- wrapper-unnorm-name is the name of the generated theorem
that installs the non-normalized definition of the wrapper function.
- new-formals are the formal parameters of the new function.
- domain-of-old-name is the name of the theorem
generated by tailrec-gen-domain-of-old-thm.
- alpha-name is the name of the function
generated by tailrec-gen-alpha-fn.
- test-of-alpha-name is the name of the theorem
generated by tailrec-gen-test-of-alpha-thm.
- old-guard-of-alpha-name is the name of the theorem
generated by tailrec-gen-old-guard-of-alpha-thm.
- domain-of-ground-base-name is the name of the theorem
generated by tailrec-gen-domain-of-ground-base-thm.
- combine-left-identity-ground-name is the name of the theorem
generated by tailrec-gen-combine-left-identity-ground-thm.
- base-guard-name is the name of the theorem
generated by tailrec-gen-base-guard-thm.
- 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
- Tailrec-event-generation
- Event generation performed by tailrec.
- Tailrec-fn
- Check redundancy,
process the inputs, and
generate the event to submit.
- Tailrec-macro-definition
- Definition of the tailrec macro.
- Tailrec-input-processing
- Input processing performed by tailrec.
