entrypoints Module, Exp ;
comment "--" ;
comment "{-" "-}" ;
layout "where", "let", "of", "split" ; -- , "mutual" ;
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] ;
-- Anders: This is kind of an ugly way to get mutual to work, but at least it
-- works, I guess there is a bug in bnfc when handling layout blocks and lists
-- TODO: Bug report?
-- DefMutual. Def ::= Def "mutual" "{" [Def] "}" ;
-- Mutual. Def ::= "mutual" "{" [Def] "}" ;
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|'\''|'_')*) ;