Exp.cf

entrypoints Exp ;

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

layout "where", "let", "split", "mutual", "module" ;
layout stop "in" ;
-- Do not use layout toplevel as it makes pExp fail!

Field.      Fld ::= AIdent "=" Exp ;
separator Fld ",";

DeclDef.    Decl ::= AIdent [AIdent] "=" ExpWhere ;
DeclType.   Decl ::= AIdent ":" Exp ;
DeclOpen.   Decl ::= "open" Exp ; 
DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ;
separator   Decl ";" ;

Where.    ExpWhere ::= Exp "where" "{" [Decl] "}" ;
NoWhere.  ExpWhere ::= Exp ;

Let.      Exp  ::= "let"  "{" [Decl] "}" "in" Exp ;
Lam.      Exp1 ::= "\\" AIdent [AIdent] "->" Exp1 ;
TLam.     Exp1 ::= "\\" "(" PseudoTDecl  ")" "->" Exp1 ;
Fun.      Exp1 ::= Exp2 "->" Exp1 ;
LFun.     Exp1 ::= Exp2 "-o" Exp1 ;
Pi.       Exp1 ::= "(" PseudoTDecl ")" "->" Exp1 ;
Or.       Exp2 ::= Exp2 "\\/" Exp2;
And.      Exp3 ::= Exp3 "/\\" Exp3;
App.      Exp4 ::= Exp4 Exp5 ;
Singleton. Exp5 ::= Exp5 "/"  Exp;
Proj.     Exp5 ::= Exp5 "." AIdent ;
Module.   Exp6 ::= "module" "{" [Decl] "}" ;
Tuple.    Exp6 ::= "(" [Fld] ")" ;
Record.   Exp6 ::= "[" [PseudoTDecl] "]"  ;
Sum.      Exp6 ::= "{" [Label] "}";
Var.      Exp6 ::= AIdent ;
U.        Exp6 ::= "Type" ;
Real.     Exp6 ::= Double ;
Split.    Exp6 ::= "split" "{" [Branch] "}" ;
PrimOp.   Exp6 ::= "primitive" String;
Import.   Exp6 ::= "import" AIdent ;
Con.      Exp6 ::= "'" AIdent;
coercions Exp 6 ;

separator Exp "," ;

-- Branches
Branch.   Branch ::= "'" AIdent "->" ExpWhere ;
separator Branch ";" ;

-- Labelled sum alternatives
Label.    Label   ::= "'" AIdent ;
separator Label "|" ;

-- Nonempty telescopes with Exp:s, this is hack to avoid ambiguities
-- in the grammar when parsing Pi
PseudoTDecl.  PseudoTDecl ::=  Exp ":" Exp ;
WPseudoTDecl. PseudoTDecl ::=  Exp "::" Weight Exp ;

Positive. Weight ::= "+" ;
Negative. Weight ::= "-" ;
Exact.    Weight ::= Integer ;

separator PseudoTDecl ";" ;

position token AIdent ((letter|'_'|'`')(letter|digit|'\''|'_')*) ;
terminator AIdent "" ;