113 lines
3.6 KiB
CFEngine3
113 lines
3.6 KiB
CFEngine3
|
||
-------------------------------------------------------------------------------
|
||
-- * PROGRAM
|
||
-------------------------------------------------------------------------------
|
||
|
||
Program. Program ::= [Def];
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * TOP-LEVEL
|
||
-------------------------------------------------------------------------------
|
||
|
||
DBind. Def ::= Bind;
|
||
DSig. Def ::= Sig;
|
||
DData. Def ::= Data;
|
||
|
||
internal Sig. Sig ::= LIdent ":" Type;
|
||
SigS. Sig ::= VarName ":" Type;
|
||
internal Bind. Bind ::= LIdent [LIdent] "=" Exp;
|
||
BindS. Bind ::= VarName [LIdent] "=" Exp;
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * Types
|
||
-------------------------------------------------------------------------------
|
||
|
||
internal TLit. Type3 ::= UIdent; -- τ
|
||
TIdent. Type3 ::= UIdent;
|
||
TVar. Type3 ::= TVar; -- α
|
||
TApp. Type2 ::= Type2 Type3 ;
|
||
TFun. Type1 ::= Type1 "->" Type; -- A → A
|
||
TAll. Type ::= "forall" TVar "." Type; -- ∀α. A
|
||
internal TEVar. Type1 ::= TEVar; -- ά
|
||
internal TData. Type1 ::= UIdent "(" [Type] ")"; -- D ()
|
||
|
||
MkTVar. TVar ::= LIdent;
|
||
internal MkTEVar. TEVar ::= LIdent;
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * DATA TYPES
|
||
-------------------------------------------------------------------------------
|
||
|
||
Data. Data ::= "data" Type "where" "{" [Inj] "}" ;
|
||
|
||
Inj. Inj ::= UIdent ":" Type ;
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * PATTERN MATCHING
|
||
-------------------------------------------------------------------------------
|
||
|
||
Branch. Branch ::= Pattern "=>" Exp ;
|
||
|
||
PVar. Pattern1 ::= LIdent;
|
||
PLit. Pattern1 ::= Lit;
|
||
PCatch. Pattern1 ::= "_";
|
||
PEnum. Pattern1 ::= UIdent;
|
||
PInj. Pattern ::= UIdent [Pattern1];
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * Expressions
|
||
-------------------------------------------------------------------------------
|
||
|
||
internal EVar. Exp4 ::= LIdent;
|
||
EVarS. Exp4 ::= VarName ;
|
||
EInj. Exp4 ::= UIdent;
|
||
ELit. Exp4 ::= Lit;
|
||
EApp. Exp3 ::= Exp3 Exp4;
|
||
internal EAdd. Exp2 ::= Exp2 "+" Exp3;
|
||
ELet. Exp1 ::= "let" Bind "in" Exp1;
|
||
-- EAbsS. Exp1 ::= "\\" Pattern "." Exp1;
|
||
EAbs. Exp1 ::= "\\" LIdent "." Exp1;
|
||
ECase. Exp1 ::= "case" Exp "of" "{" [Branch] "}";
|
||
EAnn. Exp ::= Exp1 ":" Type;
|
||
|
||
VSymbol. VarName ::= "." Symbol;
|
||
VIdent. VarName ::= LIdent;
|
||
|
||
infixSymbol. Exp2 ::= Exp2 Symbol Exp3 ;
|
||
define infixSymbol e1 vn e3 = EApp (EApp (EVarS (VSymbol vn)) e1) e3;
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * LITERALS
|
||
-------------------------------------------------------------------------------
|
||
|
||
LInt. Lit ::= Integer;
|
||
LChar. Lit ::= Char;
|
||
LString. Lit ::= String ;
|
||
|
||
-------------------------------------------------------------------------------
|
||
-- * 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 3 ;
|
||
|
||
token UIdent (upper (letter | digit | '_')*) ;
|
||
token LIdent (lower (letter | digit | '_')*) ;
|
||
token Symbol (["@#%^&*_-+=|?/<>,•:[]"]+) ;
|
||
|
||
comment "--";
|
||
comment "{-" "-}";
|
||
|