Alternative to cons that tries to avoid consing when a
This is a special purpose function that is intended to help with
reducing the memory usage of functions that modify existing cons tree
structures. Also see hons for a way to share cons structures;
What good is this? A fairly common operation in ACL2 is to ``change'' an existing data structure by consing together a new structure that is similar to it, but perhaps with some subtrees replaced. In many cases, some portion of the structure does not need to change.
For instance, consider a function like remove-equal, which updates
a list by removing all copies of some element from it. The definition of
(defun remove-equal (x l) (declare (xargs :guard (true-listp l))) (cond ((endp l) nil) ((equal x (car l)) (remove-equal x (cdr l))) (t (cons (car l) (remove-equal x (cdr l))))))
You can see that if
(defun remove-equal-with-hint (x l) (declare (xargs :guard (true-listp l))) (mbe :logic (remove-equal x l) :exec (cond ((endp l) nil) ((equal x (car l)) (remove-equal-with-hint x (cdr l))) (t (cons-with-hint (car l) (remove-equal-with-hint x (cdr l)) l)))))
This new version avoids consing in the case that we are not dropping an element. For example, at the time of this writing, we found the following memory usages on our copy of ACL2 built on CCL:
:q ;; 16 MB of memory allocated (let ((list (make-list 1000 :initial-element 0))) (time (loop for i from 1 to 1000 do (remove-equal i list)))) ;; 0 MB of memory allocated (let ((list (make-list 1000 :initial-element 0))) (time (loop for i from 1 to 1000 do (remove-equal-with-hint i list))))
This memory usage is not very surprising when you consider that the list does not change when no removal takes place. For example (still in raw Lisp):
? (let ((x '(a b c d e))) (eq x (remove-equal-with-hint 3 x))) T ?
Note that ACL2 asks Lisp to inline calls of