Proposed change to naming convention for "dataful" `*G`s
Some of our *G
typeclasses are different than others: they contain not just inG
but actual relevant data; usually a gname
but in the case of irisG
also some further information about how the Iris program logic is being instantiated. These dataful classes come with a *PreG
that represent their inG
(dataless) part.
Dataful *G
s need to be treated differently, e.g. they have special initialization lemmas and they should not be bundled in library's *G
as that leads to duplication of said data. So I propose to adjust our naming convention such that one can tell from the name whether a *G
is dataful or not.
The new naming convention is up for bikeshedding; here are some proposals coming to my mind:
- We call the dataful class
*DataG
and itsinG
-only part*G
. So e.g.heapG
→heapDataG
andheapPreG
→heapG
. - We call the dataful class
*DataG
and itsinG
-only part*PreG
. So e.g.heapG
→heapDataG
;heapPreG
stays. - We call the dataful class
*DG
and itsinG
-only part*PreG
. So e.g.heapG
→heapDG
;heapPreG
stays.
I think I prefer (2) or (3) over (1) because it prevents confusion due to accidentally using the inG
-only part, and also because it is easier for migration since we don't reuse an old name for a different purpose.
@robbertkrebbers @tchajed @jtassaro what do you think?