Mv-nth
The mv-nth element (zero-based) of a list
(Mv-nth n l) is the nth element of l, zero-based.
If n is greater than or equal to the length of l, then mv-nth
returns nil.
(Mv-nth n l) has a guard that n is a non-negative
integer.
Mv-nth is equivalent to the Common Lisp function nth (although
without the guard condition that the list is a true-listp), but is
used by ACL2 to access the nth value returned by a multiply valued expression.
So, if you do proofs about functions that involve mv-let, you may see
calls of mv-nth in the prover output. For example, the following are
logically equivalent:
(mv-let (n1 n2)
(mv (+ x y) (* x y))
(- n1 n2))
(let ((var (list (+ x y) (* x y))))
(let ((n1 (mv-nth 0 var))
(n2 (mv-nth 1 var)))
(- n1 n2)))
Here is a similar such example involving the ACL2 state. The
following two forms are logically equivalent, but the second is only legal in
contexts such as theorems (and proofs) rather than function definitions, since
it violates single-threadedness restrictions (more on this below; also see
state and see stobj).
(mv-let (erp val state)
(read-object ch state)
(value (list erp val)))
(let ((erp (mv-nth 0 (read-object ch state)))
(val (mv-nth 1 (read-object ch state)))
(state (mv-nth 2 (read-object ch state))))
(value (list erp val)))
Mv-nth is given some special treatment by the prover. To control that
behavior see theories-and-primitives.
Finally, we elaborate on the single-threadedness issue above. If EXPR
is an expression that is multiply valued, then the form (mv-nth n EXPR)
is illegal both in definitions and in forms submitted directly to the ACL2
loop. Indeed, EXPR cannot be passed as an argument to any
function (mv-nth or otherwise) in such an evaluation context. The reason
is that ACL2 code compiled for execution does not actually create a list for
multiple value return; for example, the read-object call above logically
returns a list of length 3, but when evaluated, it instead stores its three
returned values without constructing a list. The upshot is that it is
generally best not to call mv-nth directly, but rather to use mv-let, which generates mv-nth calls for reasoning but not for Lisp
evaluation. However, if you really want to use mv-nth directly to access
a multiply-valued result, then — at the cost of computational efficiency
— you can use mv-list, writing (mv-nth n (mv-list k EXPR))
for suitable k, where mv-list converts a multiple value result into
the corresponding list; see mv-list.
Function: mv-nth
(defun mv-nth (n l)
(declare (xargs :guard (and (integerp n) (>= n 0))))
(if (atom l)
nil
(if (zp n)
(car l)
(mv-nth (- n 1) (cdr l)))))
