96 lines
3 KiB
CFEngine3
96 lines
3 KiB
CFEngine3
|
||
-------------------------------------------------------------------------------
|
||
-- * 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 ;
|
||
separator nonempty Inj " " ;
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * Expressions
|
||
-------------------------------------------------------------------------------
|
||
|
||
EAnn. Exp4 ::= "(" Exp ":" Type ")";
|
||
EVar. Exp3 ::= LIdent;
|
||
EInj. Exp3 ::= UIdent;
|
||
ELit. Exp3 ::= Lit;
|
||
EApp. Exp2 ::= Exp2 Exp3;
|
||
EAppInf. Exp2 ::= Exp3 "`" Exp3 "`";
|
||
EAdd. Exp1 ::= Exp1 "+" Exp2;
|
||
ELet. Exp ::= "let" Bind "in" Exp;
|
||
EAbs. Exp ::= "\\" LIdent "." Exp;
|
||
ECase. Exp ::= "case" Exp "of" "{" [Branch] "}";
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * 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
|
||
-------------------------------------------------------------------------------
|
||
|
||
terminator Def ";";
|
||
terminator Branch ";" ;
|
||
|
||
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 "{-" "-}";
|