		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-verify-guards

Process the :verify-guards input of an APT transformation.

Signature
(process-input-verify-guards verify-guards old ctx state) → (mv erp doit state)
Arguments: old — Guard (symbolp old).
Returns: doit — Type (booleanp doit).

The APT transformations that use this utility have a :verify-guards input that specifies whether to verify the guards of the generated function(s). This input must be a boolean or :auto (the default). If it is :auto, guard verification takes place iff the old function is guard-verified. In any case, this utility returns a boolean saying whether the guard verification must take place or not.

Definitions and Theorems

Function: process-input-verify-guards

(defun process-input-verify-guards (verify-guards old ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (symbolp old)))
 (let ((__function__ 'process-input-verify-guards))
  (declare (ignorable __function__))
  (cond
   ((eq verify-guards t) (value t))
   ((eq verify-guards nil) (value nil))
   ((eq verify-guards :auto)
    (value (guard-verified-p old (w state))))
   (t
    (er-soft+
     ctx t nil
     "The :VERIFY-GUARDS input must be T, NIL, or :AUTO, ~
                      but it is ~x0 instead."
     verify-guards)))))

Theorem: booleanp-of-process-input-verify-guards.doit

(defthm booleanp-of-process-input-verify-guards.doit
  (b* (((mv ?erp ?doit acl2::?state)
        (process-input-verify-guards verify-guards old ctx state)))
    (booleanp doit))
  :rule-classes :rewrite)