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

entrypoints [Def], Exp ;

token Id ((letter|digit|["[]_"])+) ;

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

TypeDef. Def ::= "type" TypeSig1 [Decl] ;
VarDef.  Def ::= Id ":" TypeSig ":=" Exp ;
separator Def ";" ;

Decl. Decl  ::= Id ":" TypeSig ;
[].  [Decl] ::= ;
(:). [Decl] ::= "|" Decl [Decl];

TypeFun. TypeSig  ::= TypeSig1 "→"  TypeSig ;
TypeFun. TypeSig  ::= TypeSig1 "->" TypeSig ;
TypeApp. TypeSig1 ::= Id [TypeSig2] ;
TypeVar. TypeSig2 ::= Id ;
coercions TypeSig 2;

separator nonempty TypeSig2 "" ;

ExpLet.   Exp  ::= "let" "{" [Assign] "}" "in" Exp1 ;
ExpAbs.   Exp1 ::= "λ"  [Id] "." Exp1 ;
ExpAbs.   Exp1 ::= "\\" [Id] "." Exp1 ;
ExpApp.   Exp1 ::= Exp2 [Exp2] ;
ExpVar.   Exp2 ::= Id ;

Assign. Assign ::= Id ":=" Exp ;
separator nonempty Assign ";" ;

separator nonempty Exp2 "" ;
coercions Exp 2 ;

separator nonempty Id "" ;