Calling multi-valued ACL2 functions
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,''
General Form: (mv-let (var1 ... vark) term body) or (mv-let (var1 ... vark) term (declare ...) ... (declare ...) body)
Here is an extended example that illustrates both the definition of a
multi-valued function and the use of
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 a multiple value to ``do several things at once'' is very
common in ACL2. However, the function above is inefficient because it appends
(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
(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