From mboxrd@z Thu Jan 1 00:00:00 1970 Received: by pauillac.inria.fr; Wed, 16 Mar 94 20:40:25 +0100 Received: from concorde.inria.fr by pauillac.inria.fr; Wed, 16 Mar 94 18:02:44 +0100 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by concorde.inria.fr (8.6.7/8.6.6) with ESMTP id SAA22113 for ; Wed, 16 Mar 1994 18:02:42 +0100 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 16 Mar 1994 17:01:51 +0000 To: caml-list@pauillac.inria.fr Cc: John.Harrison@cl.cam.ac.uk Subject: Structure sharing Date: Wed, 16 Mar 94 17:01:12 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:120340:940316170214"@cl.cam.ac.uk> Sender: weis@pauillac.inria.fr 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.