		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Unwrapped-nonexec-body+

Enhanced variant of unwrapped-nonexec-body.

Signature
(unwrapped-nonexec-body+ fn wrld) → unwrapped-body
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: unwrapped-body — Type (pseudo-termp unwrapped-body).

This returns the same result as unwrapped-nonexec-body, but it is guard-verified and includes a run-time check (which should always succeed) on the result that allows us to prove the return type theorem without strengthening the guard on wrld. This utility also includes a run-time check (which should always succeed) that the wrapper around the body has the expected form, via the built-in function throw-nonexec-error-p; this allows us to verify the guards without strengthening the guard of wrld. Furthermore, this utility causes an error if called on a symbol that does not name a function (the error is caused via the call to non-executablep+), or if the function is executable (i.e. :non-executable is nil, or if the function does not have an unnormalized-body (which is retrieved and unwrapped).

Definitions and Theorems

Function: unwrapped-nonexec-body+

(defun unwrapped-nonexec-body+ (fn wrld)
 (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
 (let ((__function__ 'unwrapped-nonexec-body+))
  (declare (ignorable __function__))
  (b*
   (((unless (non-executablep fn wrld))
     (raise "The function ~x0 is executable." fn))
    (body (ubody+ fn wrld))
    ((unless body)
     (raise "The function ~x0 does not have an unnormalized body."
            fn))
    ((unless (and (throw-nonexec-error-p body fn (formals+ fn wrld))
                  (consp (cdddr body))))
     (raise
      "Internal error: ~
                the body ~x0 of the non-executable function ~x1 ~
                does not have the expected wrapper."
      body fn))
    (unwrapped-body (fourth body))
    ((unless (pseudo-termp unwrapped-body))
     (raise
      "Internal error: ~
                the unwrapped body ~x0 of the non-executable function ~x1 ~
                is not a pseudo-term."
      unwrapped-body fn)))
   unwrapped-body)))

Theorem: pseudo-termp-of-unwrapped-nonexec-body+

(defthm pseudo-termp-of-unwrapped-nonexec-body+
  (b* ((unwrapped-body (unwrapped-nonexec-body+ fn wrld)))
    (pseudo-termp unwrapped-body))
  :rule-classes :rewrite)