search

maude-lang / Maude

Language based on Rewriting Logic
GNU General Public License v2.0
78 stars 10 forks source link

Grammar railroad diagram #6

Open mingodad opened 1 year ago

mingodad commented 1 year ago

After a bit of manual fixes I made an approximated EBNF understood by https://www.bottlecaps.de/rr/ui to generate a railroad diagram.

Copy and paste one of the EBNF shown bellow on https://www.bottlecaps.de/rr/ui on the tab Edit Grammar then click the tab View Diagram:

MaudeTop ::=
    ( SystemCommand | Command | DebuggerCommand |
       Module | Theory | View )+

SystemCommand ::= 'in' FileName | 'load' FileName | 'sload' FileName |
    'quit' | 'eof' | 'popd' | 'pwd' |
    'cd' Directory | 'push' Directory |
    'ls' ( LsFlag )? ( Directory )?

Command ::= 'select' ModId '.' |
    'parse' ( 'in' ModId ':' )? Term '.' |
    ( 'debug' )? 'reduce' ( 'in' ModId ':' )? Term '.' |
    ( 'debug' )? 'rewrite' ( ( Nat )? )? ( 'in' ModId ':' )? Term '.' |
    ( 'debug' )? 'frewrite' ( DoubleBound )? ( 'in' ModId ':'
        )? Term '.' |
    ( 'debug' )? 'erewrite' ( DoubleBound )? ( 'in' ModId ':' )?
        Term '.' |
    ( 'debug' )? ( 'srewrite' | 'dsrewrite' ) ( ( Nat )? )? ( 'in' ModId ':' )?
        Term 'using' Strat '.' |
    'check' ( 'in' ModId ':' )? Term '.' |
    ( 'match' | 'xmatch' ) ( ( Nat )? )? ( 'in' ModId ':' )?
        Term '<=?' Term ( 'such' 'that' Condition )? '.' |
    ( 'debug' )? 'variant' 'match' ( ( Nat )? )? ( 'in' ModId ':' )?
        Term '<=?' Term ( 'such' 'that' Condition )? '.' |
    ( 'irredudant' )? 'unify' ( ( Nat )? )? ( 'in' ModId ':' )?
        UnificationEquation  ( '/\' UnificationEquation )* '.' |
    ( 'debug' )? ( 'filtered' )? 'variant' 'unify' ( ( Nat )? )? ( 'in' ModId ':' )?
        UnificationEquation  ( '/\' UnificationEquation )* '.' |
    ( 'debug' )? 'get' ( 'irredundant' )? 'variants' ( ( Nat )? )? ( 'in' ModId ':' )? Term '.' |
    ( 'debug' )? 'search' ( DoubleBound )? ( 'in' ModId ':' )? Term SearchType Term
        ( 'such' 'that' Condition )? '.' |
    ( 'debug' )? ( '{fold}' )? 'vu-narrow' ( VariantOptionList )? ( DoubleBound )?
        ( 'in' ModId ':' )? Term SearchType Term '.' |
    ( 'debug' )? 'continue' Nat '.' |
    'loop' ( 'in' ModId ':' )? Term '.' |
    ( TokenString ) |
    'trace' ( 'select' | 'deselect' | 'include' | 'exclude' )
        ( OpId | ( OpForm ) )+ '.' |
    'print' ( 'conceal' | 'reveal' ) ( OpId | ( OpForm ) )+ '.' |
    'break' ( 'select' | 'deselect' ) ( OpId | ( OpForm ) )+ '.' |
    'show' ShowItem ( ModId )? '.' |
    'show' 'view' ( ViewId )? '.' |
    'show' 'modules' '.' |
    'show' 'views' '.' |
    'show' 'search' 'graph' '.' |
    'show' 'path' ( 'labels' )? Nat '.'
    'do' 'clear' 'memo' ( ModId )? '.' |
    'set' SetOption ( 'on' | 'off' ) '.'

DoubleBound ::= ( Nat ( ',' Nat )? )? | ( ',' Nat )?

SearchType ::= '=>1' | '=>+' | '=>*' | '=>!'

UnificationEquation ::= Term '=?' Term

ShowItem ::= 'module' | 'all' | 'desugared' | 'sorts' | 'ops' | 'vars' | 'mbs' |
    'eqs' | 'rls' | 'strats' | 'sds' | 'summary' | 'kinds' | 'profile'

SetOption ::= 'show' ShowOption |
    'print' PrintOption |
    'trace' ( TraceOption )? |
    'break' | 'verbose' | 'profile' |
    'clear' ( 'memo' | 'rules' | 'profile' ) |
    'protect' ModId |
    'extend' ModId |
    'include' ModId

ShowOption ::= 'advise' | 'stats' | 'loop' 'stats' | 'timing' |
    'loop' 'timing' | 'breakdown' | 'command' | 'gc'

PrintOption ::= 'mixfix' | 'flat' | 'with' 'parentheses' |
    'with' 'aliases' | 'conceal' | 'number' | 'rat' | 'color' |
    'format' | 'graph' | 'attribute' | 'attribute' 'newline' |
    'constants' 'with' 'sorts'

TraceOption ::= 'condition' | 'whole' | 'substitution' | 'select' |
    'mbs' | 'eqs' | 'rls' | 'sds' | 'rewrite' | 'body'

VariantOptionList ::= '{' VariantOption ( ',' VariantOptionList )* '}'

VariantOption ::= 'filter' | 'delay'

DebuggerCommand ::= 'resume' '.' | 'abort' '.' | 'step' '.' | 'where' '.'

Module ::= 'fmod' ModId ( ParameterList )? 'is' ModElt* 'endfm' |
    'mod' ModId ( ParameterList )? 'is' ModElt_* 'endm' |
    'smod' ModId ( ParameterList )? 'is' SmodElt* 'endsm'

Theory ::= 'fth' ModId 'is' ModElt* 'endfth' |
    'th' ModId 'is' ModElt_* 'endth' |
    'sth' ModId 'is' SmodElt* 'endsth'

View ::= 'view' ViewId ( ParameterList )? 'from' ModExp 'to' ModExp 'is'
             ViewElt*
           'endv'

ParameterList ::= '{' ParameterDecl ( ',' ParameterDecl )* '}'

ParameterDecl ::= ParameterId '::' ModExp

ModElt ::= 'including' ModExp '.' |
    'extending' ModExp '.' |
    'protecting' ModExp '.' |
    'sorts' Sort+ '.' |
    'subsorts' Sort+ ( '<' Sort+ )+ '.' |
    'op' OpForm ':' Type* Arrow Type ( Attr )? '.' |
    'ops' ( OpId | ( OpForm ) )+ ':' Type* Arrow Type
           ( Attr )? '.' |
    'vars' VarId+ ':' Type '.' |
    Statement ( StatementAttr )? '.'

ViewElt ::= 'var' 'var'Id+ ':' Type '.' |
    'sort' Sort 'to' Sort '.' |
    'label' LabelId 'to' LabelId '.' |
    'op' OpForm 'to' OpForm '.'  |
    'op' OpForm ':' Type* Arrow Type 'to' OpForm '.' |
    'op' Term 'to' 'term' Term '.' |
    'strat' StratId 'to' StratId '.' |
    'strat' StratId ( ':' Type* )? '@' Type 'to' StratId '.' |
    'strat' StratCall 'to' 'expr' Strat '.'

ModExp ::= ModId |
    ( ModExp ) |
    ModExp '+' ModExp |
    ModExp '*' Renaming
    ModExp '{' ViewId ( ',' ViewId )* '}'

Renaming ::= ( RenamingItem ( ',' RenamingItem )* )

RenamingItem ::= 'sort' Sort 'to' Sort |
    'label' LabelId 'to' LabelId |
    'op' OpForm ToPartRenamingItem |
    'op' OpForm ':' Type* Arrow Type ToPartRenamingItem
    'strat' StratId 'to' StratId |
    'strat' StratId ( ':' Type* )? '@' Type 'to' StratId |

ToPartRenamingItem ::= 'to' OpForm ( Attr )?

Arrow ::= '->' | '~>'

Type ::= Sort | Kind

Kind ::= ( Sort (',' Sort )* )?

Sort ::= SortId | Sort '{' Sort ( ',' Sort )* '}'

ModElt_ ::= ModElt |
    Statement_ ( StatementAttr )? '.'

SmodElt ::= 'including' ModExp '.' |
    'extending' ModExp '.' |
    'protecting' ModExp '.' |
    'vars' VarId+ ':' Type '.' |
    'strats' StratId+ ( ':' Type* )? '@' Type ( StratAttr )? '.'
    StratStatement ( StatementAttr )? '.'

Statement  ::=  'mb' ( Label )? Term ':' Sort |
    'cmb' ( Label )? Term ':' Sort 'if' Condition |
    'eq' ( Label )? Term '=' Term |
    'ceq' ( Label )? Term '=' Term 'if' Condition

Statement_ ::= 'rl' ( Label )? Term '=>' Term |
    'crl' ( Label )? Term '=>' Term 'if' Condition_

StratStatement ::= 'sd' StratCall ':=' Strat |
    'csd' StratCall ':=' Strat 'if' Condition

Label ::= ( LabelId )? ':'

Condition ::= ConditionFragment ( '/\' ConditionFragment )*

Condition_ ::= ConditionFragment_
                 ( '/\' ConditionFragment_ )*

ConditionFragment ::= Term '=' Term | Term ':=' Term
                        | Term ':' Sort

ConditionFragment_ ::= ConditionFragment | Term '=>' Term

Attr ::=
    ( ( 'assoc' | 'comm' |
        ( 'left' | 'right' )? 'id:' Term |
        'idem' | 'iter' | 'memo' | 'ditto' |
        'config' | 'obj' | 'msg' | 'ctor' |
        'metadata' StringId
        'strat' ( Nat+ ) |
        'poly' ( Nat+ ) |
        'frozen' ( ( Nat+ ) )? |
        'prec' Nat |
        'gather' ( ( 'e' | 'E' | '&' )+ ) |
        'format' ( Token+ ) |
        'special' ( Hook+ ) )+ )?

StratAttr ::= ( 'metadata' StringId )?

StatementAttr ::=
    ( ( 'nonexec' |
        'metadata' StringId |
        'label' LabelId  |
        'print' PrintItem* )+ )?

StatementAttrEq ::=
    ( ( StatementAttr | 'otherwise' | 'variant' )+ )?

StatementAttrRl ::=
    ( ( StatementAttr | 'narrowing' )+ )?

PrintItem ::= StringId | VarId | VarAndSortId

Hook ::= 'id-hook' Token ( ( TokenString ) )? |
    ( 'op-hook' | 'term-hook' ) Token ( TokenString )

Strat ::= 'idle' | 'fail' |
    RuleApp | 'top'( RuleApp ) |
    Strat '?' Strat ':' Strat |
    TestVariant Term ( 'such' 'that' Condition )?
    Strat ';' Strat |
    Strat | Strat |
    Strat '*' |
    MrewVariant Term ( 'such' 'that' Condition )? 'by' VarStratList
    StratCall
    Strat '+'
    Strat 'or-else' Strat
    'not'( Strat )
    Strat '!'
    'try'( Strat )
    'test'( Strat )

RuleApp ::= LabelId ( ( Substitution )? )? ( '{' Strat (',' Strat)* '}' )?

Substitution ::= VarId '<-' Term |
    Substitution ',' Substitution

StratCall ::= StratId ( '()' )? |
    StratId ( Term (',' Term)* )

VarStratList ::= VarId 'using' Strat |
    VarStratList ',' VarStratList

TestVariant ::= 'match' | 'xmatch' | 'amatch'

MrewVariant ::= 'matchrew' | 'xmatchrew' | 'amatchrew'

FileName    //%%% OS 'dependent'
Directory   //%%% OS 'dependent'
LsFlag      //%%% OS 'dependent'

StringId    //%%% 'characters' 'enclosed' 'in' 'double' 'quotes' "'.''.''.'"
ModId       //%%% 'simple' 'identifier'',' 'by' 'convention' 'all' 'capitals'
ViewId      //%%% 'simple' 'identifier'',' 'by' 'convention' 'capitalized'
ParameterId //%%% 'simple' 'identifier'',' 'by' 'convention' 'single' 'capital'
SortId      //%%% 'simple' 'identifier'',' 'by' 'convention' 'capitalized'
VarId       //%%% 'simple' 'identifier'',' 'by' 'convention' 'capitalized'
VarAndSortId //%%% 'an' 'identifier' 'consisting' 'of' 'a' 'variable' 'name'
                   'followed' 'by' 'a' 'colon' 'followed' 'by' 'a' 'sort' 'name'
OpId        //%%% 'identifier' 'possibly' 'with' 'underscores'
OpForm ::= OpId | ( OpForm ) | OpForm+
Nat         //%%% 'a' 'natural' 'number'
Term ::= Token | ( Term ) | Term+
Token       //%%% 'sequence' 'of' 'printable' ASCII 'characters' 'delimited' 'by'
                  'whitespace''.' The 'symbols' (',' )',' (',' )?',' '{,' '}' 'and' 'comma' 'form'
                  'separate' 'tokens' 'themselves'',' 'unless' 'backquoted'
TokenString ::= Token | ( TokenString ) | TokenString*
LabelId     //%%% 'simple' 'identifier'
StratId     //%%% 'simple' 'identifier'