		Search-engine friendly clone of the ACL2 documentation.

Restrict-implementation

Restrict-fn

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

Signature
(restrict-fn old restriction undefined new-name new-enable old-to-new-name old-to-new-name? old-to-new-enable old-to-new-enable? new-to-old-name new-to-old-name? new-to-old-enable new-to-old-enable? verify-guards hints print show-only call ctx state) → (mv erp event state)
Arguments: old-to-new-name? — Guard (booleanp old-to-new-name?).; old-to-new-enable? — Guard (booleanp old-to-new-enable?).; new-to-old-name? — Guard (booleanp new-to-old-name?).; new-to-old-enable? — Guard (booleanp new-to-old-enable?).; 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: restrict-fn

(defun restrict-fn (old restriction undefined
                        new-name new-enable old-to-new-name
                        old-to-new-name? old-to-new-enable
                        old-to-new-enable? new-to-old-name
                        new-to-old-name? new-to-old-enable
                        new-to-old-enable? verify-guards
                        hints print show-only call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp old-to-new-name?)
                             (booleanp old-to-new-enable?)
                             (booleanp new-to-old-name?)
                             (booleanp new-to-old-enable?)
                             (pseudo-event-formp call))))
 (let ((__function__ 'restrict-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 restriction undefined new
                  new-enable old-to-new old-to-new-enable
                  new-to-old new-to-old-enable
                  verify-guards hints names-to-avoid))
        (restrict-process-inputs old restriction undefined
                                 new-name new-enable old-to-new-name
                                 old-to-new-name? old-to-new-enable
                                 old-to-new-enable? new-to-old-name
                                 new-to-old-name? new-to-old-enable
                                 new-to-old-enable? verify-guards
                                 hints print show-only ctx state))
       ((er event)
        (restrict-gen-everything
             old restriction undefined new
             new-enable old-to-new old-to-new-enable
             new-to-old new-to-old-enable
             verify-guards hints print show-only
             call names-to-avoid ctx state)))
    (value event))))