Currently when declaring a new uninterpreted type, we can either write type Foo; (Foo is never allocated) or type Foo (allocated); (Foo is always allocated).
I propose to also allow
type Foo
allocated(x) if <boolean expression involving x>;
for example,
type Foo
allocated(x) if x != default<Foo>();
where default<T> is a library function.
One could also allow the existing type Foo (allocated);, and/or type Foo allocated; (perhaps), as shorthand for type Foo allocated(x) if true;.
For now, these "new" types are always represented in C as void *, with the default value mapping to NULL (although we might implement ways of generalising that in the future). But the point is, this proposal allows us to implement the common case where a NULL pointer means an unallocated value, and non-NULL means allocated.
Also update any existing code that is returning allocated things from C (e.g. the "game engine" in the chess example).
UPDATE 7-Jul-2024: The above syntax turned out to be a bit too complicated to implement. I have decided to change it to a simplified version where the only allowed syntax is the following:
type Foo; // No Foo value is allocated.
type Foo (allocated); // Every Foo value is allocated.
type Foo (allocated_if_not_default); // The "default" Foo value is unallocated, all other Foo values are allocated.
I.e. you cannot write general "allocated predicates", instead there are just 3 settings to choose from.
Currently when declaring a new uninterpreted type, we can either write
type Foo;(Foo is never allocated) ortype Foo (allocated);(Foo is always allocated).I propose to also allowfor example,wheredefault<T>is a library function.One could also allow the existingtype Foo (allocated);, and/ortype Foo allocated;(perhaps), as shorthand fortype Foo allocated(x) if true;.For now, these "new" types are always represented in C as
void *, with the default value mapping to NULL (although we might implement ways of generalising that in the future). But the point is, this proposal allows us to implement the common case where a NULL pointer means an unallocated value, and non-NULL means allocated.Also update any existing code that is returning allocated things from C (e.g. the "game engine" in the chess example).
UPDATE 7-Jul-2024: The above syntax turned out to be a bit too complicated to implement. I have decided to change it to a simplified version where the only allowed syntax is the following:
I.e. you cannot write general "allocated predicates", instead there are just 3 settings to choose from.