|
|
|---|
|
|
|
|---|
Set a candidate list to try and preserve existing conses when finishing an nrev.
Signature:
In the common use case where an nrev is accumulating a transformed list (as in a std::defprojection), sometimes it may be the case that few of the list elements are actually transformed. In these cases it may be desirable to return a list that has as many conses shared with the original list as possible. This way, fewer total conses are in your working footprint.
To support this, nrev allows setting a hint, which in such a case should just be the original, untransformed list.
In the logical story, this doesn't do anything but return the unchanged nrev. In the pure ACL2 implementation, it just sets an extra stobj field to the hint. However, in the optimized implementation, when there is a hint set, then before returning the final list, we check to see if it has a suffix in common with the hint, and if so, replace that suffix with the one from the hint. Therefore, we return something equal to the list we've accumulated, but with as many of the conses from the hint as possible.
Function:
(defun nrev$a-set-hint (a nrev$a) (declare (xargs :guard t) (ignore a)) (list-fix nrev$a))
Function:
(defun nrev$c-set-hint (a nrev$c) (declare (xargs :stobjs nrev$c)) (update-nrev$c-hint a nrev$c))