entrypoints Module, Exp ;
comment "--" ;
comment "{-" "-}" ;
layout "where", "let", "split", "mutual" ;
layout stop "in" ;
-- Do not use layout toplevel as it makes pExp fail!
Module. Module ::= "module" AIdent "where" "{" [Imp] [Decl] "}" ;
Import. Imp ::= "import" AIdent ;
separator Imp ";" ;
DeclDef. Decl ::= AIdent [AIdent] "=" ExpWhere ;
DeclType. Decl ::= AIdent ":" Exp ;
DeclPrim. Decl ::= "primitive" AIdent ":" Exp ;
DeclData. Decl ::= "data" AIdent [AIdent] "=" [Label] ;
DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ;
DeclOpaque. Decl ::= "opaque" AIdent ;
DeclTransp. Decl ::= "transparent" AIdent ;
separator Decl ";" ;
Where. ExpWhere ::= Exp "where" "{" [Decl] "}" ;
NoWhere. ExpWhere ::= Exp ;
Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ;
Lam. Exp ::= "\\" AIdent [AIdent] "->" Exp ;
Split. Exp ::= "split" "{" [Branch] "}" ;
Fun. Exp1 ::= Exp2 "->" Exp1 ;
Pi. Exp1 ::= [PseudoTDecl] "->" Exp1 ;
Sigma. Exp1 ::= [PseudoTDecl] "*" Exp1 ;
App. Exp2 ::= Exp2 Exp3 ;
Fst. Exp3 ::= Exp3 ".1" ;
Snd. Exp3 ::= Exp3 ".2" ;
Pair. Exp3 ::= "(" Exp "," Exp ")" ;
Var. Exp3 ::= AIdent ;
U. Exp3 ::= "U" ;
coercions Exp 3 ;
-- Branches
Branch. Branch ::= AIdent [AIdent] "->" ExpWhere ;
separator Branch ";" ;
-- Labelled sum alternatives
Label. Label ::= AIdent [VTDecl] ;
separator Label "|" ;
-- Telescopes
VTDecl. VTDecl ::= "(" AIdent [AIdent] ":" Exp ")" ;
terminator VTDecl "" ;
-- Nonempty telescopes with Exp:s, this is hack to avoid ambiguities
-- in the grammar when parsing Pi
PseudoTDecl. PseudoTDecl ::= "(" Exp ":" Exp ")" ;
terminator nonempty PseudoTDecl "" ;
position token AIdent ((letter|'\''|'_')(letter|digit|'\''|'_')*) ;
terminator AIdent "" ;