		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-res

Process a result specification in the surjmap input.

Signature
(expdata-process-res res m err-msg-preamble ctx state) → (mv erp j state)
Arguments: m — Guard (posp m).; err-msg-preamble — Guard (msgp err-msg-preamble).
Returns: j — Type (posp j).

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.

Definitions and Theorems

Function: expdata-process-res

(defun expdata-process-res (res m err-msg-preamble ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (posp m) (msgp err-msg-preamble))))
  (let ((__function__ 'expdata-process-res))
    (declare (ignorable __function__))
    (b* ((err-msg (msg "~@0 But ~x1 is none of those."
                       err-msg-preamble res))
         ((unless (keywordp res))
          (er-soft+ ctx t 1 err-msg-preamble res))
         ((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 1 "~@0" err-msg))
         (j (str::strval (subseq name 6 (length name))))
         ((unless j)
          (er-soft+ ctx t 1 "~@0" err-msg))
         ((unless (and (<= 1 j) (<= j m)))
          (er-soft+ ctx t 1 "~@0" err-msg)))
      (value j))))

Theorem: posp-of-expdata-process-res.j

(defthm posp-of-expdata-process-res.j
  (b* (((mv ?erp ?j acl2::?state)
        (expdata-process-res res m err-msg-preamble ctx state)))
    (posp j))
  :rule-classes :rewrite)