This will fix #313 (closed) when it is ready. But it is still work-in-progress.
I am posting this to get some early feedback. The key issue to solve is remembering which locations were previously allocated so that we can ensure they do not get reallocated. This is necessary to keep the meta mechanism sound.
The approach I took now is to make the heap be of type gmap loc (option val), and None represents "deallocated". I think this is cleaner in terms of language specification than the alternative of tracking a gset loc of deallocated locations -- the latter would require an invariant to make sure no location can be both allocated and deallocated. However, a heap of (option val) makes gen_heap a bit awkward to use. It's not too horrible though, just see for yourself.
@robbertkrebbers what do you think?