Skip to content

track has_lc directly in invGS/irisGS/heapGS rather than via separate typeclass

Ralf Jung requested to merge jung/iris:has-lc into master

When I tried to make heapGS be credit-enabled by default (!809 (closed)), I realized the current scheme of using a HasLc typeclass does not work as well as we had hoped.

So here's an alternative that @robbertkrebbers and me came up with: add a has_lc parameter to invGS/irisGS/heapGS that tracks whether this instance of the logic has later credits or not. The existing short names invGS/irisGS/heapGS refer to having credits; new invGS_gen/etc can be sued to be generic over whether credits are present or to state the absence of credits (for some juicy fupd-plainly-rules).

This seems to work as intended, all the HeapLang examples now implicitly have credits available. (Not that they can do much with that, but one day... ;) @lgaeher @simonspies what do you think?

Merge request reports