Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • RefinedC RefinedC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 21
    • Issues 21
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 3
    • Merge requests 3
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Metrics
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • RefinedCRefinedC
  • Merge requests
  • !16

Sugar in the front end + Coq pretty printing

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Rodolphe Lepigre requested to merge sugar into master Jan 13, 2021
  • Overview 17
  • Commits 12
  • Pipelines 0
  • Changes 256

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.
Edited Jan 15, 2021 by Rodolphe Lepigre
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: sugar