		Search-engine friendly clone of the ACL2 documentation.

Expdata-implementation

Expdata-fn

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

Signature
(expdata-fn old surjmaps predicate 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 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: expdata-fn

(defun expdata-fn (old surjmaps predicate
                       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 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__ 'expdata-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-surjmaps
                res-surjmaps 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))
      (expdata-process-inputs old surjmaps predicate
                              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)
      (expdata-gen-everything old$ arg-surjmaps res-surjmaps
                              predicate 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
                              names-to-avoid call ctx state)))
    (value event))))