		Search-engine friendly clone of the ACL2 documentation.

Nrev

Nrev-finish

Final step to extract the elements from an nrev.

Signature: (nrev-finish nrev) → (mv list nrev')

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

Function: nrev$a-finish

(defun nrev$a-finish (nrev$a)
  (declare (xargs :guard t))
  (let* ((elems (list-fix nrev$a)))
    (mv elems nil)))

Function: nrev$c-finish

(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)))