• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
          • Isodata
            • Isodata-implementation
              • Isodata-event-generation
              • Isodata-fn
              • Isodata-input-processing
                • Isodata-symbol-isomap-alistp
                • Isodata-isomapp
                • Isodata-pos-isomap-alistp
                • Isodata-process-iso
                • Isodata-process-inputs
                • Isodata-process-arg/res-list-iso
                • Isodata-process-isomaps
                • Isodata-fresh-defiso-thm-names
                • Isodata-process-arg/res-list
                • Isodata-process-arg/res-list-iso-list
                • Isodata-process-res
                  • Isodata-process-old
                  • Isodata-fresh-defiso-name-with-*s-suffix
                  • Isodata-process-newp-of-new-name
                  • Isodata-process-undefined
                  • Isodata-isomap-listp
                • Isodata-macro-definition
            • Simplify-defun
            • Tailrec
            • Schemalg
            • Restrict
            • Expdata
            • Casesplit
            • Simplify-term
            • Simplify-defun-sk
            • Parteval
            • Solve
            • Wrap-output
            • Propagate-iso
            • Simplify
            • Finite-difference
            • Drop-irrelevant-params
            • Copy-function
            • Lift-iso
            • Rename-params
            • Utilities
            • Simplify-term-programmatic
            • Simplify-defun-sk-programmatic
            • Simplify-defun-programmatic
            • Simplify-defun+
            • Common-options
            • Common-concepts
          • Error-checking
          • Fty-extensions
          • Isar
          • Kestrel-utilities
          • Set
          • Soft
          • C
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Riscv
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • 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)