search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.9k stars 260 forks source link

Grammar railroad diagram #1244

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 Dafny.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.

Cheers !

//"/*" "*/" "//" lf cr  '+' lf  '+' tab
Dafny ::=  ( "include" stringToken  )*  ( TopDecl  )* SYNC EOF
DeclModifier ::=  ( "abstract"  | "ghost"  | "static"  | "protected"  )
TopDecl ::=  ( DeclModifier  )*  ( SubModuleDecl  | ClassDecl  | DatatypeDecl  | NewtypeDecl  | SynonymTypeDecl  | IteratorDecl  | TraitDecl  | ClassMemberDecl  )
SubModuleDecl ::=  ( ModuleDefinition  | ModuleImport  | ModuleExport  )
ModuleDefinition ::= "module"  ( Attribute  )* ModuleQualifiedName  ( "refines" ModuleQualifiedName  | Ident  )? SYNC "{"  ( TopDecl  )* "}"
ModuleImport ::= "import"  ( "opened"  )?  ( ModuleName "=" QualifiedModuleExport  | ModuleName ":" QualifiedModuleExport  | QualifiedModuleExport  )
ExportId ::= NoUSIdentOrDigits
ModuleExport ::= "export"  ( ExportId  )?  ( ellipsis  )?  ( "provides"  (  ( ExportSignature  ( "," ExportSignature  )*  )  | "*"  )  | "reveals"  (  ( ExportSignature  ( "," ExportSignature  )*  )  | "*"  )  | "extends" ExportId  ( "," ExportId  )*  )*
ExportSignature ::= TypeNameOrCtorSuffix  ( "." TypeNameOrCtorSuffix  )?
ModuleName ::= NoUSIdent
ModuleQualifiedName ::= ModuleName  ( "." ModuleName  )*
QualifiedModuleExport ::= ModuleQualifiedName  ( "`" ModuleExportSuffix  )?
ModuleExportSuffix ::=  ( ExportId  | "{" ExportId  ( "," ExportId  )* "}"  )
ClassName ::= NoUSIdent
ClassDecl ::= SYNC "class"  ( Attribute  )* ClassName  ( GenericParameters  )?  ( "extends" Type  ( "," Type  )*  | ellipsis  )? SYNC "{"  (  ( DeclModifier  )* ClassMemberDecl  )* "}"
TraitDecl ::= SYNC "trait"  ( Attribute  )* ClassName  ( GenericParameters  )?  ( "extends" Type  ( "," Type  )*  | ellipsis  )? "{"  (  ( DeclModifier  )* ClassMemberDecl  )* "}"
ClassMemberDecl ::=  ( FieldDecl  | ConstantFieldDecl  | FunctionDecl  | MethodDecl  )
DatatypeName ::= NoUSIdent
DatatypeDecl ::= SYNC  ( "datatype"  | "codatatype"  )  ( Attribute  )* DatatypeName  ( GenericParameters  )? "="  ( ellipsis  )?  ( "|"  )? DatatypeMemberDecl  ( "|" DatatypeMemberDecl  )*  ( TypeMembers  )?
DatatypeMemberName ::= NoUSIdentOrDigits
DatatypeMemberDecl ::=  ( Attribute  )* DatatypeMemberName  ( FormalsOptionalIds  )?
TypeMembers ::= "{"  (  ( DeclModifier  )* ClassMemberDecl  )* "}"
FieldDecl ::= SYNC "var"  ( Attribute  )* FIdentType  ( "," FIdentType  )* OldSemi
ConstantFieldDecl ::= SYNC "const"  ( Attribute  )* CIdentType  ( ellipsis  )?  ( ":=" Expression  )? OldSemi
NewtypeName ::= NoUSIdent
LocalVarName ::= NoUSIdent
NewtypeDecl ::= "newtype"  ( Attribute  )* NewtypeName "="  ( ellipsis  )?  ( LocalVarName  ( ":" Type  )? "|" Expression  (  ( "ghost" "witness" Expression  | "witness"  ( "*"  | Expression  )  )  )?  ( TypeMembers  )?  | Type  ( TypeMembers  )?  )
SynonymTypeName ::= NoUSIdent
SynonymTypeDecl ::= "type"  ( Attribute  )* SynonymTypeName  ( TypeParameterCharacteristics  )*  ( GenericParameters  )?  ( "="  ( LocalVarName  ( ":" Type  )? "|" Expression  (  ( "ghost" "witness" Expression  | "witness"  ( "*"  | Expression  )  )  )?  | Type  )  | ellipsis  ( TypeMembers  )?  | TypeMembers  )?
GIdentType ::=  ( "ghost"  | "new"  )* IdentType
FIdentType ::= NoUSIdentOrDigits ":" Type
CIdentType ::= NoUSIdentOrDigits  ( ":" Type  )?
IdentType ::= WildIdent ":" Type
LocalIdentTypeOptional ::= WildIdent  ( ":" Type  )?
IdentTypeOptional ::= WildIdent  ( ":" Type  )?
TypeIdentOptional ::=  ( "ghost"  )?  ( TypeAndToken  ( ":" Type  )?  | digits ":" Type  )
IteratorName ::= NoUSIdent
IteratorDecl ::= SYNC "iterator"  ( Attribute  )* IteratorName  (  ( GenericParameters  )? Formals  (  ( "yields"  | "returns"  ) Formals  )?  | ellipsis  ) IteratorSpec  ( BlockStmt  )?
TypeVariableName ::= NoUSIdent
GenericParameters ::= "<"  ( Variance  )? TypeVariableName  ( TypeParameterCharacteristics  )*  ( ","  ( Variance  )? TypeVariableName  ( TypeParameterCharacteristics  )*  )* ">"
Variance ::=  ( "*"  | "+"  | "!"  | "-"  )
TypeParameterCharacteristics ::= "(" TPCharOption  ( "," TPCharOption  )* ")"
TPCharOption ::=  ( "=="  | digits  | "!" "new"  )
MethodDecl ::= SYNC  ( "method"  | "lemma"  |  ( "greatest" "lemma"  | "colemma"  )  |  ( "least"  | "inductive"  ) "lemma"  | "twostate" "lemma"  | "constructor"  )  ( Attribute  )*  ( MethodFunctionName  )?  (  ( GenericParameters  )?  ( KType  )? Formals  ( "returns" Formals  )?  | ellipsis  ) MethodSpec  ( DividedBlockStmt  | BlockStmt  )?
KType ::= "["  ( "nat"  | "ORDINAL"  ) "]"
RequiresClause ::= "requires"  ( Attribute  )*  ( LabelName ":"  )? Expression OldSemi
EnsuresClause ::= "ensures"  ( Attribute  )* Expression OldSemi
ModifiesClause ::= "modifies"  ( Attribute  )* FrameExpression  ( "," FrameExpression  )* OldSemi
DecreasesClause ::= "decreases"  ( Attribute  )* DecreasesList OldSemi
ReadsClause ::= "reads"  ( Attribute  )* PossiblyWildFrameExpression  ( "," PossiblyWildFrameExpression  )* OldSemi
InvariantClause ::= "invariant"  ( Attribute  )* Expression OldSemi
MethodSpec ::= SYNC  ( ModifiesClause  | RequiresClause  | EnsuresClause  | DecreasesClause  )*
IteratorSpec ::= SYNC  ( ReadsClause  | ModifiesClause  |  ( "yield"  )?  ( RequiresClause  | EnsuresClause  )  | DecreasesClause  )*
Formals ::= "("  ( GIdentType  ( "," GIdentType  )*  )? ")"
FormalsOptionalIds ::= "("  ( TypeIdentOptional  ( "," TypeIdentOptional  )*  )? ")"
Type ::= TypeAndToken
TypeAndToken ::=  ( "bool"  | "char"  | "int"  | "nat"  | "real"  | "ORDINAL"  | bvToken  | "set" OptGenericInstantiation  | "iset" OptGenericInstantiation  | "multiset" OptGenericInstantiation  | "seq" OptGenericInstantiation  | "string"  | "object"  | "object?"  | "map" OptGenericInstantiation  | "imap" OptGenericInstantiation  | arrayToken OptGenericInstantiation  | TupleType  | NamedType  )  (  ( "~>"  | "-->"  | "->"  ) Type  )?
TupleType ::= "("  ( Type  ( "," Type  )*  )? ")"
NamedType ::= NameSegmentForTypeName  ( "." TypeNameOrCtorSuffix OptGenericInstantiation  )*
OptGenericInstantiation ::=  ( GenericInstantiation  )?
GenericInstantiation ::= "<" Type  ( "," Type  )* ">"
FunctionDecl ::=  ( "twostate"  )?  ( "function"  ( "method"  )?  ( Attribute  )* MethodFunctionName  (  ( GenericParameters  )? Formals ":"  ( "(" GIdentType ")"  | Type  )  | ellipsis  )  | "predicate"  ( "method"  )?  ( Attribute  )* MethodFunctionName  (  ( GenericParameters  )?  ( Formals  )?  ( ":" Type  )?  | ellipsis  )  |  ( "least"  | "inductive"  ) "predicate"  ( Attribute  )* MethodFunctionName  (  ( GenericParameters  )?  ( KType  )? Formals  ( ":"  )?  | ellipsis  )  |  ( "greatest" "predicate"  | "copredicate"  )  ( Attribute  )* MethodFunctionName  (  ( GenericParameters  )?  ( KType  )? Formals  ( ":"  )?  | ellipsis  )  ) FunctionSpec  ( FunctionBody  )?
FunctionSpec ::= SYNC  ( RequiresClause  | ReadsClause  | EnsuresClause  | DecreasesClause  )*
PossiblyWildExpression ::=  ( "*"  | Expression  )
PossiblyWildFrameExpression ::=  ( "*"  | FrameExpression  )
FrameField ::= "`" IdentOrDigits
FrameExpression ::=  ( Expression  ( FrameField  )?  | FrameField  )
FunctionBody ::= "{" Expression "}"
BlockStmt ::= "{"  ( Stmt  )* "}"
DividedBlockStmt ::= "{"  ( Stmt  )*  ( "new" ";"  ( Stmt  )*  )? "}"
Stmt ::= OneStmt
OneStmt ::= SYNC  ( BlockStmt  | UpdateStmt  | VarDeclStatement  | ReturnStmt  | IfStmt  | WhileStmt  | AssertStmt  | AssumeStmt  | BreakStmt  | CalcStmt  | ExpectStmt  | ForallStmt  | LabeledStmt  | MatchStmt  | ModifyStmt  | PrintStmt  | RevealStmt  | SkeletonStmt  | YieldStmt  )
LabeledStmt ::= "label" LabelName ":" OneStmt
SkeletonStmt ::= ellipsis ";"
BreakStmt ::= "break"  ( LabelName  |  ( "break"  )*  ) SYNC ";"
ReturnStmt ::= "return"  ( Rhs  ( "," Rhs  )*  )? ";"
YieldStmt ::= "yield"  ( Rhs  ( "," Rhs  )*  )? ";"
UpdateStmt ::=  ( Lhs  (  ( Attribute  )* ";"  |  ( "," Lhs  )*  ( ":=" Rhs  ( "," Rhs  )*  | ":|"  ( "assume"  )? Expression  | ":-"  (  ( "expect"  | "assert"  | "assume"  )  )? Expression  ( "," Rhs  )*  ) ";"  | ":"  )  | ":-"  (  ( "expect"  | "assert"  | "assume"  )  )? Expression  ( "," Rhs  )* ";"  )
Rhs ::=  ( "new"  ( NewArray  | TypeAndToken  ( NewArray  | "("  ( ActualBindings  )? ")"  )?  )  | "*"  | Expression  )  ( Attribute  )*
NewArray ::= "["  ( "]" "["  ( Expressions  )? "]"  | Expressions "]"  ( "(" Expression ")"  | "["  ( Expressions  )? "]"  )?  )
VarDeclStatement ::=  ( "ghost"  )? "var"  (  ( Attribute  )* LocalIdentTypeOptional  ( ","  ( Attribute  )* LocalIdentTypeOptional  )*  ( ":=" Rhs  ( "," Rhs  )*  |  ( Attribute  )* ":|"  ( "assume"  )? Expression  | ":-"  (  ( "expect"  | "assert"  | "assume"  )  )? Expression  ( "," Rhs  )*  )? SYNC ";"  | CasePatternLocal  ( ":="  |  ( Attribute  )* ":|"  ) Expression ";"  )
IfStmt ::= "if"  ( AlternativeBlock  |  ( BindingGuard  | Guard  | ellipsis  ) BlockStmt  ( "else"  ( IfStmt  | BlockStmt  )  )?  )
AlternativeBlock ::=  ( "{"  ( AlternativeBlockCase  )* "}"  | AlternativeBlockCase  ( AlternativeBlockCase  )*  )
AlternativeBlockCase ::= "case"  ( BindingGuard  | Expression  ) "=>" SYNC  ( Stmt SYNC  )*
WhileStmt ::= "while"  ( LoopSpec AlternativeBlock  |  ( Guard  | ellipsis  ) LoopSpec  ( BlockStmt  | ellipsis  |  )  )
LoopSpec ::=  ( SYNC InvariantClause  | SYNC DecreasesClause  | SYNC ModifiesClause  )*
DecreasesList ::= PossiblyWildExpression  ( "," PossiblyWildExpression  )*
Guard ::=  ( "*"  | "(" "*" ")"  | Expression  )
BindingGuard ::= IdentTypeOptional  ( "," IdentTypeOptional  )*  ( Attribute  )* ":|" Expression
ExtendedPattern ::=  ( "("  ( ExtendedPattern  ( "," ExtendedPattern  )*  )? ")"  | Ident "("  ( ExtendedPattern  ( "," ExtendedPattern  )*  )? ")"  | PossiblyNegatedLiteralExpr  | IdentTypeOptional  )
MatchStmt ::= "match" Expression  ( "{"  ( CaseStmt  )* "}"  |  ( CaseStmt  )*  )
CaseStmt ::= "case" ExtendedPattern "=>" SYNC  ( Stmt SYNC  )*
AssertStmt ::= "assert"  ( Attribute  )*  (  ( LabelName ":"  )? Expression  ( "by" BlockStmt  | ";"  )  | ellipsis ";"  )
ExpectStmt ::= "expect"  ( Attribute  )*  ( Expression  | ellipsis  )  ( "," Expression  )? ";"
AssumeStmt ::= "assume"  ( Attribute  )*  ( Expression  | ellipsis  ) ";"
PrintStmt ::= "print" Expression  ( "," Expression  )* ";"
RevealStmt ::= "reveal" Expression  ( "," Expression  )* ";"
ForallStmt ::= "forall"  ( "("  ( QuantifierDomain  )? ")"  |  ( QuantifierDomain  )?  )  ( EnsuresClause  )*  ( BlockStmt  )?
ModifyStmt ::= "modify"  ( Attribute  )*  ( FrameExpression  ( "," FrameExpression  )*  | ellipsis  )  ( BlockStmt  | SYNC ";"  )
CalcStmt ::= "calc"  ( Attribute  )*  ( CalcOp  )? "{"  ( Expression ";"  ( CalcOp  )?  (  ( BlockStmt  | CalcStmt  )  )*  )* "}"
CalcOp ::=  ( "=="  ( "#" "[" Expression "]"  )?  | "<"  | ">"  | "<="  | ">="  | "!="  | '\u2260'  | '\u2264'  | '\u2265'  | EquivOp  | ImpliesOp  | ExpliesOp  )
EquivOp ::= "<==>"  | '\u21d4'
ImpliesOp ::= "==>"  | '\u21d2'
ExpliesOp ::= "<=="  | '\u21d0'
AndOp ::= "&&"  | '\u2227'
OrOp ::= "||"  | '\u2228'
NegOp ::= "!"  | '\u00ac'
Forall ::= "forall"  | '\u2200'
Exists ::= "exists"  | '\u2203'
QSep ::= "::"  | '\u2022'
Expression ::= EquivExpression  ( ";" Expression  )?
EquivExpression ::= ImpliesExpliesExpression  ( EquivOp ImpliesExpliesExpression  )*
ImpliesExpliesExpression ::= LogicalExpression  (  ( ImpliesOp ImpliesExpression  | ExpliesOp LogicalExpression  ( ExpliesOp LogicalExpression  )*  ( ImpliesOp  )?  )  )?
ImpliesExpression ::= LogicalExpression  ( ImpliesOp ImpliesExpression  )?  ( ExpliesOp  )?
LogicalExpression ::=  ( AndOp RelationalExpression  ( AndOp RelationalExpression  )*  ( OrOp  )?  | OrOp RelationalExpression  ( OrOp RelationalExpression  )*  ( AndOp  )?  | RelationalExpression  (  ( AndOp RelationalExpression  ( AndOp RelationalExpression  )*  ( OrOp  )?  | OrOp RelationalExpression  ( OrOp RelationalExpression  )*  ( AndOp  )?  )  )?  )
RelationalExpression ::= ShiftTerm  ( RelOp ShiftTerm  ( RelOp ShiftTerm  )*  )?
RelOp ::=  ( "=="  ( "#" "[" Expression "]"  )?  | "<"  | ">"  | "<="  | ">="  | "!="  ( "#" "[" Expression "]"  )?  | "in"  | notIn  | "!"  ( "!"  )?  | '\u2260'  | '\u2264'  | '\u2265'  )
ShiftTerm ::= Term  (  ( "<" "<"  | ">" ">"  ) Term  )*
Term ::= Factor  ( AddOp Factor  )*
AddOp ::=  ( "+"  | "-"  )
Factor ::= BitvectorFactor  ( MulOp BitvectorFactor  )*
MulOp ::=  ( "*"  | "/"  | "%"  )
BitvectorFactor ::= AsExpression  (  ( "&" AsExpression  ( "&" AsExpression  )*  (  ( "|"  | "^"  )  )?  | "|" AsExpression  ( "|" AsExpression  )*  (  ( "^"  | "&"  )  )?  | "^" AsExpression  ( "^" AsExpression  )*  (  ( "&"  | "|"  )  )?  )  )?
AsExpression ::= UnaryExpression  (  ( "as" TypeAndToken  | "is" TypeAndToken  )  )*
UnaryExpression ::=  ( "-" UnaryExpression  | NegOp UnaryExpression  | PrimaryExpression  )
PrimaryExpression ::=  ( MapDisplayExpr  ( Suffix  )*  | SetDisplayExpr  ( Suffix  )*  | LambdaExpression  | EndlessExpression  | NameSegment  ( Suffix  )*  | SeqDisplayExpr  ( Suffix  )*  | ConstAtomExpression  ( Suffix  )*  )
Lhs ::=  ( NameSegment  ( Suffix  )*  | ConstAtomExpression Suffix  ( Suffix  )*  )
ConstAtomExpression ::=  ( LiteralExpression  | "this"  | "fresh" "(" Expression ")"  | "allocated" "(" Expression ")"  | "unchanged"  ( "@" LabelName  )? "(" FrameExpression  ( "," FrameExpression  )* ")"  | "old"  ( "@" LabelName  )? "(" Expression ")"  | "|" Expression "|"  | ParensExpression  )
LiteralExpression ::=  ( "false"  | "true"  | "null"  | Nat  | Dec  | charToken  | stringToken  )
PossiblyNegatedLiteralExpr ::=  ( "-"  ( Nat  | Dec  )  | LiteralExpression  )
LambdaExpression ::=  ( WildIdent  | "("  ( IdentTypeOptional  ( "," IdentTypeOptional  )*  )? ")"  ) LambdaSpec "=>" Expression
LambdaSpec ::=  ( ReadsClause  | "requires"  ( Attribute  )* Expression  )*
ParensExpression ::= "("  ( ActualBindings  )? ")"
SetDisplayExpr ::=  (  ( "iset"  | "multiset"  )  )?  ( "{"  ( Expressions  )? "}"  | "(" Expression ")"  )
SeqDisplayExpr ::=  ( "seq"  ( GenericInstantiation  )? "(" Expression "," Expression ")"  | "["  ( Expressions  )? "]"  )
MapDisplayExpr ::=  ( "map"  | "imap"  ) "["  ( MapLiteralExpressions  )? "]"
MapLiteralExpressions ::= Expression ":=" Expression  ( "," Expression ":=" Expression  )*
MapComprehensionExpr ::=  ( "map"  | "imap"  ) IdentTypeOptional  ( "," IdentTypeOptional  )*  ( Attribute  )*  ( "|" Expression  )? QSep Expression  ( ":=" Expression  )?
EndlessExpression ::=  ( IfExpression  | MatchExpression  | QuantifierExpression  | SetComprehensionExpr  | StmtInExpr Expression  | LetExpression  | MapComprehensionExpr  )
IfExpression ::= "if"  ( BindingGuard  | Expression  ) "then" Expression "else" Expression
StmtInExpr ::=  ( AssertStmt  | ExpectStmt  | AssumeStmt  | RevealStmt  | CalcStmt  )
LetExpression ::=  ( LetExprWithLHS  | LetExprWithoutLHS  )
LetExprWithLHS ::=  ( "ghost"  )? "var" CasePattern  ( "," CasePattern  )*  ( ":="  |  ( Attribute  )* ":|"  | ":-"  ) Expression  ( "," Expression  )* ";" Expression
LetExprWithoutLHS ::= ":-" Expression ";" Expression
MatchExpression ::= "match" Expression  ( "{"  ( CaseExpression  )* "}"  |  ( CaseExpression  )*  )
CaseExpression ::= "case" ExtendedPattern "=>" Expression
CasePattern ::=  ( Ident "("  ( CasePattern  ( "," CasePattern  )*  )? ")"  | "("  ( CasePattern  ( "," CasePattern  )*  )? ")"  | IdentTypeOptional  )
CasePatternLocal ::=  ( Ident "("  ( CasePatternLocal  ( "," CasePatternLocal  )*  )? ")"  | "("  ( CasePatternLocal  ( "," CasePatternLocal  )*  )? ")"  | LocalIdentTypeOptional  )
NameSegment ::= Ident  ( GenericInstantiation  ( AtCall  )?  | HashCall  |  ( AtCall  )?  )
NameSegmentForTypeName ::= Ident OptGenericInstantiation
HashCall ::= "#"  ( GenericInstantiation  )? "[" Expression "]" "("  ( ActualBindings  )? ")"
AtCall ::= "@" LabelName "("  ( ActualBindings  )? ")"
Suffix ::=  ( "."  ( "(" MemberBindingUpdate  ( "," MemberBindingUpdate  )* ")"  | DotSuffix  ( GenericInstantiation  ( AtCall  )?  | HashCall  |  ( AtCall  )?  )  )  | "["  ( Expression  ( ".."  ( Expression  )?  | ":=" Expression  | ":"  ( Expression  ( ":" Expression  )*  ( ":"  )?  )?  |  ( "," Expression  )*  )  | ".."  ( Expression  )?  ) "]"  | "("  ( ActualBindings  )? ")"  )
ActualBindings ::= ActualBinding  ( "," ActualBinding  )*
ActualBinding ::=  ( NoUSIdentOrDigits ":="  )? Expression
QuantifierExpression ::=  ( Forall  | Exists  ) QuantifierDomain QSep Expression
QuantifierDomain ::= IdentTypeOptional  ( "," IdentTypeOptional  )*  ( Attribute  )*  ( "|" Expression  )?
SetComprehensionExpr ::=  ( "set"  | "iset"  ) IdentTypeOptional  ( "," IdentTypeOptional  )*  ( Attribute  )* "|" Expression  ( QSep Expression  )?
Expressions ::= Expression  ( "," Expression  )*
AttributeName ::= NoUSIdent
Attribute ::= "{:" AttributeName  ( Expressions  )? "}"
Ident ::=  ( ident  | "least"  | "greatest"  )
DotSuffix ::=  ( Ident  | digits  | decimaldigits  | "requires"  | "reads"  )
NoUSIdent ::= Ident
IdentOrDigits ::=  ( Ident  | digits  )
NoUSIdentOrDigits ::=  ( NoUSIdent  | digits  )
MemberBindingUpdate ::= NoUSIdentOrDigits ":=" Expression
LabelName ::= NoUSIdentOrDigits
MethodFunctionName ::= NoUSIdentOrDigits
TypeNameOrCtorSuffix ::= IdentOrDigits
WildIdent ::= Ident
OldSemi ::=  ( SYNC ";"  )?
Nat ::=  ( digits  | hexdigits  )
Dec ::=  ( decimaldigits  )

