search

microsoft / Armada

Armada is a tool for writing, and proving correct, high-performance concurrent programs.
Other
137 stars 19 forks source link

Grammar railroad diagram #33

Open mingodad opened 3 years ago

mingodad commented 3 years ago

Looking for people using CocoR I found this project and I've done a experimental tool to convert CocoR grammars to a kind of EBNF understood by https://www.bottlecaps.de/rr/ui to generate railroad diagrams see bellow the converted and with some hand made changes of Armada.atg to allow view it at https://www.bottlecaps.de/rr/ui the order of the rules could be changed to a better view of the railroad diagrams. Copy and paste the EBNF bellow on https://www.bottlecaps.de/rr/ui tab Edit Grammar then switch to the tab View Diagram.

I implemented the generation of the Parser.ebnf on this fork of CocoR Csharp https://github.com/mingodad/CocoR-CSharp and you can download the railroad generator to generate offline using Java here https://www.bottlecaps.de/rr/download/rr-1.63-java8.zip (link from the https://www.bottlecaps.de/rr/ui on tab Welcome).

Coco.exe -genRREBNF Armada.atg
java -jar rr.war -out:Armada.atg.xhtml Parser.ebnf

Also any feedback on the CocoR extensions are welcome !

Cheers !

//
// EBNF generated by CocoR parser generator to be viewed with https://www.bottlecaps.de/rr/ui
//

//
// productions
//

