search

potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
599 stars 79 forks source link

Grammar railroad diagram #429

Closed mingodad closed 1 year ago

mingodad commented 1 year ago

Using some online tools like https://www.bottlecaps.de/rr/ui and https://www.bottlecaps.de/convert/ and manually adding the tokens from the lexer we can have a nice navigable railroad diagram.

Copy and paste the EBNF shown bellow on https://www.bottlecaps.de/rr/ui on the tab Edit Grammar the click on the tab View Diagram to see/download a navigable railroad diagram. 

/* converted on Mon May 29, 2023, 20:12 (UTC+02) by bison-to-w3c v0.64 which is Copyright (c) 2011-2023 by Gunther Rademacher <grd@gmx.net> */
//From: https://github.com/potassco/clingo/blob/master/libgringo/src/input/nongroundgrammar.yy

start    ::= PARSE_LP statement*
           | PARSE_DEF define SYNC
statement
         ::= SYNC
           | ( SCRIPT LPAREN IDENTIFIER RPAREN CODE | THEORY identifier enable_theory_definition_lexing LBRACE theory_definition_list RBRACE disable_theory_lexing | ( MINIMIZE | MAXIMIZE ) LBRACE ( optimizeweight optimizetuple optimizecond ( SEM optimizeweight optimizetuple optimizecond )* )? RBRACE | ( SHOWSIG | DEFINED ) SUB? identifier SLASH NUMBER | INCLUDE ( STRING | LT identifier GT ) | BLOCK identifier ( LPAREN idlist RPAREN )? )? DOT
           | error disable_theory_lexing ( DOT | SYNC )
           | head ( DOT | IF ( DOT | bodydot ) )
           | IF ( bodydot | DOT )
           | ( WIF ( bodydot | DOT ) LBRACK optimizeweight optimizetuple | HEURISTIC atom bodyconddot LBRACK term ( AT term )? COMMA term ) RBRACK
           | SHOW ( DOT | term ( COLON bodydot | DOT ) )
           | EDGE LPAREN term COMMA term ( SEM term COMMA term )* RPAREN bodyconddot
           | PROJECT ( SUB? identifier SLASH NUMBER DOT | atom bodyconddot )
           | CONST identifier EQ constterm DOT ( LBRACK ( DEFAULT | OVERRIDE ) RBRACK )?
           | EXTERNAL atom ( COLON ( bodydot | DOT ) | DOT ) ( LBRACK term RBRACK )?
identifier
         ::= IDENTIFIER
           | DEFAULT
           | OVERRIDE
constterm
         ::= ( constterm ( XOR | QUESTION | AND | ADD | SUB | MUL | SLASH | MOD | POW ) | SUB | BNOT ) constterm
           | LPAREN consttermvec? COMMA? RPAREN
           | AT? identifier ( LPAREN constargvec RPAREN )?
           | VBAR constterm VBAR
           | NUMBER
           | STRING
           | INFIMUM
           | SUPREMUM
consttermvec
         ::= constterm ( COMMA constterm )*
constargvec
         ::= consttermvec?
term     ::= ( term ( DOTS | XOR | QUESTION | AND | ADD | SUB | MUL | SLASH | MOD | POW ) | SUB | BNOT ) term
           | LPAREN tuplevec RPAREN
           | AT? identifier ( LPAREN argvec RPAREN )?
           | VBAR term ( SEM term )* VBAR
           | NUMBER
           | STRING
           | INFIMUM
           | SUPREMUM
           | VARIABLE
           | ANONYMOUS
ntermvec ::= term ( COMMA term )*
termvec  ::= ntermvec?
tuple    ::= ntermvec? COMMA?
tuplevec ::= tuple ( SEM tuple )*
argvec   ::= termvec ( SEM termvec )*
cmp      ::= GT
           | LT
           | GEQ
           | LEQ
           | EQ
           | NEQ