letter ::= "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"
digit ::= "0123456789"
posDigit ::= "123456789"
posDigitFrom2 ::= "23456789"
hexdigit ::= "0123456789ABCDEFabcdef"
special ::= "'_?"
cr ::= '\r'
lf ::= '\n'
tab ::= '\t'
space ::= ' '
nondigit ::= letter  '+' special
idchar ::= nondigit  '+' digit
nonidchar ::= ANY  '-' idchar
nondigitMinusABTick ::= nondigit  '-' 'a'  '-' 'b'  '-' "'"
nondigitMinusQuery ::= nondigit  '-' '?'
idcharMinusA ::= idchar  '-' 'a'
idcharMinusR ::= idchar  '-' 'r'
idcharMinusY ::= idchar  '-' 'y'
idcharMinusV ::= idchar  '-' 'v'
idcharMinusPosDigitMinusQuery ::= idchar  '-' posDigit  '-' '?'
idcharMinusTick ::= idchar  '-' "'"
charChar ::= ANY  '-' "'"  '-' '\'  '-' cr  '-' lf
stringChar ::= ANY  '-' '"'  '-' '\'  '-' cr  '-' lf
verbatimStringChar ::= ANY  '-' '"'
ident  ::= nondigitMinusABTick  ( idchar  )*  | 'a'  ( idcharMinusR  ( idchar  )*  )?  | 'a' 'r'  ( idcharMinusR  ( idchar  )*  )?  | 'a' 'r' 'r'  ( idcharMinusA  ( idchar  )*  )?  | 'a' 'r' 'r' 'a'  ( idcharMinusY  ( idchar  )*  )?  | 'a' 'r' 'r' 'a' 'y' idcharMinusPosDigitMinusQuery  ( idchar  )*  | 'a' 'r' 'r' 'a' 'y' '1'  ( '?'  )?  | 'a' 'r' 'r' 'a' 'y' '?' idchar  ( idchar  )*  | 'a' 'r' 'r' 'a' 'y' posDigit  ( digit  )* nondigitMinusQuery  ( idchar  )*  | 'a' 'r' 'r' 'a' 'y' posDigit  ( digit  )* '?' idchar  ( idchar  )*  | 'b'  ( idcharMinusV  ( idchar  )*  )?  | 'b' 'v'  ( nondigit  ( idchar  )*  )?  | 'b' 'v' '0' idchar  ( idchar  )*  | 'b' 'v' posDigit  ( idchar  )* nondigit  ( idchar  )*  | "'"  ( idchar  )?  | "'" idchar idcharMinusTick  | "'" idchar idchar idchar  ( idchar  )*
digits  ::= digit  (  ( '_'  )? digit  )*
hexdigits  ::= "0x" hexdigit  (  ( '_'  )? hexdigit  )*
decimaldigits  ::= digit  (  ( '_'  )? digit  )* '.' digit  (  ( '_'  )? digit  )*
arrayToken  ::= "array"  (  ( '1' digit  | posDigitFrom2  )  ( digit  )*  )?  ( '?'  )?
bvToken  ::= "bv"  ( '0'  | posDigit  ( digit  )*  )
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"
charToken  ::= "'"  ( charChar  | "\'"  | '\"'  | "\\"  | "\0"  | "\n"  | "\r"  | "\t"  | "\u" hexdigit hexdigit hexdigit hexdigit  ) "'"
stringToken  ::= '"'  ( stringChar  | "\'"  | '\"'  | "\\"  | "\0"  | "\n"  | "\r"  | "\t"  | "\u" hexdigit hexdigit hexdigit hexdigit  )* '"'  | '@' '"'  ( verbatimStringChar  | '""'  )* '"'
colon  ::= ':'
comma  ::= ','
verticalbar  ::= '|'
doublecolon  ::= "::"
gets  ::= ":="
boredSmiley  ::= ":|"
bullet  ::= '\u2022'
dot  ::= '.'
backtick  ::= "`"
semicolon  ::= ';'
darrow  ::= "=>"
assume  ::= "assume"
assert  ::= "assert"
calc  ::= "calc"
case  ::= "case"
then  ::= "then"
else  ::= "else"
as  ::= "as"
is  ::= "is"
by  ::= "by"
in  ::= "in"
decreases  ::= "decreases"
invariant  ::= "invariant"
function  ::= "function"
predicate  ::= "predicate"
least  ::= "least"
greatest  ::= "greatest"
inductive  ::= "inductive"
twostate  ::= "twostate"
copredicate  ::= "copredicate"
lemma  ::= "lemma"
static  ::= "static"
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  ::= '>'
singleeq  ::= "="
eq  ::= "=="
neq  ::= "!="
neqAlt  ::= '\u2260'
star  ::= '*'
at  ::= '@'
notIn  ::= "!in" CONTEXT  ( nonidchar  )
ellipsis  ::= "..."
reveal  ::= "reveal"
expect  ::= "expect"
sarrow  ::= "->"
qarrow  ::= "~>"
larrow  ::= "-->"
parno commented 3 years ago

