		Search-engine friendly clone of the ACL2 documentation.

Hons-sublis

memoized version of SUBLIS which uses fast-alists.

(hons-sublis fal x) is like sublis, but may be faster in two ways.

It uses hons-get instead of assoc, which may provide a speedup when the alist in question is very long. Note that for good performance, the fast-alist argument, fal, must be a valid fast-alist.
It uses a memoized auxiliary function, which may provide a speedup when the tree argument, x, contains large, shared structures.

Definitions and Theorems

Function: hons-sublis

(defun hons-sublis (fal x)
  (declare (xargs :guard t))
  (let ((ret (hons-sublis-aux fal x)))
    (prog2$ (clear-memoize-table 'hons-sublis-aux)
            ret)))

Theorem: hons-sublis-removal

(defthm hons-sublis-removal
  (implies (alistp fal)
           (equal (hons-sublis fal x)
                  (sublis fal x))))

Subtopics

Hons-sublis-aux: Memoized core of hons-sublis.