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--