		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-process-res

Process a result specification in the isomap input.

Signature
(isodata-process-res res m err-msg-preamble old$ ctx state) → (mv erp result state)
Arguments: m — Guard (posp m).; err-msg-preamble — Guard (msgp err-msg-preamble).; old$ — Guard (symbolp old$).
Returns: result — Type (acl2::typed-tuplep posp booleanp result).

Recall that m is the number of results of old.

We check that the result specification is a keyword :resultj, where j is a positive integer not exceeding m. We return j, if successful.

If m is 1, we also accept the keyword :result, treating it the same as :result1.

We also return a flag saying whether the result being transformed is a stobjs or not.

Definitions and Theorems

Function: isodata-process-res

(defun isodata-process-res (res m err-msg-preamble old$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (posp m)
                             (msgp err-msg-preamble)
                             (symbolp old$))))
 (declare
   (xargs :guard (not (member-eq old$ acl2::*stobjs-out-invalid*))))
 (let ((__function__ 'isodata-process-res))
  (declare (ignorable __function__))
  (b* ((irr-result (list 1 nil))
       (err-msg (msg "~@0 But ~x1 is none of those."
                     err-msg-preamble res))
       (stobjs-out (acl2::stobjs-out+ old$ (w state)))
       ((unless (= (len stobjs-out) m))
        (raise "Internal error: m is ~x0 but output stobjs are ~x1."
               m stobjs-out)
        (value irr-result))
       ((unless (keywordp res))
        (er-soft+ ctx t irr-result "~@0" err-msg))
       ((when (and (= m 1) (eq res :result)))
        (b* ((output (car stobjs-out))
             (xform-stobjs-p (not (eq output nil))))
          (value (list 1 xform-stobjs-p))))
       (name (symbol-name res))
       ((unless (and (> (length name) 6)
                     (equal (subseq name 0 6) "RESULT")))
        (er-soft+ ctx t irr-result "~@0" err-msg))
       (j (str::strval (subseq name 6 (length name))))
       ((unless j)
        (er-soft+ ctx t irr-result "~@0" err-msg))
       ((unless (and (<= 1 j) (<= j m)))
        (er-soft+ ctx t irr-result "~@0" err-msg))
       (output (nth (1- j) stobjs-out))
       (xform-stobj-p (not (eq output nil))))
    (value (list j xform-stobj-p)))))

Theorem: return-type-of-isodata-process-res.result

(defthm return-type-of-isodata-process-res.result
 (b* (((mv ?erp ?result acl2::?state)
       (isodata-process-res res m err-msg-preamble old$ ctx state)))
   (acl2::typed-tuplep posp booleanp result))
 :rule-classes :rewrite)