		Search-engine friendly clone of the ACL2 documentation.

Tailrec-implementation

Tailrec-fn

Check redundancy, process the inputs, and generate the event to submit.

Signature
(tailrec-fn old variant domain new-name new-enable accumulator wrapper wrapper-name wrapper-name-present wrapper-enable wrapper-enable-present old-to-new-name old-to-new-name-present old-to-new-enable old-to-new-enable-present new-to-old-name new-to-old-name-present new-to-old-enable new-to-old-enable-present old-to-wrapper-name old-to-wrapper-name-present old-to-wrapper-enable old-to-wrapper-enable-present wrapper-to-old-name wrapper-to-old-name-present wrapper-to-old-enable wrapper-to-old-enable-present verify-guards hints print show-only call ctx state) → (mv erp event state)
Arguments: wrapper-name-present — Guard (booleanp wrapper-name-present).; wrapper-enable-present — Guard (booleanp wrapper-enable-present).; old-to-new-name-present — Guard (booleanp old-to-new-name-present).; old-to-new-enable-present — Guard (booleanp old-to-new-enable-present).; new-to-old-name-present — Guard (booleanp new-to-old-name-present).; new-to-old-enable-present — Guard (booleanp new-to-old-enable-present).; old-to-wrapper-name-present — Guard (booleanp old-to-wrapper-name-present).; old-to-wrapper-enable-present — Guard (booleanp old-to-wrapper-enable-present).; wrapper-to-old-name-present — Guard (booleanp wrapper-to-old-name-present).; wrapper-to-old-enable-present — Guard (booleanp wrapper-to-old-enable-present).; call — Guard (pseudo-event-formp call).
Returns: event — A pseudo-event-formp.

If this call to the transformation is redundant, a message to that effect is printed on the screen. If the transformation is redundant and :show-only is t, the encapsulate, retrieved from the table, is shown on the screen.

Definitions and Theorems

Function: tailrec-fn

(defun tailrec-fn (old variant domain
                       new-name new-enable accumulator wrapper
                       wrapper-name wrapper-name-present
                       wrapper-enable wrapper-enable-present
                       old-to-new-name old-to-new-name-present
                       old-to-new-enable
                       old-to-new-enable-present
                       new-to-old-name new-to-old-name-present
                       new-to-old-enable
                       new-to-old-enable-present
                       old-to-wrapper-name
                       old-to-wrapper-name-present
                       old-to-wrapper-enable
                       old-to-wrapper-enable-present
                       wrapper-to-old-name
                       wrapper-to-old-name-present
                       wrapper-to-old-enable
                       wrapper-to-old-enable-present
                       verify-guards
                       hints print show-only call ctx state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (booleanp wrapper-name-present)
                         (booleanp wrapper-enable-present)
                         (booleanp old-to-new-name-present)
                         (booleanp old-to-new-enable-present)
                         (booleanp new-to-old-name-present)
                         (booleanp new-to-old-enable-present)
                         (booleanp old-to-wrapper-name-present)
                         (booleanp old-to-wrapper-enable-present)
                         (booleanp wrapper-to-old-name-present)
                         (booleanp wrapper-to-old-enable-present)
                         (pseudo-event-formp call))))
 (let ((__function__ 'tailrec-fn))
  (declare (ignorable __function__))
  (b*
   ((encapsulate?
         (previous-transformation-expansion call (w state)))
    ((when encapsulate?)
     (b* (((run-when show-only)
           (cw "~x0~|" encapsulate?)))
       (cw "~%The transformation ~x0 is redundant.~%"
           call)
       (value '(value-triple :invisible))))
    ((er (list old$ test
               base nonrec updates combine q r domain$
               new-name$ new-enable$ a 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$ names-to-avoid))
     (tailrec-process-inputs old variant domain
                             new-name new-enable accumulator wrapper
                             wrapper-name wrapper-name-present
                             wrapper-enable wrapper-enable-present
                             old-to-new-name old-to-new-name-present
                             old-to-new-enable
                             old-to-new-enable-present
                             new-to-old-name new-to-old-name-present
                             new-to-old-enable
                             new-to-old-enable-present
                             old-to-wrapper-name
                             old-to-wrapper-name-present
                             old-to-wrapper-enable
                             old-to-wrapper-enable-present
                             wrapper-to-old-name
                             wrapper-to-old-name-present
                             wrapper-to-old-enable
                             wrapper-to-old-enable-present
                             verify-guards
                             hints print show-only ctx state))
    ((er event)
     (tailrec-gen-everything old$ test base nonrec updates
                             combine q r variant domain$ new-name$
                             new-enable$ a 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 show-only
                             call names-to-avoid ctx state)))
   (value event))))