Final step to extract the elements from an nrev.
Signature: (nrev-finish nrev) → (mv list
In the logic, this returns (list-fix nrev) as list, and also
updates nrev' := nil.
In the pure ACL2 implementation, this function is very much like nrev-copy. The underlying representation of nrev keeps the elements in
reverse order, so nrev-finish has to reverse them, e.g., via reverse, which of course is O(n).
In the optimized implementation, we have already constructed the list in
reverse order, so we can simply return it, saving all that consing. For this
to be sound, we must simultaneously clear out nrev—otherwise, a
subsequent nrev-push would be destructively modifying conses that are
visible elsewhere in the program.
Definitions and Theorems
(defun nrev$a-finish (nrev$a)
(declare (xargs :guard t))
(let* ((elems (list-fix nrev$a)))
(mv elems nil)))
(defun nrev$c-finish (nrev$c)
(declare (xargs :stobjs nrev$c))
(let* ((elems (reverse (nrev$c-acc nrev$c)))
(nrev$c (update-nrev$c-acc nil nrev$c)))
(mv elems nrev$c)))