summaryrefslogtreecommitdiff
path: root/src/Transfer/Syntax/Syntax.cf
blob: 54866508b4baf1d5ea55f4d12310a64b67490f61 (plain)
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
entrypoints Module, Exp ;

layout "let", "where", "of" ;
layout stop "in" ;
layout toplevel ;

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

Module. Module ::= [Import] [Decl] ;

Import. Import ::= "import" Ident ;
separator Import ";" ;

DataDecl.  Decl ::= "data" Ident ":" Exp "where" "{" [ConsDecl] "}" ;
TypeDecl.  Decl ::= Ident ":" Exp ;
ValueDecl. Decl ::= Ident [Pattern] "=" Exp ;
DeriveDecl. Decl ::= "derive" Ident Ident ;
separator Decl ";" ;

ConsDecl. ConsDecl ::= Ident ":" Exp ;
separator ConsDecl ";" ;

-- Hack: constructor applied to at least one pattern
-- this is to separate it from variable patterns
PConsTop. Pattern ::= Ident Pattern1 [Pattern] ;
_.        Pattern ::= Pattern1 ;
-- Constructor pattern with parantheses
PCons.    Pattern1 ::= "(" Ident [Pattern] ")" ;
-- Record patterns
PRec.     Pattern1 ::= "{" [FieldPattern] "}";
-- The pattern matching the Type constant
PType.    Pattern1 ::= "Type" ;
-- String literal patterns
PStr.     Pattern1 ::= String ;
-- Integer literal patterns
PInt.     Pattern1 ::= Integer ;
-- Variable patterns
PVar.     Pattern1 ::= Ident ;
-- Wild card patterns
PWild.    Pattern1 ::= "_" ;

[].  [Pattern] ::= ;
(:). [Pattern] ::= Pattern1 [Pattern] ;

FieldPattern. FieldPattern ::= Ident "=" Pattern ;
separator FieldPattern ";" ;

ELet.      Exp  ::= "let" "{" [LetDef] "}" "in" Exp ;
LetDef.    LetDef ::= Ident ":" Exp "=" Exp ;
separator LetDef ";" ;

ECase.     Exp  ::= "case" Exp "of" "{" [Case] "}" ;
Case. Case ::= Pattern "->" Exp ;
separator Case ";" ;

EIf.       Exp  ::= "if" Exp "then" Exp "else" Exp ;

EAbs.      Exp2 ::= "\\" VarOrWild "->" Exp ;
EPi.       Exp2 ::= "(" VarOrWild ":" Exp ")" "->" Exp ;
EPiNoVar.  Exp2 ::= Exp3 "->" Exp ;
VVar.      VarOrWild ::= Ident ;
VWild.     VarOrWild ::= "_" ;

EOr.       Exp3 ::= Exp4 "||" Exp3 ;
EAnd.      Exp4 ::= Exp5 "&&" Exp4 ;

EEq.       Exp5 ::= Exp6 "==" Exp6 ;
ENe.       Exp5 ::= Exp6 "/=" Exp6 ;
ELt.       Exp5 ::= Exp6 "<"  Exp6 ;
ELe.       Exp5 ::= Exp6 "<=" Exp6 ;
EGt.       Exp5 ::= Exp6 ">"  Exp6 ;
EGe.       Exp5 ::= Exp6 ">=" Exp6 ;

EAdd.      Exp6 ::= Exp6 "+" Exp7 ;
ESub.      Exp6 ::= Exp6 "-" Exp7 ;

EMul.      Exp7 ::= Exp7 "*" Exp8 ;
EDiv.      Exp7 ::= Exp7 "/" Exp8 ;
EMod.      Exp7 ::= Exp7 "%" Exp8 ;

ENeg.      Exp8 ::= "-" Exp8 ;

EApp.      Exp9 ::= Exp9 Exp10 ;

EProj.     Exp10 ::= Exp10 "." Ident ;

EEmptyRec. Exp11 ::= "{" "}" ;

ERecType.  Exp11 ::= "{" [FieldType] "}" ;
FieldType. FieldType  ::= Ident ":" Exp ;
separator nonempty FieldType ";" ;

ERec.      Exp11 ::= "{" [FieldValue] "}" ;
FieldValue.FieldValue ::= Ident "=" Exp ;
separator nonempty FieldValue ";" ;

EVar.      Exp11 ::= Ident ;
EType.     Exp11 ::= "Type" ;
EStr.      Exp11 ::= String ;
EInt.      Exp11 ::= Integer ;

coercions Exp 11 ;