Make.1-X
Given an equivalence relation eq
, a hashconsing function is a function that associates the same canonical element to two elements related by eq
. Usually, the element chosen is canonical w.r.t. physical equality (==)
, so as to reduce memory consumption and enhance efficiency of equality tests.
In order to ensure canonicality, we need a way to remember the element associated to a class of equivalence; this is done using the table type generated by the Make
functor.
The actual hashconsing function. It should be compatible with eq
, that is eq x (snd @@ hashcons f x) = true
. It also returns the hash.
A comparison function. It is allowed to use physical equality on the sub-terms hashconsed by the hashcons
function, but it should be insensible to shallow copy of the compared object. It should be compatible with the hash returned by hashcons
, ie eq x y
implies fst @@ hashcons x = fst @@ hashcons y
.