Armada ::= ( "include" stringToken )* ( TopDecl )* EOF 
TopDecl ::= ( DeclModifier )* ( SubModuleDecl | ClassDecl | DatatypeDecl | NewtypeDecl | OtherTypeDecl | IteratorDecl | TraitDecl | ClassMemberDecl | RefinementConstraintDecl | ArmadaProofDecl ) 
DeclModifier ::= ( "abstract" | ghost | static | protected | "noaddr" ) 
SubModuleDecl ::= ( ( module | "layer" | "level" | "structs" | "proof" ) ( Attribute )* NoUSIdent ( dot NoUSIdent )* ( "using" NoUSIdent )? ( "refines" ModuleName )? lbrace ( TopDecl )* rbrace | import ( "opened" )? ModuleName ( ( QualifiedModuleExportSuffix )? | "=" QualifiedModuleExport | colon QualifiedModuleExport ) ( semi )? | export ( ExportIdent )? ( ( "provides" ( ModuleExportSignature ( comma ModuleExportSignature )* | star ) | "reveals" ( ModuleExportSignature ( comma ModuleExportSignature )* | star ) | "extends" ExportIdent ( comma ExportIdent )* ) )* ) 
ClassDecl ::= "struct" ( Attribute )* NoUSIdent ( GenericParameters )? ( "extends" Type ( comma Type )* )? lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
DatatypeDecl ::= ( datatype | codatatype ) ( Attribute )* NoUSIdent ( GenericParameters )? "=" ( verticalbar )? DatatypeMemberDecl ( verticalbar DatatypeMemberDecl )* ( TypeMembers )? 
NewtypeDecl ::= newtype ( Attribute )* NoUSIdent "=" ( NoUSIdent ( colon Type )? verticalbar Expression ( ( ghost )? witness Expression )? ( TypeMembers )? | Type ( TypeMembers )? ) 
OtherTypeDecl ::= type ( Attribute )* NoUSIdent ( TypeParameterCharacteristics )* ( GenericParameters )? ( "=" ( NoUSIdent ( colon Type )? verticalbar Expression ( ( ghost )? witness Expression )? | Type ) )? ( semi )? 
IteratorDecl ::= iterator ( Attribute )* NoUSIdent ( ( GenericParameters )? Formals ( ( "yields" | "returns" ) Formals )? | ellipsis ) ( IteratorSpec )* ( BlockStmt )? 
TraitDecl ::= trait ( Attribute )* NoUSIdent ( GenericParameters )? lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
ClassMemberDecl ::= ( FieldDecl | ConstantFieldDecl | FunctionDecl | MethodDecl | GlobalInvariantDecl | YieldPredicateDecl | UniversalStepConstraintDecl ) 
RefinementConstraintDecl ::= "refinement_constraint" stringToken 
ArmadaProofDecl ::= ( "refinement" NoUSIdent NoUSIdent | "include_file" stringToken ( "which_includes" stringToken ( comma stringToken )* )? | "import_module" NoUSIdent ( "which_imports" NoUSIdent ( comma NoUSIdent )* )? | "extra" NoUSIdent stringToken | "inductive_invariant" ( Attribute )* NoUSIdent ( stringToken )? ( "depends_on" NoUSIdent ( comma NoUSIdent )* )? | "use_regions" | "use_address_invariant" | "chl_invariant" ( Attribute )* NoUSIdent ( stringToken )? | "chl_local_invariant" ( Attribute )* NoUSIdent NoUSIdent ( stringToken )? | "chl_yield_pred" ( Attribute )* NoUSIdent ( stringToken )? | "chl_precondition" ( Attribute )* NoUSIdent NoUSIdent ( stringToken )? | "chl_postcondition" ( Attribute )* NoUSIdent NoUSIdent ( stringToken )? | "chl_loop_modifies" ( Attribute )* NoUSIdent NoUSIdent ( stringToken )? | "auxiliary" NoUSIdent stringToken stringToken stringToken stringToken | "weakening" ( LabelIdent ( comma LabelIdent )* )? | "starweakening" ( "statements" LabelIdent ( comma LabelIdent )* )? ( "variables" LabelIdent ( comma LabelIdent )* )? | "var_hiding" NoUSIdent ( comma NoUSIdent )* | "stack_var_hiding" NoUSIdent NoUSIdent ( comma NoUSIdent )* | "var_intro" NoUSIdent ( comma NoUSIdent )* | "stack_var_intro" NoUSIdent NoUSIdent ( stringToken )? | "reduction" ( "phase1" NoUSIdent ( "-" NoUSIdent )? ( comma NoUSIdent ( "-" NoUSIdent )? )* )? ( "phase2" NoUSIdent ( "-" NoUSIdent )? ( comma NoUSIdent ( "-" NoUSIdent )? )* )? | "combining" NoUSIdent NoUSIdent NoUSIdent | "field_hiding" NoUSIdent NoUSIdent | "field_intro" NoUSIdent NoUSIdent | "assume_intro" ( LabelIdent ( comma LabelIdent )* )? | "chl" | "critsec" NoUSIdent | "tso_elim" PeriodSeparatedIdentifierList stringToken ) 
Attribute ::= lbracecolon NoUSIdent ( Expressions )? rbrace 
NoUSIdent ::= ident 
ModuleName ::= Ident 
QualifiedModuleExportSuffix ::= ( dot ModuleName ( dot ModuleName )* | backtick ( ExportIdent | lbrace ExportIdent ( comma ExportIdent )* rbrace ) ) 
QualifiedModuleExport ::= ModuleName ( QualifiedModuleExportSuffix )? 
ExportIdent ::= FuMe_Ident 
ModuleExportSignature ::= TypeNameOrCtorSuffix ( dot TypeNameOrCtorSuffix )? 
TypeNameOrCtorSuffix ::= ( ident | digits ) 
Ident ::= ident 
GenericParameters ::= openAngleBracket ( Variance )? NoUSIdent ( TypeParameterCharacteristics )* ( comma ( Variance )? NoUSIdent ( TypeParameterCharacteristics )* )* closeAngleBracket 
Type ::= TypeAndToken 
GlobalInvariantDecl ::= invariant NoUSIdent FunctionBody 
FunctionBody ::= lbrace Expression rbrace 
YieldPredicateDecl ::= "yield_predicate" NoUSIdent FunctionBody 
UniversalStepConstraintDecl ::= "universal_step_constraint" NoUSIdent ( FunctionBody | stringToken ) 
LabelIdent ::= ( NoUSIdent | digits ) 
PeriodSeparatedIdentifierList ::= NoUSIdent ( dot NoUSIdent )* 
FieldDecl ::= var ( Attribute )* FIdentType ( gets Expression )? ( comma FIdentType ( gets Expression )? )* OldSemi 
ConstantFieldDecl ::= const ( Attribute )* CIdentType ( gets Expression )? OldSemi 
FunctionDecl ::= ( twostate )? ( function ( method )? ( Attribute )* FuMe_Ident ( ( GenericParameters )? Formals colon ( openparen GIdentType closeparen | Type ) | ellipsis ) | predicate ( method )? ( Attribute )* NoUSIdent ( ( GenericParameters )? ( Formals )? ( colon )? | ellipsis ) | inductive predicate ( Attribute )* FuMe_Ident ( ( GenericParameters )? ( KType )? Formals ( colon )? | ellipsis ) | copredicate ( Attribute )* NoUSIdent ( ( GenericParameters )? ( KType )? Formals ( colon )? | ellipsis ) ) ( FunctionSpec )* ( FunctionBody )? 
MethodDecl ::= ( method | lemma | colemma | "comethod" | inductive lemma | twostate lemma | constructor | "destructor" ) ( Attribute )* ( FuMe_Ident )? ( ( GenericParameters )? ( KType )? Formals ( "returns" Formals )? | ellipsis ) ( MethodSpec )* ( ( DividedBlockStmt | BlockStmt ) )? 
DatatypeMemberDecl ::= ( Attribute )* NoUSIdent ( FormalsOptionalIds )? 
TypeMembers ::= lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
FormalsOptionalIds ::= openparen ( TypeIdentOptional ( comma TypeIdentOptional )* )? closeparen 
FIdentType ::= ( WildIdent | digits ) colon Type 
Expression ::= EquivExpression ( semi Expression )? 
OldSemi ::= ( semi )? 
CIdentType ::= ( WildIdent | digits ) ( colon Type )? 
TypeParameterCharacteristics ::= openparen TPCharOption ( comma TPCharOption )* closeparen 
GIdentType ::= ( ( ghost | "new" ) )* IdentType 
IdentType ::= WildIdent colon Type 
WildIdent ::= ident 
LocalIdentTypeOptional ::= WildIdent ( colon Type )? 
IdentTypeOptional ::= WildIdent ( colon Type )? 
TypeIdentOptional ::= ( ghost )? ( TypeAndToken ( colon Type )? | digits colon Type ) 
TypeAndToken ::= ( bool | char | int | nat | real | ORDINAL | bvToken | set OptGenericInstantiation | iset OptGenericInstantiation | multiset OptGenericInstantiation | seq OptGenericInstantiation | "ptr" OptGenericInstantiation | string | object | object_q | map OptGenericInstantiation | imap OptGenericInstantiation | arrayToken OptGenericInstantiation | arrayToken_q OptGenericInstantiation | openparen ( Type ( comma Type )* )? closeparen | NameSegmentForTypeName ( dot TypeNameOrCtorSuffix OptGenericInstantiation )* ) ( lbracket Nat rbracket )? ( ( "~>" | "-->" | "->" ) Type )? 
Formals ::= openparen ( GIdentType ( comma GIdentType )* )? closeparen 
IteratorSpec ::= ( reads ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi | modifies ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi | ( "free" )? ( "yield" )? ( requires ( LabelIdent colon )? Expression OldSemi | ensures ( Attribute )* Expression OldSemi ) | decreases ( Attribute )* DecreasesList OldSemi ) 
BlockStmt ::= lbrace ( Stmt )* rbrace 
Variance ::= ( star | "+" | "!" | "-" ) 
TPCharOption ::= ( eq | digits | "!" "new" ) 
FuMe_Ident ::= ( NoUSIdent | digits ) 
KType ::= lbracket ( nat | ORDINAL ) rbracket 
MethodSpec ::= ( modifies ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi | ( "free" )? ( requires ( Attribute )* ( LabelIdent colon )? Expression OldSemi | ensures ( Attribute )* Expression OldSemi ) | decreases ( Attribute )* DecreasesList OldSemi | reads Expression ( comma Expression )* OldSemi | "awaits" Expression ( comma Expression )* OldSemi | "undefined_unless" Expression ( comma Expression )* OldSemi ) 
DividedBlockStmt ::= lbrace ( Stmt )* ( "new" semi ( Stmt )* )? rbrace 
FrameExpression ::= ( Expression ( backtick Ident )? | backtick Ident ) 
DecreasesList ::= PossiblyWildExpression ( comma PossiblyWildExpression )* 
OptGenericInstantiation ::= ( GenericInstantiation )? 
NameSegmentForTypeName ::= Ident OptGenericInstantiation 
Nat ::= ( digits | hexdigits ) 
GenericInstantiation ::= openAngleBracket Type ( comma Type )* closeAngleBracket 
FunctionSpec ::= ( requires ( Attribute )* Expression OldSemi | reads PossiblyWildFrameExpression ( comma PossiblyWildFrameExpression )* OldSemi | ensures ( Attribute )* Expression OldSemi | decreases DecreasesList OldSemi ) 
PossiblyWildFrameExpression ::= ( star | FrameExpression ) 
PossiblyWildExpression ::= ( star | Expression ) 
Stmt ::= OneStmt 
ExplicitYieldBlockStmt ::= ( "explicit_yield" | "atomic" ) lbrace ( Stmt )* rbrace 
OneStmt ::= ( BlockStmt | AssertStmt | AssumeStmt | PrintStmt | RevealStmt | SomehowStmt | FenceStmt | GotoStmt | CompareAndSwapStmt | AtomicExchangeStmt | DeallocStmt | CreateThreadStmt | UpdateStmt | VarDeclStatement | IfStmt | WhileStmt | MatchStmt | ForallStmt | CalcStmt | ModifyStmt | "label" LabelIdent colon OneStmt | "break" ( LabelIdent | ( "break" )* ) semi | "continue" semi | ReturnStmt | SkeletonStmt | JoinStmt | ExplicitYieldBlockStmt ) 
AssertStmt ::= "assert" ( Attribute )* ( ( LabelIdent colon )? Expression ( by BlockStmt | semi ) | ellipsis semi ) 
AssumeStmt ::= ( assume | "wait_until" ) ( Attribute )* ( Expression | ellipsis ) semi 
PrintStmt ::= "print" Expression ( comma Expression )* semi 
RevealStmt ::= reveal Expression ( comma Expression )* semi 
SomehowStmt ::= "somehow" ( ( "undefined_unless" Expression ( comma Expression )* | modifies ( Attribute )* Expression ( comma Expression )* | ensures Expression ) )* semi 
FenceStmt ::= "fence" semi 
GotoStmt ::= "goto" LabelIdent semi 
CompareAndSwapStmt ::= "compare_and_swap" openparen Expression comma Expression comma Expression closeparen semi 
AtomicExchangeStmt ::= "atomic_exchange" openparen Expression comma Expression closeparen semi 
DeallocStmt ::= "dealloc" Expression semi 
CreateThreadStmt ::= "create_thread" NoUSIdent openparen ( Expressions )? closeparen semi 
UpdateStmt ::= ( Lhs ( ( Attribute )* semi | ( comma Lhs )* ( ( gets | "::=" ) Rhs ( comma Rhs )* | boredSmiley ( assume )? Expression | ":-" Expression ) semi | colon ) | ":-" Expression semi ) 
VarDeclStatement ::= ( ghost )? ( "noaddr" )? var ( ( Attribute )* LocalIdentTypeOptional ( comma ( Attribute )* LocalIdentTypeOptional )* ( ( ( gets | "::=" ) Rhs ( comma Rhs )* | ( Attribute )* boredSmiley ( assume )? Expression | ":-" Expression ) )? semi | CasePatternLocal ( gets | ( Attribute )* boredSmiley ) Expression semi ) 
IfStmt ::= "if" ( AlternativeBlock | ( ExistentialGuard | Guard | ellipsis ) BlockStmt ( else ( IfStmt | BlockStmt ) )? ) 
WhileStmt ::= "while" ( ( LoopSpec )* AlternativeBlock | ( Guard | ellipsis ) ( LoopSpec )* ( BlockStmt | ellipsis | ) ) 
MatchStmt ::= "match" Expression ( lbrace ( CaseStatement )* rbrace | ( CaseStatement )* ) 
ForallStmt ::= ( "forall" | "parallel" ) ( openparen ( QuantifierDomain )? closeparen | ( QuantifierDomain )? ) ( ( "free" )? ensures Expression OldSemi )* ( BlockStmt )? 
CalcStmt ::= calc ( Attribute )* ( CalcOp )? lbrace ( Expression semi ( CalcOp )? ( ( BlockStmt | CalcStmt ) )* )* rbrace 
ModifyStmt ::= "modify" ( Attribute )* ( FrameExpression ( comma FrameExpression )* | ellipsis ) ( BlockStmt | semi ) 
ReturnStmt ::= ( "return" | "yield" ) ( Rhs ( comma Rhs )* )? semi 
SkeletonStmt ::= ellipsis ( "where" Ident ( comma Ident )* gets Expression ( comma Expression )* )? semi 
JoinStmt ::= "join" Expression semi 
Rhs ::= ( "new" ( NewArray | TypeAndToken ( ( NewArray | openparen ( Expressions )? closeparen ) )? ) | star | Expression | "create_thread" NoUSIdent openparen ( Expressions )? closeparen | "malloc" openparen Type closeparen | "calloc" openparen Type comma Expression closeparen | "compare_and_swap" openparen Expression comma Expression comma Expression closeparen | "atomic_exchange" openparen Expression comma Expression closeparen ) ( Attribute )* 
Lhs ::= ( NameSegment ( Suffix )* | star Expression | ConstAtomExpression Suffix ( Suffix )* ) 
NewArray ::= lbracket ( rbracket lbracket ( Expressions )? rbracket | Expressions rbracket ( ( openparen Expression closeparen | lbracket ( Expressions )? rbracket ) )? ) 
Expressions ::= Expression ( comma Expression )* 
CasePatternLocal ::= ( Ident openparen ( CasePatternLocal ( comma CasePatternLocal )* )? closeparen | openparen ( CasePatternLocal ( comma CasePatternLocal )* )? closeparen | LocalIdentTypeOptional ) 
AlternativeBlock ::= ( lbrace ( AlternativeBlockCase )* rbrace | AlternativeBlockCase ( AlternativeBlockCase )* ) 
ExistentialGuard ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* boredSmiley Expression 
Guard ::= ( star | openparen star closeparen | Expression ) 
AlternativeBlockCase ::= case ( ExistentialGuard | Expression ) darrow ( Stmt )* 
LoopSpec ::= ( ( "free" )? invariant ( Attribute )* Expression OldSemi | ensures Expression OldSemi | decreases ( Attribute )* DecreasesList OldSemi | modifies ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi ) 
CaseStatement ::= case ( Ident ( openparen ( CasePattern ( comma CasePattern )* )? closeparen )? | openparen CasePattern ( comma CasePattern )* closeparen ) darrow ( Stmt )* 
CasePattern ::= ( Ident openparen ( CasePattern ( comma CasePattern )* )? closeparen | openparen ( CasePattern ( comma CasePattern )* )? closeparen | IdentTypeOptional ) 
QuantifierDomain ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* ( verticalbar Expression )? 
CalcOp ::= ( eq ( "#" lbracket Expression rbracket )? | openAngleBracket | closeAngleBracket | "<=" | ">=" | neq | neqAlt | "\u2264" | "\u2265" | EquivOp | ImpliesOp | ExpliesOp ) 
EquivOp ::= ( "<==>" | "\u21d4" ) 
ImpliesOp ::= ( "==>" | "\u21d2" ) 
ExpliesOp ::= ( "<==" | "\u21d0" ) 
AndOp ::= ( "&&" | "\u2227" ) 
OrOp ::= ( "||" | "\u2228" ) 
NegOp ::= ( "!" | "\u00ac" ) 
Forall ::= ( "forall" | "\u2200" ) 
Exists ::= ( "exists" | "\u2203" ) 
QSep ::= ( doublecolon | bullet ) 
EquivExpression ::= ImpliesExpliesExpression ( EquivOp ImpliesExpliesExpression )* 
ImpliesExpliesExpression ::= LogicalExpression ( ( ImpliesOp ImpliesExpression | ExpliesOp LogicalExpression ( ExpliesOp LogicalExpression )* ) )? 
LogicalExpression ::= ( AndOp RelationalExpression ( AndOp RelationalExpression )* | OrOp RelationalExpression ( OrOp RelationalExpression )* | RelationalExpression ( ( AndOp RelationalExpression ( AndOp RelationalExpression )* | OrOp RelationalExpression ( OrOp RelationalExpression )* ) )? ) 
ImpliesExpression ::= LogicalExpression ( ImpliesOp ImpliesExpression )? 
RelationalExpression ::= ShiftTerm ( RelOp ShiftTerm ( RelOp ShiftTerm )* )? 
ShiftTerm ::= Term ( ( openAngleBracket openAngleBracket | closeAngleBracket closeAngleBracket ) Term )* 
RelOp ::= ( eq ( "#" lbracket Expression rbracket )? | openAngleBracket | closeAngleBracket | "<=" | ">=" | neq ( "#" lbracket Expression rbracket )? | in | notIn | "!" ( "!" )? | neqAlt | "\u2264" | "\u2265" ) 
Term ::= Factor ( AddOp Factor )* 
Factor ::= BitvectorFactor ( MulOp BitvectorFactor )* 
AddOp ::= ( "+" | "-" ) 
BitvectorFactor ::= AsExpression ( ( "&" AsExpression ( "&" AsExpression )* | verticalbar AsExpression ( verticalbar AsExpression )* | "^" AsExpression ( "^" AsExpression )* ) )? 
MulOp ::= ( star | "/" | "%" ) 
AsExpression ::= UnaryExpression ( as TypeAndToken )* 
UnaryExpression ::= ( "-" UnaryExpression | NegOp UnaryExpression | "&" UnaryExpression | star UnaryExpression | map MapDisplayExpr ( Suffix )* | imap MapDisplayExpr ( Suffix )* | iset ISetDisplayExpr ( Suffix )* | LambdaExpression | EndlessExpression | NameSegment ( Suffix )* | DisplayExpr ( Suffix )* | MultiSetExpr ( Suffix )* | SeqConstructionExpr ( Suffix )* | ConstAtomExpression ( Suffix )* ) 
MapDisplayExpr ::= lbracket ( MapLiteralExpressions )? rbracket 
Suffix ::= ( dot ( openparen MemberBindingUpdate ( comma MemberBindingUpdate )* closeparen | DotSuffix ( GenericInstantiation | HashCall | ) ) | lbracket ( Expression ( ".." ( Expression )? | gets Expression | colon ( Expression ( colon Expression )* ( colon )? )? | ( comma Expression )* ) | ".." ( Expression )? ) rbracket | openparen ( Expressions )? closeparen ) 
ISetDisplayExpr ::= lbrace ( Expressions )? rbrace 
LambdaExpression ::= ( WildIdent | openparen ( IdentTypeOptional ( comma IdentTypeOptional )* )? closeparen ) ( ( reads PossiblyWildFrameExpression ( comma PossiblyWildFrameExpression )* | requires Expression ) )* LambdaArrow Expression 
EndlessExpression ::= ( "if" ( ExistentialGuard | Expression ) then Expression else Expression | MatchExpression | QuantifierGuts | set SetComprehensionExpr | iset SetComprehensionExpr | StmtInExpr Expression | LetExpr | map MapComprehensionExpr | imap MapComprehensionExpr | reveal Expression | NamedExpr ) 
NameSegment ::= Ident ( GenericInstantiation | HashCall | ) 
DisplayExpr ::= ( lbrace ( Expressions )? rbrace | lbracket ( Expressions )? rbracket ) 
MultiSetExpr ::= multiset ( lbrace ( Expressions )? rbrace | openparen Expression closeparen ) 
SeqConstructionExpr ::= seq openparen Expression comma Expression closeparen 
ConstAtomExpression ::= ( "false" | "true" | "null" | Nat | Dec | charToken | stringToken | "this" | "$me" | "$sb_empty" | "$state" | "fresh" openparen Expression closeparen | "allocated" openparen Expression closeparen | "allocated_array" openparen Expression closeparen | "if_undefined" openparen Expression comma Expression closeparen | "global_view" openparen Expression closeparen | "unchanged" ( "@" LabelIdent )? openparen FrameExpression ( comma FrameExpression )* closeparen | "old" ( "@" LabelIdent )? openparen Expression closeparen | verticalbar Expression verticalbar | ( int | real ) openparen Expression closeparen | ParensExpression ) 
Dec ::= decimaldigits 
ParensExpression ::= openparen ( Expressions )? closeparen 
LambdaArrow ::= darrow 
MapLiteralExpressions ::= Expression gets Expression ( comma Expression gets Expression )* 
MapComprehensionExpr ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* ( verticalbar Expression )? QSep Expression ( gets Expression )? 
MatchExpression ::= "match" Expression ( lbrace ( CaseExpression )* rbrace | ( CaseExpression )* ) 
QuantifierGuts ::= ( Forall | Exists ) QuantifierDomain QSep Expression 
SetComprehensionExpr ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* verticalbar Expression ( QSep Expression )? 
StmtInExpr ::= ( AssertStmt | AssumeStmt | CalcStmt ) 
LetExpr ::= ( LetExprWithLHS | LetExprWithoutLHS ) 
NamedExpr ::= "label" NoUSIdent colon Expression 
LetExprWithLHS ::= ( ghost )? var CasePattern ( comma CasePattern )* ( gets | ( Attribute )* boredSmiley | ":-" ) Expression ( comma Expression )* semi Expression 
LetExprWithoutLHS ::= ":-" Expression semi Expression 
CaseExpression ::= case ( Ident ( openparen ( CasePattern ( comma CasePattern )* )? closeparen )? | openparen CasePattern ( comma CasePattern )* closeparen ) darrow Expression 
HashCall ::= "#" ( GenericInstantiation )? lbracket Expression rbracket openparen ( Expressions )? closeparen 
MemberBindingUpdate ::= ( ident | digits ) gets Expression 
DotSuffix ::= ( ident | digits | decimaldigits | requires | reads ) 

