Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Grammar railroad diagram #1244

Open
mingodad opened this issue Jun 6, 2021 · 9 comments
Open

Grammar railroad diagram #1244

mingodad opened this issue Jun 6, 2021 · 9 comments
Assignees
@davidcok
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials part: parser First phase of Dafny's pipeline priority: not yet Will reconsider working on this when we're looking for work

Comments

@mingodad
Copy link

mingodad commented Jun 6, 2021

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
Copy link
Collaborator

parno commented Jun 7, 2021

Cool, nice looking visualization!

@mingodad
Copy link
Author

mingodad commented Jun 8, 2021

After an issue was pointed out here Framstag/libosmscout#1096 (comment) 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
Copy link
Collaborator

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

  • automatically generate the grammars above from Dafny.atg, and
  • run your tool to generate up-to-date railroad diagrams that we can link from the Dafny documentation page?

@mingodad
Copy link
Author

mingodad commented Jun 12, 2021 •
edited
Loading

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 !

@mingodad mingodad mentioned this issue Jul 1, 2021
Open
@keyboardDrummer keyboardDrummer added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Jul 7, 2021
@keyboardDrummer keyboardDrummer added the part: parser First phase of Dafny's pipeline label Jul 19, 2021
@keyboardDrummer
Copy link
Member

Dafny-lsp.atg

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

@mingodad
Copy link
Author

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
Copy link
Member

keyboardDrummer commented Jul 26, 2021 •
edited
Loading

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
Copy link
Author

The message reporting it here #1244 (comment)

@mingodad
Copy link
Author

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 .

@robin-aws robin-aws mentioned this issue Aug 3, 2022
Closed
@davidcok davidcok added the part: documentation Dafny's reference manual, tutorial, and other materials label Dec 4, 2022
@davidcok davidcok self-assigned this Dec 4, 2022
@sorawee sorawee mentioned this issue May 3, 2024
Closed
@MikaelMayer MikaelMayer added the priority: not yet Will reconsider working on this when we're looking for work label Aug 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@davidcok davidcok

Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials part: parser First phase of Dafny's pipeline priority: not yet Will reconsider working on this when we're looking for work
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
6 participants
@mingodad @parno @keyboardDrummer @MikaelMayer @davidcok @RustanLeino