From mboxrd@z Thu Jan 1 00:00:00 1970 Received: by pauillac.inria.fr; Thu, 17 Mar 94 14:44:24 +0100 Received: from localhost.inria.fr by pauillac.inria.fr; Thu, 17 Mar 94 10:21:51 +0100 To: John Harrison Cc: caml-list@pauillac.inria.fr Subject: Re: Structure sharing In-Reply-To: Your message of Wed, 16 Mar 1994 17:01:12 +0000. <"swan.cl.cam.:120340:940316170214"@cl.cam.ac.uk> Date: Thu, 17 Mar 1994 10:21:51 +0100 Message-Id: <17303.763896111@pauillac.inria.fr> From: Chet Murthy Sender: weis@pauillac.inria.fr Hi, John, I also did some work recently with structure-sharing in Coq. Specifically, I wrote a caml-light generic hash-conser which walks the in-memory representation in an unsafe manner, "re-sharing" a datastructure. Since I don't have type information, I can't detect the fact that something's mutable, so this only works for purely applicative data. Whatever. Anyway, I had an application where I wanted to read something in off of disk, and then "un-share" it completely - walk it completely, so I could hash the leaves of the datastructure into a symbol table. But then, well, the datastructure is unshared - I ought to re-share it, no? Well, hash-consing was a modest loss on a reasonable-sized benchmark. That is, for Constructions at least, the datastructures are simple enough, and small enough, that hash-consing costs more than it is worth when it is done "globally" On the other hand, when I did it on the output of the type-checker, and the term which I fed as input (coupled, so that the type-checker's output will be hash-consed "onto" the term being type-checked), I got a slight speedup. All this to say that it probably isn't a big win either way, in caml-light, for Coq. --chet--