		Search-engine friendly clone of the ACL2 documentation.

Isodata-implementation

Isodata-fn

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

Signature
(isodata-fn old isomaps predicate undefined new-name new-enable old-to-new-name old-to-new-name-suppliedp old-to-new-enable old-to-new-enable-suppliedp new-to-old-name new-to-old-name-suppliedp new-to-old-enable new-to-old-enable-suppliedp newp-of-new-name newp-of-new-name-suppliedp newp-of-new-enable newp-of-new-enable-suppliedp verify-guards untranslate hints print show-only compatibility call ctx state) → (mv erp event-form state)
Arguments: old-to-new-name-suppliedp — Guard (booleanp old-to-new-name-suppliedp).; old-to-new-enable-suppliedp — Guard (booleanp old-to-new-enable-suppliedp).; new-to-old-name-suppliedp — Guard (booleanp new-to-old-name-suppliedp).; new-to-old-enable-suppliedp — Guard (booleanp new-to-old-enable-suppliedp).; newp-of-new-name-suppliedp — Guard (booleanp newp-of-new-name-suppliedp).; newp-of-new-enable-suppliedp — Guard (booleanp newp-of-new-enable-suppliedp).; call — Guard (pseudo-event-formp call).
Returns: event-form — 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. Do nothing if this invocation of the transformation is redundant.

Definitions and Theorems

Function: isodata-fn

(defun isodata-fn (old isomaps predicate undefined
                       new-name new-enable old-to-new-name
                       old-to-new-name-suppliedp
                       old-to-new-enable
                       old-to-new-enable-suppliedp
                       new-to-old-name
                       new-to-old-name-suppliedp
                       new-to-old-enable
                       new-to-old-enable-suppliedp
                       newp-of-new-name
                       newp-of-new-name-suppliedp
                       newp-of-new-enable
                       newp-of-new-enable-suppliedp
                       verify-guards untranslate hints print
                       show-only compatibility call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp old-to-new-name-suppliedp)
                             (booleanp old-to-new-enable-suppliedp)
                             (booleanp new-to-old-name-suppliedp)
                             (booleanp new-to-old-enable-suppliedp)
                             (booleanp newp-of-new-name-suppliedp)
                             (booleanp newp-of-new-enable-suppliedp)
                             (pseudo-event-formp call))))
 (let ((__function__ 'isodata-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$ arg-isomaps
                 res-isomaps undefined$ new$ new-enable$
                 old-to-new$ old-to-new-enable$
                 new-to-old$ new-to-old-enable$
                 newp-of-new$ newp-of-new-enable$
                 verify-guards$ hints$ names-to-avoid))
       (isodata-process-inputs old isomaps predicate undefined
                               new-name new-enable old-to-new-name
                               old-to-new-name-suppliedp
                               old-to-new-enable
                               old-to-new-enable-suppliedp
                               new-to-old-name
                               new-to-old-name-suppliedp
                               new-to-old-enable
                               new-to-old-enable-suppliedp
                               newp-of-new-name
                               newp-of-new-name-suppliedp
                               newp-of-new-enable
                               newp-of-new-enable-suppliedp
                               verify-guards untranslate
                               hints print show-only ctx state))
      ((er event)
       (isodata-gen-everything old$ arg-isomaps res-isomaps
                               predicate undefined$ new$ new-enable$
                               old-to-new$ old-to-new-enable$
                               new-to-old$ new-to-old-enable$
                               newp-of-new$ newp-of-new-enable$
                               verify-guards$ untranslate
                               hints$ print show-only compatibility
                               names-to-avoid call ctx state)))
     (value event))))