stainless icon indicating copy to clipboard operation
stainless copied to clipboard

Add erasure of AnyHeapRef-bounded type parameters and better allocator examples

Open gsps opened this issue 3 years ago • 1 comments

This PR improves upon the existing AllocatorMono example by a) adding a variant AllocatorMonoAbstract that abstracts the implementation and simply gives a model of an allocator that could feasibly be used in client code, and b) AllocatorPolyAbstract, a generic variant of the allocator.

To achieve the latter, type parameters on classes and functions upper-bounded by AnyHeapRef are now erased during EffectElaboration.

Drive-by fixes of several bugs in EffectElaboration.

gsps avatar Jan 18 '22 18:01 gsps

@gsps it is more likely to get merged if it targets main branch

vkuncak avatar Jan 20 '22 18:01 vkuncak