//
// tokens
//

bool ::= "bool"
char ::= "char"
int ::= "int"
nat ::= "nat"
real ::= "real"
ORDINAL ::= "ORDINAL"
object ::= "object"
object_q ::= "object?"
string ::= "string"
set ::= "set"
iset ::= "iset"
multiset ::= "multiset"
seq ::= "seq"
map ::= "map"
imap ::= "imap"
colon ::= ":"
comma ::= ","
verticalbar ::= "|"
doublecolon ::= "::"
gets ::= ":="
boredSmiley ::= ":|"
bullet ::= "\u2022"
dot ::= "."
backtick ::= "`"
semi ::= ";"
darrow ::= "=>"
assume ::= "assume"
calc ::= "calc"
case ::= "case"
then ::= "then"
else ::= "else"
as ::= "as"
by ::= "by"
in ::= "in"
decreases ::= "decreases"
invariant ::= "invariant"
function ::= "function"
predicate ::= "predicate"
inductive ::= "inductive"
twostate ::= "twostate"
copredicate ::= "copredicate"
lemma ::= "lemma"
static ::= "static"
protected ::= "protected"
import ::= "import"
export ::= "export"
class ::= "class"
trait ::= "trait"
datatype ::= "datatype"
codatatype ::= "codatatype"
var ::= "var"
const ::= "const"
newtype ::= "newtype"
type ::= "type"
iterator ::= "iterator"
method ::= "method"
colemma ::= "colemma"
constructor ::= "constructor"
modifies ::= "modifies"
reads ::= "reads"
requires ::= "requires"
ensures ::= "ensures"
ghost ::= "ghost"
witness ::= "witness"
lbracecolon ::= "{:"
lbrace ::= "{"
rbrace ::= "}"
lbracket ::= "["
rbracket ::= "]"
openparen ::= "("
closeparen ::= ")"
openAngleBracket ::= "<"
closeAngleBracket ::= ">"
eq ::= "=="
neq ::= "!="
neqAlt ::= "\u2260"
star ::= "*"
ellipsis ::= "..."
reveal ::= "reveal"
module ::= "module"
commit ::= "commit"
jaylorch commented 3 years ago

Wow, this is fantastic. Thanks!