I was wondering if we could have 2 evar_info, one returned by
find_undefined and another one by
find_defined. In some sense move the
evar_body option type outside and have the general api
find return one or the other info.
We already have in the evar map distinct defined/undefined maps, I was thinking of making them carry different info. For example I expect we don't need to have the entire context/type once the evar is assigned.
Can anyone see a problem in doing that?
I've been looking at that recently, actually
I am 100% in favour of this change but there are parts of the code that are not ready yet IIRC
(I mean, if you just go for an isomorphism it's fine, but if you want to remove data it's going to be hard)
A good first step is to double check calls to
Evd.find, most of those are actually statically known to be calls to Evd.find_undefined
About dreams, I'd like, on the coq-elpi side, to build a weak map on the evar_info_unassigned. For this to work I need two things: one is to add a field which is the evar number (easy, to get a fast "hash") and another one would be to make it "immutable" (if the uvar body is hoisted, it is kind of like that). One thing that worries me is there are a few metadata which Coq may update (TC status for example). I don't know how far this can go..., if they can be hoisted as well...
I can't build a weak map on Evar.t because it is not boxed, but boxing it just for coq-elpi would be too much...
Of course we could decide we box them and make the evar map a weak map!
I have no idea if this would scale, but if it does it would solve a major problem of the current evar map, which implements a heap without a garbage collector.
It would also simplify many things, eg no need to roll back the evar map. But one would need to bench it...
I think it's very dangerous to implement the evarmap as a weak map. Clearly it's a heap and it's lacking a GC, but the lifetimes are not bound to the actual reachability of OCaml values. Rather, I'd prefer that we clearly expose a set of roots in the map and implement our own GC atop of that.
Not even mentioning the fact we have to marshal that stuff.
There is one moral root, the proof root. All other roots are the terms one builds before calling refine. I fail to see the danger.
Yes, marshaling sigma "as is" won't work.
it's an interesting experiment though, if ever you try this out I would be very eager to see the results
no, the one root theory is an illusion. We can (and we do) store data that can refer to evars outside of the proof term
That would be a potential leak, but won't be worse than today.
I prefer a leak to a Not_found
but you'd still have to make imperative copies from time to time, so it's not clear to me that it's going to be efficient when compared to a high-level GC
copies of what? I thought so, but actually no (as long as the evar counter is always increasing)
since it is weak, you can pull out of backtracking completely
how do you backtrack on assignment?
the whole API is designed around the immutability of the evarmap, you can't change that like that...
Sure you have to undo assignments (but the weak hash table can just stay there, outside the monad). Nevermind this point.
Each evar introduced by pretyping while type-checking a term is a root too, no?
Derive, Program, and mutual (co)fixpoints in interactive mode all introduce multiple roots too, right?
Last updated: Dec 07 2023 at 14:02 UTC