--- 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"} ;