		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 xform-stobjs-p
                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 xform-stobjs-p
                              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))))