Cool, nice looking visualization!

mingodad commented 3 years ago

After an issue was pointed out here https://github.com/Framstag/libosmscout/issues/1096#issuecomment-856664383 I implemented the generation of the EBNF understood by https://www.bottlecaps.de/rr/ui directly on CcocoR (https://github.com/mingodad/CocoR-CPP and https://github.com/mingodad/CocoR-CSharp ) and bellow is the new generated EBNF when using the -genRREBNF command line parameter.

My forks also add several small improvements to help devlop/debug grammars with CocoR and I welcome any feedback !

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

//
// productions
//

Dafny ::= ( "include" stringToken )* ( TopDecl )* EOF 
TopDecl ::= ( DeclModifier )* ( SubModuleDecl | ClassDecl | DatatypeDecl | NewtypeDecl | SynonymTypeDecl | IteratorDecl | TraitDecl | ClassMemberDecl ) 
DeclModifier ::= ( "abstract" | ghost | static | "protected" ) 
SubModuleDecl ::= ( ModuleDefinition | ModuleImport | ModuleExport ) 
ClassDecl ::= class ( Attribute )* ClassName ( GenericParameters )? ( ( "extends" Type ( comma Type )* | ellipsis ) )? lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
DatatypeDecl ::= ( datatype | codatatype ) ( Attribute )* DatatypeName ( GenericParameters )? singleeq ( ellipsis )? ( verticalbar )? DatatypeMemberDecl ( verticalbar DatatypeMemberDecl )* ( TypeMembers )? 
NewtypeDecl ::= newtype ( Attribute )* NewtypeName singleeq ( ellipsis )? ( LocalVarName ( colon Type )? verticalbar Expression ( ( ghost witness Expression | witness ( star | Expression ) ) )? ( TypeMembers )? | Type ( TypeMembers )? ) 
SynonymTypeDecl ::= type ( Attribute )* SynonymTypeName ( TypeParameterCharacteristics )* ( GenericParameters )? ( ( singleeq ( LocalVarName ( colon Type )? verticalbar Expression ( ( ghost witness Expression | witness ( star | Expression ) ) )? | Type ) | ellipsis ( TypeMembers )? | TypeMembers ) )? 
IteratorDecl ::= iterator ( Attribute )* IteratorName ( ( GenericParameters )? Formals ( ( "yields" | "returns" ) Formals )? | ellipsis ) IteratorSpec ( BlockStmt )? 
TraitDecl ::= trait ( Attribute )* ClassName ( GenericParameters )? ( ( "extends" Type ( comma Type )* | ellipsis ) )? lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
ClassMemberDecl ::= ( FieldDecl | ConstantFieldDecl | FunctionDecl | MethodDecl ) 
ModuleDefinition ::= "module" ( Attribute )* ModuleQualifiedName ( ( "refines" ModuleQualifiedName | Ident ) )? lbrace ( TopDecl )* rbrace 
ModuleImport ::= import ( "opened" )? ( ModuleName singleeq QualifiedModuleExport | ModuleName colon QualifiedModuleExport | QualifiedModuleExport ) 
ModuleExport ::= export ( ExportId )? ( ellipsis )? ( ( "provides" ( ExportSignature ( comma ExportSignature )* | star ) | "reveals" ( ExportSignature ( comma ExportSignature )* | star ) | "extends" ExportId ( comma ExportId )* ) )* 
Attribute ::= lbracecolon AttributeName ( Expressions )? rbrace 
ModuleQualifiedName ::= ModuleName ( dot ModuleName )* 
Ident ::= ( ident | least | greatest ) 
ModuleName ::= NoUSIdent 
QualifiedModuleExport ::= ModuleQualifiedName ( backtick ModuleExportSuffix )? 
ExportId ::= NoUSIdentOrDigits 
NoUSIdentOrDigits ::= ( NoUSIdent | digits ) 
ExportSignature ::= TypeNameOrCtorSuffix ( dot TypeNameOrCtorSuffix )? 
TypeNameOrCtorSuffix ::= IdentOrDigits 
NoUSIdent ::= Ident 
ModuleExportSuffix ::= ( ExportId | lbrace ExportId ( comma ExportId )* rbrace ) 
ClassName ::= NoUSIdent 
GenericParameters ::= openAngleBracket ( Variance )? TypeVariableName ( TypeParameterCharacteristics )* ( comma ( Variance )? TypeVariableName ( TypeParameterCharacteristics )* )* closeAngleBracket 
Type ::= TypeAndToken 
FieldDecl ::= var ( Attribute )* FIdentType ( comma FIdentType )* OldSemi 
ConstantFieldDecl ::= const ( Attribute )* CIdentType ( ellipsis )? ( gets Expression )? OldSemi 
FunctionDecl ::= ( twostate )? ( function ( method )? ( Attribute )* MethodFunctionName ( ( GenericParameters )? Formals colon ( openparen GIdentType closeparen | Type ) | ellipsis ) | predicate ( method )? ( Attribute )* MethodFunctionName ( ( GenericParameters )? ( Formals )? ( colon Type )? | ellipsis ) | ( least | inductive ) predicate ( Attribute )* MethodFunctionName ( ( GenericParameters )? ( KType )? Formals ( colon )? | ellipsis ) | ( greatest predicate | copredicate ) ( Attribute )* MethodFunctionName ( ( GenericParameters )? ( KType )? Formals ( colon )? | ellipsis ) ) FunctionSpec ( FunctionBody )? 
MethodDecl ::= ( method | lemma | ( greatest lemma | colemma ) | ( least | inductive ) lemma | twostate lemma | constructor ) ( Attribute )* ( MethodFunctionName )? ( ( GenericParameters )? ( KType )? Formals ( "returns" Formals )? | ellipsis ) MethodSpec ( ( DividedBlockStmt | BlockStmt ) )? 
DatatypeName ::= NoUSIdent 
DatatypeMemberDecl ::= ( Attribute )* DatatypeMemberName ( FormalsOptionalIds )? 
TypeMembers ::= lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
DatatypeMemberName ::= NoUSIdentOrDigits 
FormalsOptionalIds ::= openparen ( TypeIdentOptional ( comma TypeIdentOptional )* )? closeparen 
FIdentType ::= NoUSIdentOrDigits colon Type 
OldSemi ::= ( semicolon )? 
CIdentType ::= NoUSIdentOrDigits ( colon Type )? 
Expression ::= EquivExpression ( semicolon Expression )? 
NewtypeName ::= NoUSIdent 
LocalVarName ::= NoUSIdent 
SynonymTypeName ::= NoUSIdent 
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 | string | object | object_q | map OptGenericInstantiation | imap OptGenericInstantiation | arrayToken OptGenericInstantiation | TupleType | NamedType ) ( ( qarrow | larrow | sarrow ) Type )? 
IteratorName ::= NoUSIdent 
Formals ::= openparen ( GIdentType ( comma GIdentType )* )? closeparen 
IteratorSpec ::= ( ( ReadsClause | ModifiesClause | ( "yield" )? ( RequiresClause | EnsuresClause ) | DecreasesClause ) )* 
BlockStmt ::= lbrace ( Stmt )* rbrace 
TypeVariableName ::= NoUSIdent 
Variance ::= ( star | "+" | "!" | "-" ) 
TPCharOption ::= ( eq | digits | "!" "new" ) 
MethodFunctionName ::= NoUSIdentOrDigits 
KType ::= lbracket ( nat | ORDINAL ) rbracket 
MethodSpec ::= ( ( ModifiesClause | RequiresClause | EnsuresClause | DecreasesClause ) )* 
DividedBlockStmt ::= lbrace ( Stmt )* ( "new" semicolon ( Stmt )* )? rbrace 
RequiresClause ::= requires ( Attribute )* ( LabelName colon )? Expression OldSemi 
LabelName ::= NoUSIdentOrDigits 
EnsuresClause ::= ensures ( Attribute )* Expression OldSemi 
ModifiesClause ::= modifies ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi 
FrameExpression ::= ( Expression ( FrameField )? | FrameField ) 
DecreasesClause ::= decreases ( Attribute )* DecreasesList OldSemi 
DecreasesList ::= PossiblyWildExpression ( comma PossiblyWildExpression )* 
ReadsClause ::= reads ( Attribute )* PossiblyWildFrameExpression ( comma PossiblyWildFrameExpression )* OldSemi 
PossiblyWildFrameExpression ::= ( star | FrameExpression ) 
InvariantClause ::= invariant ( Attribute )* Expression OldSemi 
OptGenericInstantiation ::= ( GenericInstantiation )? 
TupleType ::= openparen ( Type ( comma Type )* )? closeparen 
NamedType ::= NameSegmentForTypeName ( dot TypeNameOrCtorSuffix OptGenericInstantiation )* 
NameSegmentForTypeName ::= Ident OptGenericInstantiation 
GenericInstantiation ::= openAngleBracket Type ( comma Type )* closeAngleBracket 
FunctionSpec ::= ( ( RequiresClause | ReadsClause | EnsuresClause | DecreasesClause ) )* 
FunctionBody ::= lbrace Expression rbrace 
PossiblyWildExpression ::= ( star | Expression ) 
FrameField ::= backtick IdentOrDigits 
IdentOrDigits ::= ( Ident | digits ) 
Stmt ::= OneStmt 
OneStmt ::= ( BlockStmt | UpdateStmt | VarDeclStatement | ReturnStmt | IfStmt | WhileStmt | AssertStmt | AssumeStmt | BreakStmt | CalcStmt | ExpectStmt | ForallStmt | LabeledStmt | MatchStmt | ModifyStmt | PrintStmt | RevealStmt | SkeletonStmt | YieldStmt ) 
UpdateStmt ::= ( Lhs ( ( Attribute )* semicolon | ( comma Lhs )* ( gets Rhs ( comma Rhs )* | boredSmiley ( assume )? Expression | ":-" ( ( expect | assert | assume ) )? Expression ( comma Rhs )* ) semicolon | colon ) | ":-" ( ( expect | assert | assume ) )? Expression ( comma Rhs )* semicolon ) 
VarDeclStatement ::= ( ghost )? var ( ( Attribute )* LocalIdentTypeOptional ( comma ( Attribute )* LocalIdentTypeOptional )* ( ( gets Rhs ( comma Rhs )* | ( Attribute )* boredSmiley ( assume )? Expression | ":-" ( ( expect | assert | assume ) )? Expression ( comma Rhs )* ) )? semicolon | CasePatternLocal ( gets | ( Attribute )* boredSmiley ) Expression semicolon ) 
ReturnStmt ::= "return" ( Rhs ( comma Rhs )* )? semicolon 
IfStmt ::= "if" ( AlternativeBlock | ( BindingGuard | Guard | ellipsis ) BlockStmt ( else ( IfStmt | BlockStmt ) )? ) 
WhileStmt ::= "while" ( LoopSpec AlternativeBlock | ( Guard | ellipsis ) LoopSpec ( BlockStmt | ellipsis | ) ) 
AssertStmt ::= assert ( Attribute )* ( ( LabelName colon )? Expression ( by BlockStmt | semicolon ) | ellipsis semicolon ) 
AssumeStmt ::= assume ( Attribute )* ( Expression | ellipsis ) semicolon 
BreakStmt ::= "break" ( LabelName | ( "break" )* ) semicolon 
CalcStmt ::= calc ( Attribute )* ( CalcOp )? lbrace ( Expression semicolon ( CalcOp )? ( ( BlockStmt | CalcStmt ) )* )* rbrace 
ExpectStmt ::= expect ( Attribute )* ( Expression | ellipsis ) ( comma Expression )? semicolon 
ForallStmt ::= "forall" ( openparen ( QuantifierDomain )? closeparen | ( QuantifierDomain )? ) ( EnsuresClause )* ( BlockStmt )? 
LabeledStmt ::= "label" LabelName colon OneStmt 
MatchStmt ::= "match" Expression ( lbrace ( CaseStmt )* rbrace | ( CaseStmt )* ) 
ModifyStmt ::= "modify" ( Attribute )* ( FrameExpression ( comma FrameExpression )* | ellipsis ) ( BlockStmt | semicolon ) 
PrintStmt ::= "print" Expression ( comma Expression )* semicolon 
RevealStmt ::= reveal Expression ( comma Expression )* semicolon 
SkeletonStmt ::= ellipsis semicolon 
YieldStmt ::= "yield" ( Rhs ( comma Rhs )* )? semicolon 
Rhs ::= ( "new" ( NewArray | TypeAndToken ( ( NewArray | openparen ( ActualBindings )? closeparen ) )? ) | star | Expression ) ( Attribute )* 
Lhs ::= ( NameSegment ( Suffix )* | ConstAtomExpression Suffix ( Suffix )* ) 
NewArray ::= lbracket ( rbracket lbracket ( Expressions )? rbracket | Expressions rbracket ( ( openparen Expression closeparen | lbracket ( Expressions )? rbracket ) )? ) 
ActualBindings ::= ActualBinding ( comma ActualBinding )* 
Expressions ::= Expression ( comma Expression )* 
CasePatternLocal ::= ( Ident openparen ( CasePatternLocal ( comma CasePatternLocal )* )? closeparen | openparen ( CasePatternLocal ( comma CasePatternLocal )* )? closeparen | LocalIdentTypeOptional ) 
AlternativeBlock ::= ( lbrace ( AlternativeBlockCase )* rbrace | AlternativeBlockCase ( AlternativeBlockCase )* ) 
BindingGuard ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* boredSmiley Expression 
Guard ::= ( star | openparen star closeparen | Expression ) 
AlternativeBlockCase ::= case ( BindingGuard | Expression ) darrow ( Stmt )* 
LoopSpec ::= ( ( InvariantClause | DecreasesClause | ModifiesClause ) )* 
ExtendedPattern ::= ( openparen ( ExtendedPattern ( comma ExtendedPattern )* )? closeparen | Ident openparen ( ExtendedPattern ( comma ExtendedPattern )* )? closeparen | PossiblyNegatedLiteralExpr | IdentTypeOptional ) 
PossiblyNegatedLiteralExpr ::= ( "-" ( Nat | Dec ) | LiteralExpression ) 
CaseStmt ::= case ExtendedPattern darrow ( Stmt )* 
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 )* ( ImpliesOp )? ) )? 
LogicalExpression ::= ( AndOp RelationalExpression ( AndOp RelationalExpression )* ( OrOp )? | OrOp RelationalExpression ( OrOp RelationalExpression )* ( AndOp )? | RelationalExpression ( ( AndOp RelationalExpression ( AndOp RelationalExpression )* ( OrOp )? | OrOp RelationalExpression ( OrOp RelationalExpression )* ( AndOp )? ) )? ) 
ImpliesExpression ::= LogicalExpression ( ImpliesOp ImpliesExpression )? ( ExpliesOp )? 
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 | "^" ) )? | verticalbar AsExpression ( verticalbar AsExpression )* ( ( "^" | "&" ) )? | "^" AsExpression ( "^" AsExpression )* ( ( "&" | verticalbar ) )? ) )? 
MulOp ::= ( star | "/" | "%" ) 
AsExpression ::= UnaryExpression ( ( as TypeAndToken | is TypeAndToken ) )* 
UnaryExpression ::= ( "-" UnaryExpression | NegOp UnaryExpression | PrimaryExpression ) 
PrimaryExpression ::= ( MapDisplayExpr ( Suffix )* | SetDisplayExpr ( Suffix )* | LambdaExpression | EndlessExpression | NameSegment ( Suffix )* | SeqDisplayExpr ( Suffix )* | ConstAtomExpression ( Suffix )* ) 
MapDisplayExpr ::= ( map | imap ) lbracket ( MapLiteralExpressions )? rbracket 
Suffix ::= ( dot ( openparen MemberBindingUpdate ( comma MemberBindingUpdate )* closeparen | DotSuffix ( GenericInstantiation ( AtCall )? | HashCall | ( AtCall )? ) ) | lbracket ( Expression ( ".." ( Expression )? | gets Expression | colon ( Expression ( colon Expression )* ( colon )? )? | ( comma Expression )* ) | ".." ( Expression )? ) rbracket | openparen ( ActualBindings )? closeparen ) 
SetDisplayExpr ::= ( ( iset | multiset ) )? ( lbrace ( Expressions )? rbrace | openparen Expression closeparen ) 
LambdaExpression ::= ( WildIdent | openparen ( IdentTypeOptional ( comma IdentTypeOptional )* )? closeparen ) LambdaSpec darrow Expression 
EndlessExpression ::= ( IfExpression | MatchExpression | QuantifierExpression | SetComprehensionExpr | StmtInExpr Expression | LetExpression | MapComprehensionExpr ) 
NameSegment ::= Ident ( GenericInstantiation ( AtCall )? | HashCall | ( AtCall )? ) 
SeqDisplayExpr ::= ( seq ( GenericInstantiation )? openparen Expression comma Expression closeparen | lbracket ( Expressions )? rbracket ) 
ConstAtomExpression ::= ( LiteralExpression | "this" | "fresh" openparen Expression closeparen | "allocated" openparen Expression closeparen | "unchanged" ( at LabelName )? openparen FrameExpression ( comma FrameExpression )* closeparen | "old" ( at LabelName )? openparen Expression closeparen | verticalbar Expression verticalbar | ParensExpression ) 
LiteralExpression ::= ( "false" | "true" | "null" | Nat | Dec | charToken | stringToken ) 
ParensExpression ::= openparen ( ActualBindings )? closeparen 
Nat ::= ( digits | hexdigits ) 
Dec ::= decimaldigits 
LambdaSpec ::= ( ( ReadsClause | requires ( Attribute )* Expression ) )* 
MapLiteralExpressions ::= Expression gets Expression ( comma Expression gets Expression )* 
MapComprehensionExpr ::= ( map | imap ) IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* ( verticalbar Expression )? QSep Expression ( gets Expression )? 
IfExpression ::= "if" ( BindingGuard | Expression ) then Expression else Expression 
MatchExpression ::= "match" Expression ( lbrace ( CaseExpression )* rbrace | ( CaseExpression )* ) 
QuantifierExpression ::= ( Forall | Exists ) QuantifierDomain QSep Expression 
SetComprehensionExpr ::= ( set | iset ) IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* verticalbar Expression ( QSep Expression )? 
StmtInExpr ::= ( AssertStmt | ExpectStmt | AssumeStmt | RevealStmt | CalcStmt ) 
LetExpression ::= ( LetExprWithLHS | LetExprWithoutLHS ) 
LetExprWithLHS ::= ( ghost )? var CasePattern ( comma CasePattern )* ( gets | ( Attribute )* boredSmiley | ":-" ) Expression ( comma Expression )* semicolon Expression 
LetExprWithoutLHS ::= ":-" Expression semicolon Expression 
CasePattern ::= ( Ident openparen ( CasePattern ( comma CasePattern )* )? closeparen | openparen ( CasePattern ( comma CasePattern )* )? closeparen | IdentTypeOptional ) 
CaseExpression ::= case ExtendedPattern darrow Expression 
AtCall ::= at LabelName openparen ( ActualBindings )? closeparen 
HashCall ::= "#" ( GenericInstantiation )? lbracket Expression rbracket openparen ( ActualBindings )? closeparen 
MemberBindingUpdate ::= NoUSIdentOrDigits gets Expression 
DotSuffix ::= ( Ident | digits | decimaldigits | requires | reads ) 
ActualBinding ::= ( NoUSIdentOrDigits gets )? Expression 
AttributeName ::= NoUSIdent 

