stainless
stainless copied to clipboard
Add erasure of AnyHeapRef-bounded type parameters and better allocator examples
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 it is more likely to get merged if it targets main
branch