Nrev
A safe mechanism for implementing something like nreverse, for
writing tail-recursive functions that use less memory by avoiding the final
reverse step.
Motivation
To avoid stack overflows, you sometimes need tail-recursive executable
versions of your functions. These tail-recursive functions often produce their
elements in the reverse of the desired order. For instance, here is a basic,
tail-recursive map:
(defun map-exec (x acc)
(if (atom x)
acc
(map-exec (cdr x) (cons (f (car x)) acc))))
But this produces elements in the wrong order. To correct for this, you
might explicitly reverse the elements, e.g.,:
(defun map (x)
(mbe :logic (if (atom x)
nil
(cons (f (car x)) (map (cdr x))))
:exec (reverse (map-exec x nil))))
This successfully avoids stack overflows, but since reverse is
applicative, this approach allocates twice as many conses as the naive, non
tail-recursive version.
In Common Lisp, we could avoid this overhead using nreverse, a
destructive routine that can reverse a list in-place by swapping pointers. But
since nreverse is destructive, it wouldn't be sound to just make it
generally available in ACL2.
Even so, we would like to have something like nreverse that would allow
us to write tail-recursive versions of map without having to allocate
double the conses. In principle, it is okay to use nreverse here because
we are only tampering with fresh conses that are not reachable from anywhere
else in the program. (Well, that's almost true; if map-exec were memoized, then we could get into trouble.)
Solution
nrev is, we believe, a safe mechanism for writing tail-recursive
functions that can (at your option) avoid this double consing by using
destructive, under-the-hood operations.
Without trust tags, nrev is roughly on par with the ordinary
reverse based solution:
- Memory — same as reverse, i.e., still twice as many as the non
tail-recursive version.
- Runtime — perhaps around 1.3x worse than reverse due to the
ACL2::stobj overhead.
With a trust tag, nrev is roughly on par with the nreverse
solution:
- Memory — same as nreverse, i.e., avoids the double consing
problem.
- Runtime — perhaps around 1.25x worse than nreverse due to the
ACL2::stobj overhead, but still faster than a traditional reverse
based solution.
Loading nrev
For the pure ACL2 (no trust tags) version, you can use:
(include-book "centaur/nrev/pure" :dir :system)
For the optimized (trust tags) version, you can instead load:
(include-book "centaur/nrev/fast" :dir :system)
Note that it's perfectly fine to start with the pure book and then load the
fast version later. Loading the fast version will "retroactively" optimize
all functions that are based on nrev.
Using nrev
These books implement an abstract stobj called nrev. The logical story
is that nrev is just a list. The fundamental operation on nrev is
nrev-push, which logically conses "onto the right," like rcons.
Once you have pushed the desired elements, you can get them back out in queue
order using nrev-finish.
See nrev-demo for a basic example.
Subtopics
- Nrev-set-hint
- Set a candidate list to try and preserve existing conses when finishing an nrev.
- Nrev-finish
- Final step to extract the elements from an nrev.
- Nrev-copy
- Slow operation to copy the current contents of nrev, without
destroying it.
- Nrev-push
- Fundamental operation to extend nrev with a new element.
- Nrev-fix
- Identity function for nrev.
- Nrev-demo
- Short demonstration of using nrev for a basic map function.
- Nrev-stobj
- Definition of the nrev abstract stobj.
- Nrev2
- An extra nrev created with ACL2::defstobj-clone.
- Nrev-append
- Add several elements into nrev at once.
- With-local-nrev
- Wrapper for with-local-stobj for common cases of using nrev.
- Nrev$c
- The concrete nrev stobj.
