au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

New Surface Syntax And Parser #324

Open zilinc opened 4 years ago

zilinc commented 4 years ago

Description

For some reason, we want to rewrite our surface syntax parser, and also take this opportunity to revise our surface syntax.

gteege commented 4 years ago

Just a contribution / proposal for an improved surface syntax: An expression with an "observed variable" <expr> !v is difficult to read, because the variable "banging" is at the end and v is always a valid variable from the context. Since <expr> may be arbitrary large and complex, it may be misleading when you first read <expr> and only realize afterwards that v has been made readonly. Even in the bilby fs code there are examples where <expr> has more than one line.

I propose the syntax let !v in <expr> instead (or additionally, to be upward compatible). Remarks: