granule-project / granule

A statically-typed linear functional language with graded modal types for fine-grained program reasoning
https://granule-project.github.io
BSD 3-Clause "New" or "Revised" License
589 stars 35 forks source link

Grammar railroad diagram #233

Open mingodad opened 10 months ago

mingodad commented 10 months ago

While trying to add frontend/src/Language/Granule/Syntax/Parser.y to https://mingodad.github.io/parsertl-playground/playground/ an Yacc/Lex compatible online editor/tester I found that the grammar has too many conflicts and didn't continue but at least I've got an EBNF understood by https://www.bottlecaps.de/rr/ui to generate a nice navigable railroad diagram, see bellow.

//
// EBNF to be viewd at https://www.bottlecaps.de/rr/ui
//
// Copy and paste this at https://www.bottlecaps.de/rr/ui in the 'Edit Grammar' tab
// then click the 'View Diagram' tab.
//

TopLevel::=
      module CONSTR where NL Defs
    | module CONSTR hiding '(' Ids ')' where NL Defs
    | language CONSTR NL TopLevel
    | Defs

Ids::=
      CONSTR
    | CONSTR ',' Ids

Defs::=
      Def
    | DataDecl
    | Import
    | DataDecl NL Defs
    | Def NL Defs
    | Import NL Defs

NL::=
      nl NL
    | nl

Import::=
      import

Def::=
      Sig NL Bindings
    | Sig NL Spec NL Bindings

Spec::=
      spec SpecList

SpecList::=
      Example ';' SpecList
    | Components
    | /*%empty*/

Example::=
      Expr '=' Expr '!' CONSTR
    | Expr '=' Expr

Components::=
      VAR
    | VAR '%' Coeffect
    | VAR ',' Components
    | VAR '%' Coeffect ',' Components
    | /*%empty*/

DataDecl::=
      data CONSTR TyVars KindAnn where DataConstrs
    | data CONSTR TyVars KindAnn '=' DataConstrs

Sig::=
      VAR ':' TypeScheme

Bindings::=
      Binding ';' NL Bindings
    | Binding

Binding::=
      VAR '=' Expr
    | VAR Pats '=' Expr

DataConstrs::=
      DataConstr DataConstrNext
    | /*%empty*/

DataConstr::=
      CONSTR ':' TypeScheme
    | CONSTR TyParams

DataConstrNext::=
      '|' DataConstrs
    | ';' DataConstrs
    | /*%empty*/

TyVars::=
      '(' VAR ':' Kind ')' TyVars
    | VAR TyVars
    | /*%empty*/

KindAnn::=
      ':' Kind
    | /*%empty*/

Pats::=
      PAtom
    | PAtom Pats

PAtom::=
      VAR
    | '_'
    | INT
    | FLOAT
    | CONSTR
    | '(' NAryConstr ')'
    | '[' PAtom ']'
    | '!' PAtom
    | '[' NAryConstr ']'
    | '(' PMolecule ',' PMolecule ')'

PMolecule::=
      NAryConstr
    | PAtom

NAryConstr::=
      CONSTR Pats

ForallSig::=
      '{' VarSigs '}'
    | Vars1

Forall::=
      forall ForallSig '.'
    | forall ForallSig '.' '{' Constraints '}' "=>"

Constraints::=
      Constraint ',' Constraints
    | Constraint

TypeScheme::=
      Type
    | Forall Type
    | '{' Constraints '}' "=>" Type

VarSigs::=
      VarSig ',' VarSigs
    | VarSig

VarSig::=
      Vars1 ':' Kind
    | Vars1

Vars1::=
      VAR
    | VAR Vars1

Hint::=
      '-' VAR
    | '-' VAR INT

Hints::=
      Hint
    | Hint Hints

Kind::=
      Type

Type::=
      '(' VAR ':' Type ')' "->" Type
    | '(' VAR ':' Type ')' '%' Coeffect "->" Type
    | TyJuxt
    | '!' TyAtom
    | '*' TyAtom
    | Type "->" Type
    | Type '%' Coeffect "->" Type
    | Type "×" Type
    | Type '&' Type
    | TyAtom '[' Coeffect ']'
    | TyAtom "*{" Guarantee '}'
    | TyAtom '[' ']'
    | TyAtom '<' Effect '>'
    | case Type of TyCases
    | exists '{' VAR ':' Type '}' '.' Type

TyJuxt::=
      TyJuxt '`' TyAtom '`'
    | TyJuxt TyAtom
    | TyAtom
    | TyAtom '+' TyAtom
    | TyAtom '-' TyAtom
    | TyAtom '*' TyAtom
    | TyAtom '^' TyAtom
    | TyAtom "/\\" TyAtom
    | TyAtom "\\/" TyAtom
    | TyAtom "<=" TyAtom
    | TyAtom '.' "<=" TyAtom
    | TyAtom ">=" TyAtom
    | TyAtom '.' ">=" TyAtom
    | TyAtom "==" TyAtom
    | TyAtom "/=" TyAtom
    | TyAtom "=>" TyAtom

