(hons-copy x)returns a normed object that is equal to X.
Major Section: 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
is often slower than just using
hons directly when constructing the