(hons x y) returns a normed object equal to (cons x y).
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 is just cons; we leave it enabled and would think
it odd to ever prove a theorem about it.
Under the hood, hons does whatever is necessary to ensure that its result
is normed.
What might this involve?
Since the car and cdr of any normed cons must be normed, we need to
hons-copy x and y. This requires little work if x and y are already
normed, but can be expensive if x or y contain large, un-normed cons
structures.
After that, we need to check whether any normed cons equal to (x . y)
already exists. If so, we return it; otherwise, we need to construct a new
cons for (x . y) and install it as the normed version of (x . y).
Generally speaking, these extra operations make hons much slower than
cons, even when given normed arguments.
