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.

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

Grammar railroad diagram #13

Open
mingodad opened this issue Jun 28, 2021 · 3 comments
Open

Grammar railroad diagram #13

mingodad opened this issue Jun 28, 2021 · 3 comments

Comments

@mingodad
Copy link

mingodad commented Jun 28, 2021

I've done a experimental tool to convert bison grammars to a kind of EBNF understood by https://www.bottlecaps.de/rr/ui to generate railroad diagrams see bellow the converted src/libs/parse/parser.ml and with some hand made changes 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.

/*
From https://github.com/arsalanc-v2/dafny-of-python/blob/master/src/libs/parse/parser.ml
*/

program ::=  stmts_plus EOF
stmts_plus ::=  /* empty */ | stmt | stmt NEWLINE stmts_plus | stmt SEMICOLON stmts_plus
newline_star ::=   /* empty */ | NEWLINE newline_star
stmt ::=  newline_star compound_stmt | newline_star small_stmt
small_stmt ::=  assignment | star_exps | RETURN star_exps | PASS | ASSERT exp | BREAK
compound_stmt ::=  list DEF IDENTIFIER LPAREN param_star RPAREN ARROW typ_id COLON block | IF exp COLON block elif_star ELSE COLON block | IF exp COLON block elif_star | list FOR star_targets IN star_exps COLON block | list WHILE exp COLON block
assignment ::=  exp COLON exp EQ star_exps | exp EQ star_exps | exp PLUSEQ star_exps | exp MINUSEQ star_exps | exp TIMESEQ star_exps | exp DIVIDEEQ star_exps
elif_star ::=   /* empty */ | ELIF exp COLON block elif_star
star_exps ::=  exp star_exps_rest COMMA | exp star_exps_rest | exp COMMA | exp
star_exps_rest ::=  star_exps_rest COMMA exp | COMMA exp
star_targets ::=  star_target star_targets_rest COMMA | star_target star_targets_rest | star_target
star_targets_rest ::=  star_targets_rest COMMA star_target | COMMA star_target
star_target ::=  IDENTIFIER | LPAREN star_targets RPAREN | LBRACK star_targets RBRACK
exp ::=  implication IF implication ELSE exp | LAMBDA id_star COLON exp | implication | typ
implication ::=  implication BIIMPL disjunction | implication IMPLIES disjunction | implication EXPLIES disjunction | disjunction
disjunction ::=  disjunction OR conjunction | conjunction
conjunction ::=  conjunction AND inversion | inversion
inversion ::=  NOT inversion | comparison
comparison ::=  comparison EQEQ sum | comparison NEQ sum | comparison LTE sum | comparison LT sum | comparison GTE sum | comparison GT sum | comparison NOT_IN sum | comparison IN sum | sum
sum ::=  sum PLUS term | sum MINUS term | term
term ::=  term TIMES factor | term DIVIDE factor | term MOD factor | factor
factor ::=  PLUS factor | MINUS factor | power
power ::=  primary
primary ::=  primary DOT IDENTIFIER | primary LPAREN arguments RPAREN | primary slice | atom
arguments ::=  exp_star
atom ::=  IDENTIFIER | TRUE | FALSE | INT | FLOAT | strings | NONE | FORALL id_star DOUBLECOLON exp | EXISTS id_star DOUBLECOLON exp | LPAREN exp COMMA exp_star RPAREN | LPAREN exp RPAREN | lst_exp | set_exp | dict_exp | LEN LPAREN star_exps RPAREN | MAX LPAREN star_exps RPAREN | OLD LPAREN star_exps RPAREN | FRESH LPAREN star_exps RPAREN
strings ::=  STRING | strings STRING
slice ::=  LBRACK exp COLON exp RBRACK | LBRACK exp COLON RBRACK | LBRACK COLON exp RBRACK | LBRACK COLON RBRACK | LBRACK exp RBRACK
lst_exp ::=  LBRACK exp_star RBRACK
dict_exp ::=  LBRACE kv_star RBRACE
kv_star ::=   /* empty */ | kv_rest
kv_rest ::=  kv COMMA kv_rest | kv COMMA | kv
kv ::=  exp COLON exp
set_exp ::=  LBRACE exp_star RBRACE
spec ::=  PRE spec_rem | POST spec_rem | DECREASES spec_rem | INVARIANT spec_rem | READS spec_rem | MODIFIES spec_rem
spec_rem ::=  exp NEWLINE
block ::=  NEWLINE newline_star indent_plus stmts_plus dedent_plus
indent_plus ::=  INDENT
dedent_plus ::=  DEDENT
typ_id ::=  typ | IDENTIFIER
typ ::=  data_typ | base_typ
typ_plus ::=  typ_plus COMMA typ_id | typ_id
base_typ ::=  STRING_TYP | INT_TYP | FLOAT_TYP | BOOL_TYP | NONE | OBJ_TYP
data_typ ::=  LIST_TYP LBRACK typ_id RBRACK | LIST_TYP | DICT_TYP LBRACK typ_id COMMA typ_id RBRACK | DICT_TYP | SET_TYP LBRACK typ_id RBRACK | SET_TYP | TUPLE_TYP LBRACK typ_plus RBRACK | TUPLE_TYP | CALLABLE_TYP LBRACK LBRACK typ_plus RBRACK COMMA typ_id RBRACK | TYPE_TYP LBRACK typ_id RBRACK | TYPE_TYP
param_star ::=   /* empty */ | param_rest
param_rest ::=  param COMMA param_rest | param COMMA | param
param ::=  IDENTIFIER COLON exp
id_star ::=  /* empty */ | id_rest
id_rest ::=  IDENTIFIER COMMA id_rest | IDENTIFIER
exp_star ::=   /* empty */ | exp_rest
exp_rest ::=  exp COMMA exp_rest | exp COMMA | exp

