		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-old-to-wrapper-enable

Process the :old-to-wrapper-enable input of an APT transformation.

Signature
(process-input-old-to-wrapper-enable old-to-wrapper-enable old-to-wrapper-enable-present gen-wrapper ctx state) → (mv erp processed-old-to-wrapper-enable state)
Arguments: old-to-wrapper-enable-present — Guard (booleanp old-to-wrapper-enable-present).; gen-wrapper — Guard (booleanp gen-wrapper).
Returns: processed-old-to-wrapper-enable — Type (booleanp processed-old-to-wrapper-enable).

This is quite analogous to process-input-old-to-new-enable, but for the :old-to-wrapper-enable input of an APT transformation. The gen-wrapper parameter is t iff the wrapper is generated, i.e. if the :wrapper input of the transformation is t. If this is nil, we ensure that :old-to-wrapper-enable is absent.

Definitions and Theorems

Function: process-input-old-to-wrapper-enable

(defun process-input-old-to-wrapper-enable
       (old-to-wrapper-enable old-to-wrapper-enable-present
                              gen-wrapper ctx state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (booleanp old-to-wrapper-enable-present)
                         (booleanp gen-wrapper))))
 (let ((__function__ 'process-input-old-to-wrapper-enable))
  (declare (ignorable __function__))
  (if gen-wrapper
   (if old-to-wrapper-enable-present
    (b*
     (((er &)
       (ensure-value-is-boolean$ old-to-wrapper-enable
                                 "The :OLD-TO-WRAPPER-ENABLE input"
                                 t nil)))
     (value old-to-wrapper-enable))
    (value (get-default-input-old-to-wrapper-enable (w state))))
   (if old-to-wrapper-enable-present
    (er-soft+
     ctx t nil
     "Since the :WRAPPER input is (perhaps by default) NIL, ~
                   no :OLD-TO-WRAPPER-ENABLE input may be supplied,
                   but ~x0 was supplied instead."
     old-to-wrapper-enable)
    (value nil)))))

Theorem: booleanp-of-process-input-old-to-wrapper-enable.processed-old-to-wrapper-enable

(defthm
 booleanp-of-process-input-old-to-wrapper-enable.processed-old-to-wrapper-enable
 (b* (((mv ?erp ?processed-old-to-wrapper-enable
           acl2::?state)
       (process-input-old-to-wrapper-enable
            old-to-wrapper-enable
            old-to-wrapper-enable-present
            gen-wrapper ctx state)))
   (booleanp processed-old-to-wrapper-enable))
 :rule-classes :rewrite)