GitLab

This MR introduces several changes intended to make RefinedC more user-friendly.

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 notation has 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 has notation void*,
• LVoid is now called void_layout.
• Additionally, 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 an associated printing sugar is defined automatically.