		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-function-is-pure-if-raw

Cause an error if a function has raw Lisp code and is not whitelisted as pure.

Signature
(ensure-function-is-pure-if-raw fn description error-erp error-val ctx state) → (mv erp val state)
Arguments: fn — Value to check.
Guard (symbolp fn).; description — Guard (msgp description).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — Type (implies erp (equal erp error-erp)).; val — Type (and (implies erp (equal val error-val)) (implies (and (not erp) error-erp) (not val))) .

Definitions and Theorems

Function: ensure-function-is-pure-if-raw

(defun ensure-function-is-pure-if-raw
       (fn description
           error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn) (msgp description))))
 (b*
  (((unless (or (not (rawp fn state))
                (pure-raw-p fn)))
    (er-soft+
     ctx error-erp error-val
     "~@0 has raw Lisp code, ~
           but it is not in the whitelist of ~
           known pure functions with raw Lisp code."
     description)))
  (value nil)))

Theorem: return-type-of-ensure-function-is-pure-if-raw.erp

(defthm return-type-of-ensure-function-is-pure-if-raw.erp
 (b*
  (((mv ?erp ?val ?state)
    (ensure-function-is-pure-if-raw fn description
                                    error-erp error-val ctx state)))
  (implies erp (equal erp error-erp)))
 :rule-classes :rewrite)

Theorem: return-type-of-ensure-function-is-pure-if-raw.val

(defthm return-type-of-ensure-function-is-pure-if-raw.val
 (b*
  (((mv ?erp ?val ?state)
    (ensure-function-is-pure-if-raw fn description
                                    error-erp error-val ctx state)))
  (and (implies erp (equal val error-val))
       (implies (and (not erp) error-erp)
                (not val))))
 :rule-classes :rewrite)

Subtopics

Ensure-function-is-pure-if-raw$: Calls ensure-function-is-pure-if-raw with ctx and state as the last two arguments.