What generation condition for types?
Currently a new RefinedC type is automatically generated on a struct if either:
- it has a refinement (i.e., at least one
rc::refined_by
annotation), - it has a
rc::ptr_type
annotation (in which case there can be norc::refined_by
, and the refinement isunit
).
One might wonder, can we relax this? And would this be useful in practice?
I have tried relaxing this behaviour but there is no obvious way to do this. The problem is that we explicitly rely on the fact that no types are generated in two cases:
- nested structs, as for
mpool_locked_inner
in https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/examples/mpool.c#L75, - and union cases (which are also nested structs), as
empty
in https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/examples/mutable_map.c#L22.
One solution is to add a rc::only_nested
annotation that instructs the front end not to generate a type. However that is a bit annoying in the case of unions. However there is no easy way to avoid this since the front end does not distinguish structs that are nested from those that appear at the top level.
Another possible solution (not tried yet) is to move the rc::union_tag
annotation into structs (and not have it as field annotation). This annotation would also disable the generation of a type, while keeping the information we need for the struct.