MV-LET

calling multi-valued ACL2 functions 
Major Section:  PROGRAMMING


Example Form:
(mv-let (x y z)              ; local variables
        (mv 1 2 3)           ; multi-valued expression
        (declare (ignore y)) ; optional declarations
        (cons x z))          ; body
The form above binds the three ``local variables,'' x, y, and z, to the three results returned by the multi-valued expression and then evaluates the body. The result is '(1 . 3). The second local, y, is declared ignored. The multi-valued expression can be any ACL2 expression that returns k results, where k is the number of local variables listed. Often however it is simply the application of a k-valued function. Mv-let is the standard way to invoke a multi-valued function when the caller must manipulate the vector of results returned. 

General Form:
(mv-let (var1 ... vark)
        term
        body)
or
(mv-let (var1 ... vark)
        term
        (declare ...) ... (declare ...)
        body)
where the vari are distinct variables, term is a term that returns k results and mentions only variables bound in the environment containing the mv-let expression, and body is a term mentioning only the vari and variables bound in the environment containing the mv-let. Each vari must occur in body unless it is declared ignored in one of the optional declare forms, unless this requirement is turned off; see set-ignore-ok. The value of the mv-let term is the result of evaluating body in an environment in which the vari are bound, in order, to the k results obtained by evaluating term in the environment containing the mv-let.

Here is an extended example that illustrates both the definition of a multi-valued function and the use of mv-let to call it. Consider a simple binary tree whose interior nodes are conses and whose leaves are non-conses. Suppose we often need to know the number, n, of interior nodes of such a tree; the list, syms, of symbols that occur as leaves; and the list, ints, of integers that occur as leaves. (Observe that there may be leaves that are neither symbols nor integers.) Using a multi-valued function we can collect all three results in one pass.

Here is the first of two definitions of the desired function. This definition is ``primitive recursive'' in that it has only one argument and that argument is reduced in size on every recursion. 

(defun count-and-collect (x)


; We return three results, (mv n syms ints) as described above.


  (cond ((atom x)


; X is a leaf.  Thus, there are 0 interior nodes, and depending on
; whether x is a symbol, an integer, or something else, we return
; the list containing x in as the appropriate result.


         (cond ((symbolp x) (mv 0 (list x) nil))
               ((integerp x)(mv 0 nil      (list x)))
               (t           (mv 0 nil      nil))))
        (t 


; X is an interior node.  First we process the car, binding n1, syms1, and
; ints1 to the answers.


           (mv-let (n1 syms1 ints1)
                   (count-and-collect (car x))


; Next we process the cdr, binding n2, syms2, and ints2.


                   (mv-let (n2 syms2 ints2)
                           (count-and-collect (car x))


; Finally, we compute the answer for x from those obtained for its car
; and cdr, remembering to increment the node count by one for x itself.


                           (mv (1+ (+ n1 n2))
                               (append syms1 syms2)
                               (append ints1 ints2)))))))
This use of multiple values to ``do several things at once'' is very common in ACL2. However, the function above is inefficient because it appends syms1 to syms2 and ints1 to ints2, copying the list structures of syms1 and ints1 in the process. By adding ``accumulators'' to the function, we can make the code more efficient. 
(defun count-and-collect1 (x n syms ints)
  (cond ((atom x)
         (cond ((symbolp x) (mv n (cons x syms) ints))
               ((integerp x) (mv n syms (cons x ints)))
               (t (mv n syms ints))))
        (t (mv-let (n2 syms2 ints2)
                   (count-and-collect1 (cdr x) (1+ n) syms ints)
                   (count-and-collect1 (car x) n2 syms2 ints2)))))
We claim that (count-and-collect x) returns the same triple of results as (count-and-collect1 x 0 nil nil). The reader is urged to study this claim until convinced that it is true and that the latter method of computing the results is more efficient. One might try proving the theorem 
(defthm count-and-collect-theorem
  (equal (count-and-collect1 x 0 nil nil) (count-and-collect x))).
Hint: the inductive proof requires attacking a more general theorem.

ACL2 does not support the Common Lisp construct multiple-value-bind, whose logical meaning seems difficult to characterize. Mv-let is the ACL2 analogue of that construct.