Grammar.cf

entrypoints Defs, Expr;

comment "--";
comment "{-" "-}";

layout "with";
layout toplevel;

Defs.         Defs  ::= [Def];
DefType.      Def   ::= PIdent ":" Expr;
DefFun.       Def   ::= FunCase;
DefFunEmpty.  Def   ::= Pattern;
DefData.      Def   ::= "data" PIdent [DataTele] "=" [Con];
DefDataWith.  Def   ::= "data" PIdent [DataTele] "=" [Con] "with" "{" [FunCase] "}";
DefDataEmpty. Def   ::= "data" PIdent [DataTele];
separator     Def   ";";

FunCase.   FunCase  ::= Pattern "=" Expr;
separator  FunCase  ";";

Pattern.   Pattern  ::= PIdent [ParPat];
ParVar.    ParPat   ::= Arg;
ParLeft.   ParPat   ::= PLeft;
ParRight.  ParPat   ::= PRight;
ParEmpty.  ParPat   ::= PPar ")";
ParPat.    ParPat   ::= PPar Pattern ")";
terminator ParPat   "";

Con.       Con      ::= PIdent [ConTele];
separator  nonempty Con "|";

VarTele.   ConTele  ::= PPar Expr ":" Expr ")";
TypeTele.  ConTele  ::= Expr5;
terminator ConTele  "";

DataTele.  DataTele ::= PPar Expr ":" Expr ")";
terminator DataTele "";

PiTele.    PiTele   ::= PPar Expr ":" Expr ")";
terminator nonempty PiTele "";

Lam.       Expr     ::= PLam [Arg] "->" Expr;
Arr.       Expr1    ::= Expr2 "->" Expr1;
Pi.        Expr1    ::= [PiTele] "->" Expr1;
PathImp.   Expr2    ::= Expr3 "=" Expr3;
At.        Expr3    ::= Expr3 "@" Expr4;
App.       Expr4    ::= Expr4 Expr5;
Var.       Expr5    ::= Arg;
Universe.  Expr5    ::= U;
Interval.  Expr5    ::= I;
ELeft.     Expr5    ::= PLeft;
ERight.    Expr5    ::= PRight;
Path.      Expr5    ::= PPath;
PathCon.   Expr5    ::= Ppath;
Coe.       Expr5    ::= PCoe;
Iso.       Expr5    ::= PIso;
Squeeze.   Expr5    ::= PSqueeze;
_.         Expr     ::= Expr1;
_.         Expr1    ::= Expr2;
_.         Expr2    ::= Expr3;
_.         Expr3    ::= Expr4;
_.         Expr4    ::= Expr5;
Paren.     Expr5    ::= PPar Expr ")";

Arg.       Arg      ::= PIdent;
NoArg.     Arg      ::= Pus;
separator  nonempty Arg "";

position token U ('T' 'y' 'p' 'e' digit*);
position token I 'I';
position token PLeft 'l' 'e' 'f' 't';
position token PRight 'r' 'i' 'g' 'h' 't';
position token PPath 'P' 'a' 't' 'h';
position token Ppath 'p' 'a' 't' 'h';
position token PCoe 'c' 'o' 'e';
position token PIso 'i' 's' 'o';
position token PSqueeze 's' 'q' 'u' 'e' 'e' 'z' 'e';
position token PLam '\\';
position token PPar '(';
position token Pus '_';
position token PIdent (letter(letter|digit|'\''|'_'|'-')*);