forked from bachelor-group-66-systemf/churf
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Grammar.cf
113 lines (85 loc) · 3.55 KB
/
Grammar.cf
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
-------------------------------------------------------------------------------
-- * 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 "{-" "-}";