Grammar.cf

entrypoints Defs;

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

layout "let";
layout stop "in";
layout toplevel;

Defs.      Defs ::= [Def];
Def.       Def ::= PIdent [Arg] "=" Expr;
DefType.   Def ::= PIdent ":" Expr;

separator  Def ";";

Let.      Expr  ::= "let" "{" [Def] "}" "in" Expr;
Lam.      Expr  ::= PLam [Binder] "->" Expr;
Arr.      Expr1 ::= Expr2 "->" Expr1;
Pi.       Expr1 ::= [TypedVar] "->" Expr1;
Prod.     Expr2 ::= Expr3 "*" Expr2;
Sigma.    Expr2 ::= [TypedVar] "*" Expr2;
Over.     Expr3 ::= Expr4 "|" Expr3;
Id.       Expr4 ::= Expr5 "=" Expr5;
Pair.     Expr5 ::= Expr5 "," Expr6;
Pmap.     Expr6 ::= Expr6 "<*>" Expr7;
App.      Expr7 ::= Expr7 Expr8;
Var.      Expr8 ::= Arg;
Nat.      Expr8 ::= PNat;
Suc.      Expr8 ::= PSuc;
Rec.      Expr8 ::= PR;
Idp.      Expr8 ::= PIdp;
Coe.      Expr8 ::= PCoe;
Proj1.    Expr8 ::= PProjl;
Proj2.    Expr8 ::= PProjr;
Pcon.     Expr8 ::= Ppcon;
Iso.      Expr8 ::= PIso;
NatConst. Expr8 ::= PInt;
Universe. Expr8 ::= U;
_.        Expr  ::= Expr1;
_.        Expr1 ::= Expr2;
_.        Expr2 ::= Expr3;
_.        Expr3 ::= Expr4;
_.        Expr4 ::= Expr5;
_.        Expr5 ::= Expr6;
_.        Expr6 ::= Expr7;
_.        Expr7 ::= Expr8;
Paren.    Expr8 ::= PPar Expr ")";

Arg.       Arg ::= PIdent;
NoArg.     Arg ::= Pus;
terminator Arg "";

-- Like Arg, but cannot be empty
Binder.   Binder ::= Arg;
separator nonempty Binder "";

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

position token U ('T' 'y' 'p' 'e' digit*);
position token PLam '\\';
position token PPar '(';
position token PInt digit+;
position token PIdp 'i' 'd' 'p';
position token PR 'R';
position token PSuc 's' 'u' 'c';
position token PNat 'N' 'a' 't';
position token Pus '_';
position token PCoe 'c' 'o' 'e';
position token Ppcon 'p' 'c' 'o' 'n';
position token PProjl 'p' 'r' 'o' 'j' '1';
position token PProjr 'p' 'r' 'o' 'j' '2';
position token PIso 'i' 's' 'o';
position token PIdent (letter(letter|digit|'\''|'_')*);