Process a result specification in the
(isodata-process-res res m err-msg-preamble old$ ctx state) → (mv erp result state)
Recall that
We check that the result specification is a keyword
If
We also return a flag saying whether the result being transformed is a stobjs or not.
Function:
(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:
(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)