Hons
(hons x y) returns a normed object equal to (cons x
y).
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.
Function: hons
(defun hons (x y)
(declare (xargs :guard t))
(cons x y))
Subtopics
- Normed
- Normed objects are ACL2 Objects that are "canonical" or "unique"
in a certain sense.
- Hons-note
- Notes about hons, especially pertaining to expensive resizing
operations
- Hons-resize
- (hons-resize ...) can be used to manually adjust the sizes of
the hash tables that govern which ACL2 Objects are considered normed.
- Hons-wash
- (hons-wash) is like gc$ but can also garbage collect
normed objects (CCL and GCL Only).
- Hons-clear
- (hons-clear gc) is a drastic garbage collection mechanism that
clears out the underlying Hons Space.
- Hons-copy
- (hons-copy x) returns a normed object that is equal to
X.
- Maybe-wash-memory
- Conditionally trigger a hons-wash and also clear-memoize-tables to reclaim memory. (CCL only; requires a
trust tag)
- Hons-equal
- (hons-equal x y) is a recursive equality check that optimizes
when parts of its arguments are normed.
- Hons-summary
- (hons-summary) prints basic information about the sizes of the
tables in the current Hons Space.
- Hons-equal-lite
- (hons-equal-lite x y) is a non-recursive equality check that
optimizes if its arguments are normed.
- Hons-sublis
- memoized version of SUBLIS which uses fast-alists.
- Hons-wash!
- A version of hons-wash for parallel execution
- Hons-clear!
- A version of hons-clear for parallel execution
- Hons-copy-persistent
- (hons-copy-persistent x) returns a normed object that is
equal to X and which will be re-normed after any calls to hons-clear.
