		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-multiple-values

Atj-restore-mv-calls-in-body

Restore mv calls in a translated function body.

Signature
(atj-restore-mv-calls-in-body body out-types wrld) → new-body
Arguments: body — Guard (pseudo-termp body).; out-types — Guard (atj-type-listp out-types).; wrld — Guard (plist-worldp wrld).
Returns: new-body — Type (pseudo-termp new-body), given (pseudo-termp body).

This is the top-level call of atj-restore-mv-calls-in-term: see that function for details. We initialize numres with the number of output types of the function whose body we are processing.

Definitions and Theorems

Function: atj-restore-mv-calls-in-body

(defun atj-restore-mv-calls-in-body (body out-types wrld)
  (declare (xargs :guard (and (pseudo-termp body)
                              (atj-type-listp out-types)
                              (plist-worldp wrld))))
  (let ((__function__ 'atj-restore-mv-calls-in-body))
    (declare (ignorable __function__))
    (b* ((numres (len out-types))
         ((unless (> numres 0))
          (raise "Internal error: no output types.")))
      (atj-restore-mv-calls-in-term body (len out-types)
                                    wrld))))

Theorem: pseudo-termp-of-atj-restore-mv-calls-in-body

(defthm pseudo-termp-of-atj-restore-mv-calls-in-body
 (implies
   (pseudo-termp body)
   (b*
     ((new-body (atj-restore-mv-calls-in-body body out-types wrld)))
     (pseudo-termp new-body)))
 :rule-classes :rewrite)