TyCases::=
      TyCase TyCasesNext

TyCasesNext::=
      ';' TyCases
    | /*%empty*/

TyCase::=
      Type "->" Type

Constraint::=
      TyJuxt TyAtom
    | TyAtom '>' TyAtom
    | TyAtom '<' TyAtom
    | TyAtom "<=" TyAtom
    | TyAtom '.' "<=" TyAtom
    | TyAtom ">=" TyAtom
    | TyAtom '.' ">=" TyAtom
    | TyAtom "==" TyAtom
    | TyAtom "/=" TyAtom
    | TyAtom "=>" TyAtom
    | TyAtom "⨱" TyAtom

TyAtom::=
      CONSTR
    | '(' ',' ')'
    | VAR
    | INT
    | FLOAT
    | '(' Type ')'
    | '(' Type ',' Type ')'
    | TyAtom ':' Kind
    | '{' CoeffSet '}'
    | '{' CoeffSet '}' '.'

TyParams::=
      TyAtom TyParams
    | /*%empty*/

Coeffect::=
      INT
    | '.' INT
    | "∞"
    | FLOAT
    | CONSTR
    | VAR
    | Coeffect ".." Coeffect
    | Coeffect '+' Coeffect
    | Coeffect '*' Coeffect
    | Coeffect '-' Coeffect
    | Coeffect '^' Coeffect
    | Coeffect "/\\" Coeffect
    | Coeffect "\\/" Coeffect
    | '(' Coeffect ')'
    | '{' CoeffSet '}'
    | '{' CoeffSet '}' '.'
    | Coeffect ':' Kind
    | '(' Coeffect ',' ',' Coeffect ')'
    | '(' Coeffect "×" Coeffect ')'

CoeffSet::=
      CoeffSetElems
    | /*%empty*/

CoeffSetElems::=
      CoeffSetElem ',' CoeffSetElems
    | CoeffSetElem

CoeffSetElem::=
      CONSTR
    | VAR

Effect::=
      '{' EffSet '}'
    | /*%empty*/
    | TyJuxt

EffSet::=
      Eff ',' EffSet
    | Eff

Eff::=
      CONSTR

Guarantee::=
      CONSTR

Expr::=
      let LetBind MultiLet
    | "\\" '(' PAtom ':' Type ')' "->" Expr
    | "\\" PAtom "->" Expr
    | let LetBindEff MultiLetEff
    | try Expr as '[' PAtom ']' in Expr catch Expr
    | try Expr as '[' PAtom ']' ':' Type in Expr catch Expr
    | case Expr of Cases
    | if Expr then Expr else Expr
    | clone Expr as CopyBind in Expr
    | endorse Expr as CopyBind in Expr
    | pack '<' Type ',' Atom '>' as exists '{' VAR ':' Type '}' '.' Type
    | unpack '<' VAR ',' VAR '>' '=' Expr in Expr
    | Form

LetBind::=
      PAtom ':' Type '=' Expr
    | PAtom '=' Expr
    | NAryConstr ':' Type '=' Expr
    | NAryConstr '=' Expr

CopyBind::=
      PAtom ':' Type
    | PAtom

MultiLet::=
      ';' LetBind MultiLet
    | in Expr

LetBindEff::=
      PAtom "<-" Expr
    | PAtom ':' Type "<-" Expr

MultiLetEff::=
      ';' LetBindEff MultiLetEff
    | in Expr

Cases::=
      Case CasesNext

CasesNext::=
      ';' Cases
    | /*%empty*/

Case::=
      PAtom "->" Expr
    | NAryConstr "->" Expr

Form::=
      Form '+' Form
    | Form '-' Form
    | Form '*' Form
    | Form '/' Form
    | Form '<' Form
    | Form '>' Form
    | Form "<=" Form
    | Form ">=" Form
    | Form "==" Form
    | Form "/=" Form
    | Form "∘" Form
    | Form '.' Form
    | Juxt

Juxt::=
      Juxt '`' Atom '`'
    | Juxt Atom
    | Atom
    | Juxt '@' TyAtom

Hole::=
      "{!" Vars1 "!}"
    | "{!" Hints "!}"
    | "{!" Hints Vars1 "!}"
    | "{!" Vars1 Hints "!}"
    | "{!" "!}"
    | '?'

Atom::=
      '(' Expr ')'
    | INT
    | FLOAT
    | VAR
    | '[' Expr ']'
    | '#' INT
    | '#' FLOAT
    | CONSTR
    | '#' CONSTR
    | '(' Expr ',' Expr ')'
    | CHAR
    | STRING
    | '#' CHAR
    | '#' STRING
    | Hole
    | share Expr
buggymcbugfix commented 5 months ago

Thanks, I tried following your instructions, but the site https://www.bottlecaps.de seems to be down.

mingodad commented 5 months ago

It's IPV6 now but there is a mirror with IPV4 here https://rr.red-dove.com/ui also for offline usage the project is here https://github.com/GuntherRademacher/rr