HONS-COPY

Major Section:  HONS-AND-MEMOIZATION

This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.

In the logic, hons-copy is just the identity function; we leave it enabled and would think it odd to ever prove a theorem about it.

Under the hood, hons-copy does whatever is necessary to produce a normed version of X.

What might this involve?

If X is a symbol, character, or number, then it is already normed and nothing is done.

If X is a string, we check if any normed version of X already exists. If so, we return the already-normed version; otherwise, we install X as the normed version for all strings that are equal to X.

If X is a cons, we must determine if there is a normed version of X, or recursively construct and install one. Norming large cons trees can become expensive, but there are a couple of cheap cases. In particular, if X is already normed, or if large subtrees of X are already normed, then not much needs to be done. The slowest case is norming some large ACL2 cons structure that has no subtrees which are already normed.

Note that running hons-copy on an object that was created with cons is often slower than just using hons directly when constructing the object.