Structure sharing

John Harrison (John.Harrison@cl.cam.ac.uk)
Wed, 16 Mar 94 17:01:12 +0000

To: caml-list@pauillac.inria.fr
Subject: Structure sharing
Date: Wed, 16 Mar 94 17:01:12 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:120340:940316170214"@cl.cam.ac.uk>

My research work is in theorem proving and I'm quite interested in the impact
on efficiency of structure-sharing the datatypes representing terms etc.

Has anyone tried implementing global hash consing in CAML? (That is, ensuring
that you never keep two distinct copies of any "cons cell".) Presumably this
would make the system slower in most applications (the faster EQ for structural
equality testing being overwhelmed by the slowness of constructors). But it
might make it much more usable on really small systems, which is consonant with
the CAML Light ideology.

Alternatively, how well would it work if I used the "hashtbl" library and did
everything myself for the datatypes I'm interested in? Am I making things non
GC-able by putting them in a hash table? How do the hash tables in "hashtbl"
work exactly?

Thanks,

John Harrison (jrh@cl.cam.ac.uk)

Hardware Verification Group
University of Cambridge Computer Laboratory
New Museums Site
Pembroke Street
Cambridge CB2 3QG
England.