		Search-engine friendly clone of the ACL2 documentation.

Restrict-input-processing

Restrict-process-inputs

Process all the inputs.

Signature
(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) → (mv erp result 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?).
Returns: result — A (tuple (old symbolp) (restriction pseudo-termp) (undefined pseudo-termp) (new symbolp) (new-enable booleanp) (old-to-new symbolp) (old-to-new-enable symbolp) (new-to-old symbolp) (new-to-old-enable symbolp) (verify-guards booleanp) (hints evmac-input-hints-p) (names-to-avoid symbol-listp) result).

Definitions and Theorems

Function: restrict-process-inputs

(defun 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)
 (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?))))
 (let ((__function__ 'restrict-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((er old)
     (restrict-process-old old verify-guards ctx state))
    ((er verify-guards)
     (process-input-verify-guards verify-guards old ctx state))
    ((er restriction)
     (restrict-process-restriction restriction
                                   old verify-guards ctx state))
    ((er undefined)
     (restrict-process-undefined undefined old ctx state))
    ((er (list new names-to-avoid))
     (process-input-new-name new-name old nil ctx state))
    ((er new-enable)
     (process-input-new-enable new-enable old ctx state))
    ((er (list old-to-new names-to-avoid))
     (process-input-old-to-new-name
          old-to-new-name old-to-new-name?
          old new names-to-avoid ctx state))
    ((er old-to-new-enable)
     (process-input-old-to-new-enable old-to-new-enable
                                      old-to-new-enable? ctx state))
    ((er (list new-to-old names-to-avoid))
     (process-input-new-to-old-name
          new-to-old-name new-to-old-name?
          old new names-to-avoid ctx state))
    ((er new-to-old-enable)
     (process-input-new-to-old-enable new-to-old-enable
                                      new-to-old-enable? ctx state))
    ((er hints)
     (evmac-process-input-hints hints ctx state))
    ((er &)
     (evmac-process-input-print print ctx state))
    ((er &)
     (evmac-process-input-show-only show-only ctx state)))
   (value (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)))))