Perfect sharing

Stream: metaprogramming / tactics

[Mirek Olšák]

After talking with ATP people, I was curious if / how it would be possible to implement perfect sharing (also known as hash-consing) in Lean. perfect sharing means that we have some inductive type T (representing some kind of terms), however it is implemented so that

1. every time a constructor of T is called, it does a lookup into a global hash-table if such object has been already constructed, and if it was, it outputs the cached value
2. equality check is done purely by pointer-equality
3. whenever we index with an element of T in a hash-table, we use the raw pointer of T as the hash
4. (bonus) the global hash table is a value-weak in the sense that it does not increase reference count for the object, but automatically removes an item if the value has been released from memory

If I understand correctly, many of these steps would have to be done as unsafe, especially hashing with a pointer value, right? On the other hand, I don't think we could get inconsistency from pointer equality as equality decision procedure under such setup.

[Henrik Böving]

This has existed for a long time in the form of the shareCommon function and related things and is routinely used in high performance meta programs such as grind or bv_decide developed by the FRO.

[Mirek Olšák]

Is there a documentation / basic example of how this is used?

[Henrik Böving]

If you just want to take an object graph and share it you call shareCommon. If you want to build a framework where you keep accumulating shared terms you use the ShareCommonT monad transformer on top of whatever monad you are working in for your framework and share through their associated functions. Once you are operating on shared terms you can use (unsafe) functions like ptrEq to compare things. SymM/GrindM are probably the prime users of this API at the moment.

[Mirek Olšák]

So the idea is that inside that monad, I would call a standard constructor, and then wrap the result with shareCommonM to build a shared object? I was a bit confused that in SymM, there is docs#Lean.Meta.Sym.shareCommonInc for gradually building objects but I don't see a global shareCommon alternative.

[Henrik Böving]

The particular way that SymM works with share common is designed slightly differently for performance reasons. If you know that the term is already mostly shared the benefit of certain optimizations that are done in shareCommon diminishes. Both of the operations are going to get you there though.