// Tokens

//comment lexbuf  ::= "import"
//comment lexbuf  ::= "from"
FORALL  ::= "forall"
EXISTS  ::= "exists"
BIIMPL  ::= "<==>"
IMPLIES  ::= "==>"
EXPLIES  ::= "<=="
DOUBLECOLON  ::= "::"
LPAREN  ::= '('
RPAREN  ::= ')'
LBRACE  ::= '{'
RBRACE  ::= '}'
LBRACK  ::= '['
RBRACK  ::= ']'
DOT  ::= '.'
COLON  ::= ':'
SEMICOLON  ::= ';'
COMMA  ::= ','
OLD  ::= "old"
LEN  ::= "len"
IDENTIFIER  ::= "max"
IDENTIFIER  ::= "filter"
IDENTIFIER  ::= "map"
ARROW  ::= "->"
ARROW  ::= "->"
DEF  ::= "def"
LAMBDA  ::= "lambda"
IF  ::= "if"
ELIF  ::= "elif"
ELSE  ::= "else"
FOR  ::= "for"
WHILE  ::= "while"
BREAK  ::= "break"
PASS  ::= "pass"
RETURN  ::= "return"
ASSERT  ::= "assert"
NOT_IN  ::= "not in"
IN  ::= "in"
EQEQ  ::= "=="
EQ  ::= '='
NEQ  ::= "!="
PLUS  ::= '+'
PLUSEQ  ::= "+="
MINUS  ::= '-'
MINUSEQ  ::= "-="
TIMES  ::= '*'
TIMESEQ  ::= "*="
DIVIDE  ::= "/"
DIVIDEEQ  ::= "/="
MOD  ::= "%"
LTE  ::= "<="
LT  ::= '<'
GTE  ::= ">="
GT  ::= '>'
AND  ::= "and"
OR  ::= "or"
NOT  ::= "not"
TRUE  ::= "True"
FALSE  ::= "False"
NONE  ::= "None"
@mingodad
Copy link
Author

I have edited the EBNF from the first message to fix several issues with the tool I used to generate it.

@arsalan0c
Copy link
Owner

This is awesome, thank you for sharing! Would you be able to suggest how I may automatically generate the diagrams from the source?

I've also tried to use the batch diagram generation function of the generator together with the above EBNF but the html output does not show the diagram properly. I suppose it's because it lacks the manual changes you made.

@mingodad
Copy link
Author

mingodad commented Jul 1, 2021

Someone asked for other similar job here dafny-lang/dafny#1244 (comment) and I gave one possible way.

How did you invoked the batch diagram generation function ?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants