Grammar railroad diagram

[mingodad]

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/parser_tptp.mly 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://raw.githubusercontent.com/bytekid/koala/master/src/parser_tptp.mly
*/

main ::=  /* empty */ | main unit | EOF
unit ::=  annotated_formula | include_file | comment | annotation
include_file ::=  Include LeftParen file_name formula_selection RightParen Dot
file_name ::=  single_quoted
formula_selection ::=  /* empty */ | Comma name_list
name_list ::=  name | name_list Comma name
comment ::=  CommentPercent | CommentStar | CommentEprover
annotation ::=  AnnotationPercent | AnnotationStar
annotated_formula ::=  CNF_T LeftParen name Comma formula_role Comma cnf_formula formula_annotations RightParen Dot | FOF_T | THF_T | TFF_T LeftParen name Comma Type Comma tff_typed_atom RightParen Dot | TFF_T LeftParen name Comma formula_role Comma tff_cnf_formula formula_annotations RightParen Dot | TCF_T LeftParen name Comma formula_role Comma tff_cnf_formula formula_annotations RightParen Dot
tff_cnf_formula ::=  cnf_formula | tff_quantified_formula | LeftParen tff_quantified_formula RightParen
tff_quantified_formula ::=  tff_fol_quantifier LBrace tff_variable_list RBrace Column tff_unitary_formula
tff_fol_quantifier ::=  ForAll | Exists
tff_variable_list ::=  tff_variable | tff_variable Comma tff_variable_list
tff_variable ::=  tff_typed_variable | tff_default_type_variable
tff_typed_variable ::=  variable_name Column tff_atomic_type
tff_default_type_variable ::=  variable_name
variable_name ::=  UpperWord
tff_unitary_formula ::=  cnf_formula
tff_typed_atom ::=  tff_untyped_atom Column tff_top_level_type | tff_untyped_atom Column tff_top_level_type Or attr_list | LeftParen tff_typed_atom RightParen
attr_list ::=  attr | attr_list Or attr
attr ::=  defined_functor LeftParen attr_name Comma attr_args RightParen
attr_name ::=  functor_name | defined_functor | system_functor
attr_args ::=  unsigned_integer | attr_list_arg | attr_str_arg
attr_list_arg ::=  LBrace attr_ilist_arg_list RBrace | LBrace attr_slist_arg_list RBrace
attr_ilist_arg_list ::=  unsigned_integer | unsigned_integer Comma attr_ilist_arg_list
attr_slist_arg_list ::=  attr_str_arg | attr_str_arg Comma attr_slist_arg_list
tff_untyped_atom ::=  functor_name | defined_functor | system_functor
attr_str_arg ::=  functor_name | defined_functor
tff_top_level_type ::=  tff_atomic_type | tff_mapping_type | LeftParen tff_mapping_type RightParen
tff_atomic_type ::=  atomic_word | defined_type
defined_type ::=  DollarWord | DollarDollarWord
tff_unitary_type ::=  tff_atomic_type | tff_xprod_type
tff_mapping_type ::=  tff_unitary_type Arrow tff_atomic_type | LeftParen tff_unitary_type RightParen Arrow tff_atomic_type
tff_xprod_type ::=  tff_atomic_type Star tff_atomic_type | tff_xprod_type Star tff_atomic_type
formula_annotations ::=  /* empty */ | Comma | Comma source optional_info
optional_info ::=  /* empty */ | Comma source
source ::=  plain_term | plain_term_list
plain_term_list ::=  LBrace RBrace | LBrace arguments RBrace
cnf_formula ::=  LeftParen disjunction RightParen | LeftParen LeftParen cnf_formula RightParen RightParen | disjunction
disjunction ::=  literal | disjunction Or literal
literal ::=  atomic_formula | fol_infix_unary | Negation atomic_formula | Negation LeftParen atomic_formula RightParen | LeftParen atomic_formula RightParen | LeftParen fol_infix_unary RightParen
fol_infix_unary ::=  term NegEquality term
atomic_formula ::=  plain_atomic_formula | defined_atomic_formula | system_atomic_formula
plain_atomic_formula ::=  functor_name | functor_name LeftParen arguments RightParen
plain_term ::=  functor_name | functor_name LeftParen arguments RightParen
functor_name ::=  atomic_word
arguments ::=  arguments_rev
arguments_rev ::=  term | arguments_rev Comma term
term ::=  function_term | variable
variable ::=  UpperWord
function_term ::=  plain_term | defined_term | system_term
defined_term ::=  defined_atom | defined_atomic_term
defined_atom ::=  number
defined_atomic_term ::=  defined_plain_term
defined_plain_term ::=  defined_functor | defined_functor LeftParen arguments RightParen
system_term ::=  system_functor | system_functor LeftParen arguments RightParen
defined_functor ::=  Equality | DollarWord
system_functor ::=  DollarDollarWord
defined_atomic_formula ::=  defined_plain_formula | defined_infix_formula
system_atomic_formula ::=  system_plain_formula
defined_plain_formula ::=  defined_functor | defined_functor LeftParen arguments RightParen
system_plain_formula ::=  system_functor | system_functor LeftParen arguments RightParen
defined_infix_formula ::=  term defined_infix_pred term
defined_infix_pred ::=  infix_equality
infix_equality ::=  Equality
formula_role ::=  LowerWord
number ::=  integer | rational | real
rational ::=  signed_rational | unsigned_rational
signed_rational ::=  Plus unsigned_rational | Minus unsigned_rational
unsigned_rational ::=  Decimal Slash Decimal
real ::=  signed_real | unsigned_real
signed_real ::=  Plus unsigned_real | Minus unsigned_real
unsigned_real ::=  decimal_fraction | decimal_exponent
decimal_fraction ::=  Decimal_fraction
decimal_exponent ::=  Decimal_exponent
integer ::=  signed_integer | unsigned_integer
signed_integer ::=  Plus unsigned_integer | Minus unsigned_integer
unsigned_integer ::=  Decimal
name ::=  atomic_word | integer_string
atomic_word ::=  LowerWord | single_quoted | key_word
key_word ::=  CNF_T | FOF_T | TFF_T | TCF_T | THF_T | Include | Type
single_quoted ::=  QuotedStr
integer_string ::=  Decimal | Plus Decimal | Minus Decimal

// Tokens

Comma ::= ','
Dot ::= '.'
Column ::= ':'
LeftParen ::= '('
RightParen ::= ')'
LBrace ::= '['
RBrace ::= ']'

/* logic */
ForAll ::= '!'
Exists ::= '?'
And ::= '&'
NegAnd ::= "~&"
Or ::= '|'
NegOr ::= "~|"
Equality ::= '='
NegEquality ::= "!="
Negation ::= '~'
ImplicationLR ::= "=>"
ImplicationRL ::= "<="
Equivalence ::= "<=>"
NegEquivalence ::= "<~>"
Plus ::= '+'
Minus ::= '-'
Star ::= '*'
Arrow ::= '>'
Less_Sign ::= '<'
Slash ::= '/'
/*keywords*/

CNF_T ::= "cnf"
FOF_T ::= "fof"
TFF_T ::= "tff"
TCF_T ::= "tcf"
THF_T ::= "thf"
Include ::= "include"
Type ::= "type"