Process a result specification in the
Recall that
We check that the result specification is a keyword
If
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 1) (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))) (value 1)) (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))) (value j))))
Theorem:
(defthm posp-of-isodata-process-res.result (b* (((mv ?erp ?result acl2::?state) (isodata-process-res res m err-msg-preamble old$ ctx state))) (posp result)) :rule-classes :rewrite)