Core.cf

--- Input file to BNF Converter
---   This describes the labelled BNF Grammar of
---   Mini-TT concrete syntax

-- Expressions

ELam.     Exp1   ::= "\\" Patt1 "." Exp1 ;
ESet.     Exp3   ::= "U" ;
EPi.      Exp1   ::= "Pi"  Patt1 ":" Exp1 "." Exp1 ;
ESig.     Exp1   ::= "Sig" Patt1 ":" Exp1 "." Exp1 ;
EOne.     Exp3   ::= "1";
Eunit.    Exp3   ::= "0";
EPair.    Exp    ::= Exp1 "," Exp ;
ECon.     Exp2   ::= "$" Ident Exp3;
EData.    Exp1   ::= DataTk "(" [Summand] ")" ;
ECase.    Exp1   ::= CaseTk "(" [Branch] ")" ;
EFst.     Exp3   ::= Exp3 ".1" ;
ESnd.     Exp3   ::= Exp3 ".2" ;
EApp.     Exp2   ::= Exp2 Exp3 ;
EVar.     Exp3   ::= Ident ;
EVoid.    Exp3   ::= "Void" ;
EDec.     Exp1   ::= Decl ";" Exp1 ;
EPN.      Exp3   ::= "PN" ;

-- syntax sugars
eArrow.   Exp1   ::= Exp2 "->" Exp1 ;
eTimes.   Exp1   ::= Exp2 "*"  Exp1 ;
define eArrow a b = EPi  Punit a b ;
define eTimes a b = ESig Punit a b ;

coercions Exp 3 ;

-- declarations
Def.      Decl ::= "let"    Patt1 ":" Exp1 "=" Exp1 ;
Drec.     Decl ::= "letrec" Patt1 ":" Exp1 "=" Exp1 ;

-- patterns
PPair.    Patt    ::= Patt1 "," Patt ;
Punit.    Patt1   ::= "_" ;
PVar.     Patt1   ::= Ident ;

coercions Patt 1 ;

Summand.  Summand ::= Ident      Exp3;
separator Summand "|" ;

Branch.   Branch  ::= Ident "->" Exp1 ;
separator Branch  "|" ;

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

separator nonempty Ident "" ;

position token CaseTk {"fun"} ;
position token DataTk {"Sum"} ;