`(hons-copy x)`

returns a normed object that is equal to X.
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.