entrypoints Module, Exp ;

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

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

Module.   Module ::= "module" AIdent "where" "{" [Imp] [Def] "}" ;

Import.   Imp ::= "import" AIdent ;
separator Imp ";" ;

Def.       Def ::= AIdent [Arg] "=" ExpWhere ;
DefTDecl.  Def ::= AIdent ":" Exp ;
DefData.   Def ::= "data" AIdent [Arg] "=" [Sum] ;
-- TODO: Mutual not working.
-- NB: No iterated mutuals allowed!
-- DefMutual. Def ::= "mutual" "{" [Def] "}" "end" ;

separator  Def ";" ;

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

Let.      Exp  ::= "let" "{" [Def] "}" "in" Exp ;
Lam.      Exp  ::= "\\" [Binder] "->" Exp ;
Split.    Exp  ::= "split" "{" [Branch] "}" ;
Fun.      Exp1 ::= Exp2 "->" Exp1 ;
Pi.       Exp1 ::= [PiDecl] "->" Exp1 ;
App.      Exp2 ::= Exp2 Exp3 ;
Var.      Exp3 ::= Arg ;
U.        Exp3 ::= "U" ;
Undef.    Exp3 ::= "undefined" ;
PN.       Exp3 ::= "PN" ;
coercions Exp 3 ;

Binder.   Binder ::= Arg ;
separator nonempty Binder "" ;

-- Like Binder, but may be empty
Arg.       Arg ::= AIdent ;
NoArg.     Arg ::= "_" ;
terminator Arg "" ;

-- Branches
Branch.   Branch ::= AIdent [Arg] "->" ExpWhere ;
separator Branch ";" ;

-- Labelled sum alternatives
Sum.      Sum   ::= AIdent [VDecl] ;
separator Sum "|" ;

-- Telescopes
VDecl.     VDecl ::= "(" [Binder] ":" Exp ")" ;
terminator VDecl "" ;

-- Nonempty telescopes with Exp:s, this is hack to avoid ambiguities in the
-- grammar when parsing Pi
PiDecl.   PiDecl ::= "(" Exp ":" Exp ")" ;
terminator nonempty PiDecl "" ;

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