		Search-engine friendly clone of the ACL2 documentation.

Parteval-implementation

Parteval-fn

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

Signature
(parteval-fn old static new-name new-enable thm-name thm-enable verify-guards untranslate print show-only call ctx state) → (mv erp event state)
Arguments: 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: parteval-fn

(defun parteval-fn (old static new-name new-enable thm-name
                        thm-enable verify-guards untranslate
                        print show-only call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (pseudo-event-formp call)))
  (let ((__function__ 'parteval-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$ static$ new-name$ new-enable$
                    thm-name$ verify-guards$ case &))
          (parteval-process-inputs
               old static new-name new-enable
               thm-name thm-enable verify-guards
               untranslate print show-only ctx state))
         (event (parteval-gen-everything
                     old$
                     static$ new-name$ new-enable$ thm-name$
                     thm-enable verify-guards$ untranslate
                     print show-only case call (w state))))
      (value event))))