atom     ::= SUB? identifier ( LPAREN argvec RPAREN )?
rellitvec
         ::= ( cmp term )+
literal  ::= ( NOT NOT? )? ( TRUE | FALSE | atom | term rellitvec )
nlitvec  ::= literal ( COMMA literal )*
litvec   ::= nlitvec?
optcondition
         ::= ( COLON litvec )?
aggregatefunction
         ::= SUM
           | SUMP
           | MIN
           | MAX
           | COUNT
bodyaggrelem
         ::= COLON litvec
           | ntermvec optcondition
altbodyaggrelem
         ::= literal optcondition
bodyaggregate
         ::= ( LBRACE ( altbodyaggrelem ( SEM altbodyaggrelem )* )? | aggregatefunction LBRACE ( bodyaggrelem ( SEM bodyaggrelem )* )? ) RBRACE
upper    ::= ( cmp? term )?
lubodyaggregate
         ::= ( term cmp? )? bodyaggregate upper
           | theory_atom
headaggregate
         ::= ( aggregatefunction LBRACE ( termvec COLON literal optcondition ( SEM termvec COLON literal optcondition )* )? | LBRACE ( literal optcondition ( SEM literal optcondition )* )? ) RBRACE
luheadaggregate
         ::= ( term cmp? )? headaggregate upper
           | theory_atom
conjunction
         ::= literal COLON litvec
dsym     ::= SEM
           | VBAR
disjunction
         ::= literal ( ( COMMA | dsym | COLON ( nlitvec dsym | SEM ) ) literal ( ( COMMA | dsym | COLON ( SEM | nlitvec dsym ) ) literal )* optcondition | COLON litvec )
bodycomma
         ::= ( ( literal | ( NOT NOT? )? lubodyaggregate ) ( COMMA | SEM ) | conjunction SEM )*
bodydot  ::= bodycomma ( literal | ( NOT NOT? )? lubodyaggregate | conjunction ) DOT
bodyconddot
         ::= DOT
           | COLON ( DOT | bodydot )
head     ::= literal
           | disjunction
           | luheadaggregate
optimizetuple
         ::= ( COMMA ntermvec )?
optimizeweight
         ::= term ( AT term )?
optimizecond
         ::= ( COLON ( literal ( COMMA literal )* )? )?
define   ::= identifier EQ constterm
idlist   ::= ( identifier ( COMMA identifier )* )?
theory_op
         ::= THEORY_OP
           | NOT
theory_op_list
         ::= theory_op+
theory_term
         ::= LBRACE theory_opterm_list RBRACE
           | LBRACK theory_opterm_list RBRACK
           | LPAREN ( theory_opterm ( COMMA theory_opterm_nlist? )? )? RPAREN
           | identifier ( LPAREN theory_opterm_list RPAREN )?
           | NUMBER
           | STRING
           | INFIMUM
           | SUPREMUM
           | VARIABLE
theory_opterm
         ::= theory_op_list? theory_term ( theory_op_list theory_term )*
theory_opterm_nlist
         ::= theory_opterm ( COMMA theory_opterm )*
theory_opterm_list
         ::= theory_opterm_nlist?
theory_atom_element
         ::= theory_opterm_nlist disable_theory_lexing optcondition
           | disable_theory_lexing COLON litvec
theory_atom_element_list
         ::= ( theory_atom_element ( enable_theory_lexing SEM theory_atom_element )* )?
theory_atom_name
         ::= identifier ( LPAREN argvec RPAREN )?
theory_atom
         ::= AND theory_atom_name ( enable_theory_lexing LBRACE theory_atom_element_list enable_theory_lexing RBRACE ( theory_op theory_opterm )? disable_theory_lexing )?
theory_operator_list
         ::= ( theory_op ( COMMA theory_op )* )?
theory_operator_definition
         ::= theory_op enable_theory_definition_lexing COLON NUMBER COMMA ( UNARY | BINARY COMMA ( LEFT | RIGHT ) )
