The first change concern the syntax of constraints in annotations. The following is now allowed:
- [own l : ty] (previously written [l @ &own<ty>]),
- [shr l : ty] (previously written [l @ &shr<ty>]),
- [frac β l : ty] (previously written [l @ &frac<β, ty>]).
- The old notations have been removed.

The second change is some renaming around singleton types and layouts:
- [singleton_val] is now called [value],
- [singleton_place] is now called [place],
- [LPtr] is now called [void_ptr] and is accessed with notation [void*],
- [LVoid] is now called [void_layout].
- The front end now accepts `void*` as an identifier.

The last change introduces a new Coq scope called [printing_sugar] that is only opened at the beginning of proofs in generated proof files. It defines printing notations intended at making the output of the tool closer to the syntax of the front end. In particular it defines the following notations:
- [own l : ty], [shr l : ty], [frac {β} l : ty],
- [uninit<ly>], [value<ly, v>], [place<l>], [&own<ty>], ...
- For each user-defined types a similar printing sugar is defined automatically.

Rodolphe Lepigre authored 4 years ago and Michael Sammler committed 4 years ago

This fixes the third point of #30.

Co-authored-by: Michael Sammler <msammler@mpi-sws.org>

Using [block_id] to refer to the first component of locations.

- Put stuff in sections in [lang.v].
- Renamed [mk_layout] into [Layout] (for uniformity).
- Renamed [it_min] and [it_max] into [max_int] and [min_int].
- Some other renamings on [int_type]-related stuff.
- Changed [max_int] to be the last representable integer.
- Turned [in_it_range] into an instance of [ElemOf].

Michael Sammler authored 4 years ago and Rodolphe Lepigre committed 4 years ago

Co-authored-by: Rodolphe Lepigre <lepigre@mpi-sws.org>