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)) ; bodyThe form above binds the three ``local variables,''
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
kis the number of local variables listed. Often however it is simply the application of a
Mv-letis 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
variare distinct variables,
termis a term that returns
kresults and mentions only variables bound in the environment containing the
bodyis a term mentioning only the
variand variables bound in the environment containing the
varimust occur in
bodyunless it is declared
ignorablein one of the optional
declareforms, unless this requirement is turned off; see set-ignore-ok. The value of the
mv-letterm is the result of evaluating
bodyin an environment in which the
variare bound, in order, to the
kresults obtained by evaluating
termin the environment containing the
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,
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)This use of a multiple value to ``do several things at once'' is very common in ACL2. However, the function above is inefficient because it appends
; 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)))))))
ints2, copying the list structures of
ints1in 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
Mv-let is the ACL2 analogue of that construct.