//
// 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 ::= "`"
semicolon ::= ";"
darrow ::= "=>"
assume ::= "assume"
assert ::= "assert"
calc ::= "calc"
case ::= "case"
then ::= "then"
else ::= "else"
as ::= "as"
is ::= "is"
by ::= "by"
in ::= "in"
decreases ::= "decreases"
invariant ::= "invariant"
function ::= "function"
predicate ::= "predicate"
least ::= "least"
greatest ::= "greatest"
inductive ::= "inductive"
twostate ::= "twostate"
copredicate ::= "copredicate"
lemma ::= "lemma"
static ::= "static"
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 ::= ">"
singleeq ::= "="
eq ::= "=="
neq ::= "!="
neqAlt ::= "\u2260"
star ::= "*"
at ::= "@"
ellipsis ::= "..."
reveal ::= "reveal"
expect ::= "expect"
sarrow ::= "->"
qarrow ::= "~>"
larrow ::= "-->"
RustanLeino commented 3 years ago

I love these diagrams! Even though I know both the grammar and Dafny.atg file well, I'm finding it both interesting and useful to look at these.

Do you have (or can you create) some script we can use to

mingodad commented 3 years ago

Yes there is, 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 Dafny.atg
java -jar rr.war -out:Dafny.atg.xhtml Parser.ebnf

Also any feedback on the CocoR extensions are welcome !

keyboardDrummer commented 3 years ago

Dafny-lsp.atg

Could you link to the file you're referring to?

mingodad commented 3 years ago

Good question, looking at where I found it https://github.com/just-me-/dafny-language-server/blob/master/Source/Dafny/Dafny.atg I can see that it's an old clone of Dafny itself. So it's my fault when reporting it. Probably I should delete it ?

keyboardDrummer commented 3 years ago

Probably I should delete it?

Delete what? This ticket also contains a sort of feature request. If you find a bug related to the grammar in the future, in might be easier to cut a separate ticket for it.

mingodad commented 3 years ago

The message reporting it here https://github.com/dafny-lang/dafny/issues/1244#issuecomment-886039577

mingodad commented 2 years ago

I also just got a working port of CocoR to Typescrip/Javascript here https://github.com/mingodad/CocoR-Typescript and also an online playground here https://mingodad.github.io/CocoR-Typescript/playground .