[memo] General Memo datatype

[ejgallego]

This is required for

• #348
• #363

[Alizter]

We discussed using Dune's memo back when we designed the current memo. What were the reasons we decided against?

I think that library is in pretty good shape, and we should vendor it (I can set that up easily).

[ejgallego]

Dune's memo does something different than what we need (and it is almost of the size of Flèche) Dune's memo does true memoization + scheduling, our memo.ml only does the memoization part.

Indeed, something like Memo or Incr could be useful in the future, as of today they won't work well I think, but I'm happy if someone wants to setup an experimental branch. But little to reap from Dune's memo given the base Coq API is linear.

What I mean by this issue is to turn our memo.ml into a more general (memoization-only) table, so we can:

• cache other stuff instead of just the current caches
• control the size (by keeping track of old values)

So this is more about implementing a fancier version of OCaml's Hashtbl. Maybe JS's core has something like that?

[ejgallego]

Actually it is not easy to control the size of a Hashtbl so that is one of the key difficulties here.

Computing the true size can take a long time, so I guess at some point we need some cleanup heuristics triggered by global Gc stats, I tried but it is not easy to design something that works smoothly.

I'm opening this issue indeed to see if someone else would like to try.