-------------------------------------------------------------------------------
-- * PROGRAM
-------------------------------------------------------------------------------

Program. Program ::= [Def];

-------------------------------------------------------------------------------
-- * TOP-LEVEL
-------------------------------------------------------------------------------

DBind. Def ::= Bind;
DSig.  Def ::= Sig;
DData. Def ::= Data; 

Sig.   Sig ::= LIdent ":" Type;
Bind. Bind ::= LIdent [LIdent] "=" Exp;

-------------------------------------------------------------------------------
-- * Types
-------------------------------------------------------------------------------

         TLit.     Type1 ::= UIdent;                 -- τ
         TVar.     Type1 ::= TVar;                   -- α
internal TEVar.    Type1 ::= TEVar;                  -- ά
         TData.    Type1 ::= UIdent "(" [Type] ")";  -- D ()
         TFun.     Type  ::= Type1 "->" Type;        -- A → A
         TAll.     Type  ::= "forall" TVar "." Type; -- ∀α. A 

         MkTVar.  TVar  ::= LIdent;
internal MkTEVar. TEVar ::= LIdent;

-------------------------------------------------------------------------------
-- * DATA TYPES
-------------------------------------------------------------------------------

Data. Data ::= "data" Type "where" "{" [Inj] "}" ;

Inj. Inj ::= UIdent ":" Type ;

-------------------------------------------------------------------------------
-- * Expressions
-------------------------------------------------------------------------------

EVar.  Exp4 ::= LIdent;
EInj.  Exp4 ::= UIdent;
ELit.  Exp4 ::= Lit;
EApp.  Exp3 ::= Exp3 Exp4;
EAdd.  Exp2 ::= Exp2 "+" Exp3;
ELet.  Exp1  ::= "let" Bind "in" Exp1; 
EAbs.  Exp1  ::= "\\" LIdent "." Exp1;
ECase. Exp1  ::= "case" Exp "of" "{" [Branch] "}";
EAnn.  Exp  ::= Exp1 ":" Type;

-------------------------------------------------------------------------------
-- * LITERALS
-------------------------------------------------------------------------------

LInt.  Lit ::= Integer;
LChar. Lit ::= Char;

-------------------------------------------------------------------------------
-- * PATTERN MATCHING 
-------------------------------------------------------------------------------

Branch. Branch ::= Pattern "=>" Exp ;

PVar.        Pattern1 ::= LIdent;
PLit.        Pattern1 ::= Lit;
PCatch.      Pattern1 ::= "_";
PEnum.       Pattern1 ::= UIdent;
PInj.        Pattern  ::= UIdent [Pattern1];

-------------------------------------------------------------------------------
-- * AUX
-------------------------------------------------------------------------------

layout "of", "where";
layout toplevel;

separator Def ";";
separator Branch ";" ;
separator Inj ";";

separator LIdent "";
separator Type " ";
separator TVar " ";
separator nonempty Pattern1 " ";

coercions Pattern 1;
coercions Exp 4;
coercions Type 1 ;

token UIdent (upper (letter | digit | '_')*) ;
token LIdent (lower (letter | digit | '_')*) ;

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