		Search-engine friendly clone of the ACL2 documentation.

Defaults-table

Set-default-input-old-to-wrapper-enable

Set the default :old-to-wrapper-enable input of APT transformations.

Some APT transformations include an :old-to-wrapper-enable input that specifies whether to enable the generated theorem that rewrites (a term involving) a call of the old function to (a term involving) a call of the wrapper function. This theorem is generated, and this input is allowed, only when the wrapper is generated.

This macro sets an entry in the APT defaults table that provides the default value of the :old-to-wrapper-enable input. It must be a boolean. It cannot be t if the default :wrapper-to-old-enable is currently t.

The initial value of this default is nil.

Macro: set-default-input-old-to-wrapper-enable

(defmacro set-default-input-old-to-wrapper-enable (bool)
  (declare (xargs :guard (booleanp bool)))
  (b* ((ctx (cons 'set-default-input-old-to-wrapper-enable
                  bool)))
    (cons 'make-event-terse
          (cons (cons 'set-default-input-old-to-wrapper-enable-fn
                      (cons bool
                            (cons (cons 'quote (cons ctx 'nil))
                                  '(state))))
                'nil))))

Definitions and Theorems

Function: set-default-input-old-to-wrapper-enable-fn

(defun set-default-input-old-to-wrapper-enable-fn (bool ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (booleanp bool)))
 (let ((__function__ 'set-default-input-old-to-wrapper-enable-fn))
  (declare (ignorable __function__))
  (b* ((table (table-alist+ *defaults-table-name* (w state))
)
       (pair (assoc-eq :wrapper-to-old-enable table)))
   (if
    (and (consp pair) (cdr pair) bool)
    (er-soft+
     ctx t nil
     "Since the :WRAPPER-TO-OLD-ENABLE default is T, ~
                     the :OLD-TO-WRAPPER-ENABLE default cannot be set to T. ~
                     At most one of these two defaults may be T at any time.")
    (value (cons 'table
                 (cons *defaults-table-name*
                       (cons ':old-to-wrapper-enable
                             (cons bool 'nil)))))))))