		Search-engine friendly clone of the ACL2 documentation.

Untranslate-for-execution

Convert-subexpression-to-mv

Rewrite an expression that occurs a multiply valued context to make its multiple returns explicit.

Signature
(convert-subexpression-to-mv n x world) → (mv errmsg new-x)
Arguments: n — Number of return values this expression has.
Guard (natp n).; x — The expression to rewrite.
Guard (ute-term-p x).; world — World, for return-value checking.
Guard (plist-worldp world).
Returns: errmsg — NIL on success, or an error msg on failure.; new-x — Type (ute-term-p new-x), given (ute-term-p x).

Definitions and Theorems

Function: convert-subexpression-to-mv

(defun convert-subexpression-to-mv (n x world)
 (declare (xargs :guard (and (natp n)
                             (ute-term-p x)
                             (plist-worldp world))))
 (declare (xargs :guard (<= 2 n)))
 (let ((__function__ 'convert-subexpression-to-mv))
  (declare (ignorable __function__))
  (b*
   (((when (atom x))
     (mv (msg "Expected ~x0 return values, found ~x1."
              n x)
         x))
    ((when (fquotep x))
     (mv (msg "Expected ~x0 return values, found ~x1."
              n x)
         x))
    (fn (first x))
    (args (rest x))
    ((when (consp fn))
     (b* (((list & formals body) (first x))
          ((mv err body)
           (convert-subexpression-to-mv n body world))
          ((when err) (mv err x))
          (new-x (cons (list 'lambda formals body)
                       (cdr x))))
       (mv nil new-x)))
    ((when (eq fn 'if))
     (b* (((list test then else) args)
          ((mv err1 then)
           (convert-subexpression-to-mv n then world))
          ((when err1)
           (mv (msg "> In then branch of ~x0:~%~@1~%"
                    test err1)
               x))
          ((mv err2 else)
           (convert-subexpression-to-mv n else world))
          ((when err2)
           (mv (msg "> In else branch of ~x0:~%~@1~%"
                    else err2)
               x))
          (new-x (list 'if test then else)))
       (mv nil new-x)))
    ((when (eq fn 'mv-let))
     (b* (((list vars expr body) args)
          ((mv err1 body)
           (convert-subexpression-to-mv n body world))
          ((when err1)
           (mv (msg "> In body of mv-let binding ~x0:~%~@1~%"
                    vars err1)
               x))
          (new-x (list 'mv-let vars expr body)))
       (mv nil new-x)))
    ((when (eq fn 'cons))
     (b*
      (((mv matchp cons-args)
        (match-cons-nest x))
       ((unless matchp)
        (mv (msg "Expected ~x0 return values, found ~x1.~%"
                 n x)
            x))
       ((unless (equal (len cons-args) n))
        (mv
         (msg
          "Expected ~x0 return values, but found cons nest of size ~x1: ~x2~%"
          n (len cons-args)
          x)
         x))
       (new-x (cons 'mv cons-args)))
      (mv nil new-x)))
    (stobjs-out (getprop fn 'stobjs-out
                         :bad 'current-acl2-world
                         world))
    ((when (eq stobjs-out :bad))
     (mv (msg "Don't know :stobjs-out of ~x0.~%" fn)
         x))
    ((unless (equal (len stobjs-out) n))
     (mv
      (msg "Expected ~x0 return values, but ~x1 returns ~x2 values."
           n (car x)
           (len stobjs-out))
      x)))
   (mv nil x))))

Theorem: ute-term-p-of-convert-subexpression-to-mv.new-x

(defthm ute-term-p-of-convert-subexpression-to-mv.new-x
  (implies (ute-term-p x)
           (b* (((mv ?errmsg ?new-x)
                 (convert-subexpression-to-mv n x world)))
             (ute-term-p new-x)))
  :rule-classes :rewrite)