theory_operator_definiton_list
         ::= ( theory_operator_definition ( enable_theory_lexing SEM theory_operator_definition )* )?
theory_definition_identifier
         ::= identifier
           | LEFT
           | RIGHT
           | UNARY
           | BINARY
           | HEAD
           | BODY
           | ANY
           | DIRECTIVE
theory_term_definition
         ::= theory_definition_identifier enable_theory_lexing LBRACE theory_operator_definiton_list enable_theory_definition_lexing RBRACE
theory_atom_type
         ::= HEAD
           | BODY
           | ANY
           | DIRECTIVE
theory_atom_definition
         ::= AND theory_definition_identifier SLASH NUMBER COLON theory_definition_identifier COMMA ( enable_theory_lexing LBRACE theory_operator_list enable_theory_definition_lexing RBRACE COMMA theory_definition_identifier COMMA )? theory_atom_type
theory_definition_nlist
         ::= ( theory_definition_list SEM )? ( theory_atom_definition | theory_term_definition )
theory_definition_list
         ::= theory_definition_nlist?
enable_theory_lexing
         ::=
enable_theory_definition_lexing
         ::=
disable_theory_lexing
         ::=

//Tokens

//\(\S+\)\s+\(\S+\)
ADD ::= "+"
AND ::= "&"
EQ ::= "="
AT ::= "@"
BASE ::= "#base"
BNOT ::= "~"
COLON ::= ":"
COMMA ::= ","
CONST ::= "#const"
COUNT ::= "#count"
CUMULATIVE ::= "#cumulative"
DOT ::= "."
DOTS ::= ".."
END ::=  "<EOF>"
EXTERNAL ::= "#external"
DEFINED ::= "#defined"
FALSE ::= "#false"
FORGET ::= "#forget"
GEQ ::= ">="
GT ::= ">"
IF ::= ":-"
INCLUDE ::= "#include"
INFIMUM ::= "#inf"
LBRACE ::= "{"
LBRACK ::= "["
LEQ ::= "<="
LPAREN ::= "("
LT ::= "<"
MAX ::= "#max"
MAXIMIZE ::= "#maximize"
MIN ::= "#min"
MINIMIZE ::= "#minimize"
MOD ::= "\\"
MUL ::= "*"
NEQ ::= "!="
POW ::= "**"
QUESTION ::= "?"
RBRACE ::= "}"
RBRACK ::= "]"
RPAREN ::= ")"
SEM ::= ";"
SHOW ::= "#show"
EDGE ::= "#edge"
PROJECT ::= "#project"
HEURISTIC ::= "#heuristic"
SHOWSIG ::= "#showsig"
SLASH ::= "/"
SUB ::= "-"
SUM ::= "#sum"
SUMP ::= "#sum+"
SUPREMUM ::= "#sup"
TRUE ::= "#true"
BLOCK ::= "#program"
UBNOT
UMINUS
VBAR ::= "|"
VOLATILE ::= "#volatile"
WIF ::= ":~"
XOR ::= "^"
PARSE_LP ::= "<program>"
PARSE_DEF ::= "<define>"
ANY ::= "any"
UNARY ::= "unary"
BINARY ::= "binary"
LEFT ::= "left"
RIGHT ::= "right"
HEAD ::= "head"
BODY ::= "body"
DIRECTIVE ::= "directive"
THEORY ::= "#theory"
SYNC ::= "EOF"
rkaminsk commented 1 year ago

Thanks, for letting us know. You might also be interested in potassco/guide#25.

mingodad commented 1 year ago

Hello @rkaminsk thanks for the link ! That link is also viable on https://www.bottlecaps.de/rr/ui, the one I showed above is a direct conversion from the parser at clingo/libgringo/src/input/nongroundgrammar.yy and it's complete (except the manual inclusion of the tokens).