		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-function-number-of-results

Cause an error if a function does not have a given number of results.

Signature
(ensure-function-number-of-results fn n description error-erp error-val ctx state) → (mv erp val state)
Arguments: fn — Function to check.
Guard (and (function-namep fn (w state)) (not (member-eq fn *stobjs-out-invalid*))) .; n — Number of results that fn must have.
Guard (posp n).; 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))) .

The function must not be one whose stobjs-out are invalid.

Definitions and Theorems

Function: ensure-function-number-of-results

(defun ensure-function-number-of-results
       (fn n description
           error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare
  (xargs
      :guard (and (posp n)
                  (msgp description)
                  (and (function-namep fn (w state))
                       (not (member-eq fn *stobjs-out-invalid*))))))
 (b* (((unless (= (number-of-results fn (w state)) n))
       (er-soft+ ctx error-erp error-val
                 "~@0 must return ~x1 ~@2." description
                 n (if (= n 1) "result" "results"))))
   (value nil)))

Theorem: return-type-of-ensure-function-number-of-results.erp

(defthm return-type-of-ensure-function-number-of-results.erp
  (b* (((mv ?erp ?val ?state)
        (ensure-function-number-of-results
             fn n description
             error-erp error-val ctx state)))
    (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-ensure-function-number-of-results.val

(defthm return-type-of-ensure-function-number-of-results.val
  (b* (((mv ?erp ?val ?state)
        (ensure-function-number-of-results
             fn n 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-number-of-results$: Calls ensure-function-number-of-results with ctx and state as the last two arguments.