Overview
The HashCons Library supports the implementation of hashconsed representations of data structures. Such representations are useful to reduce space usage by sharing common substructures and to provide constanttime equality testing for large structures.
To use this library, you need to use a twolevel definition of your data structures. For example, we might define a hashcons representation of lambda terms as follows:
structure HC = HashCons
type var = HashConsString.obj
datatype term_node
= VAR of var
 LAM of (var * term)
 APP of (term * term)
withtype term = term_node HC.obj
And you need to define an equality function on your terms (this function can use the hashcons identity on subterms). For example, here is the equality function for our lambda terms:
fun eq (APP(t11, t12), APP(t21, t22)) = HC.same(t11, t21) andalso HC.same(t12, t22)
 eq (LAM(x, t1), LAM(y, t2)) = HC.same(x, y) andalso HC.same(t1, t2)
 eq (VAR x, VAR y) = HC.same(x, y)
 eq _ = false
With the equality function defined, we can then create a hashcons table:
val tbl = HC.new {eq = eq}
And define constructor functions:
val mkAPP = HC.cons2 tbl (0wx1, APP)
val mkLAM = HC.cons2 tbl (0wx3, LAM)
val mkVAR = HC.cons1 tbl (0wx7, VAR)
val var = HW.mk
Note that we pick successive prime numbers for the constructor hash codes. Using these constructors, we can construct the representation of the identity function "\(\lambda{} x . x\)" as follows:
mkLAM(var "x", mkVAR(var "x"))
In addition to term construction, this library also supports finite sets and maps using the unique hashcons codes as keys.
Contents
structure HashCons

The main module in the library, which defines the basic types and various utility functions.
structure HashConsAtom

Code to package the
Atom.atom
type as a hashconsed object. structure HashConsMap

Implements finite maps keyed by hashconsed objects.
structure HashConsString

Code to package the
string
type as a hashconsed object. structure HashConsSet

Implements finite sets of hashconsed objects.
functor HashConsGroundFn

A functor for implementing new leaf types as hashconsed objects.