/
source.fstar.js
267 lines (266 loc) · 9.42 KB
/
source.fstar.js
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
// This is a TextMate grammar distributed by `starry-night`.
// This grammar is developed at
// <https://github.com/FStarLang/atom-fstar>
// and licensed `apache-2.0`.
// See <https://github.com/wooorm/starry-night> for more info.
/** @type {import('../lib/index.js').Grammar} */
const grammar = {
extensions: ['.fst', '.fsti'],
names: ['f*', 'fstar'],
patterns: [
{include: '#comments'},
{include: '#modules'},
{include: '#options'},
{include: '#expr'}
],
repository: {
commentblock: {
patterns: [
{
begin: '\\(\\*',
beginCaptures: {
0: {name: 'punctuation.definition.comment.begin.fstar'}
},
end: '\\*\\)',
endCaptures: {0: {name: 'punctuation.definition.comment.end.fstar'}},
name: 'comment.block.fstar',
patterns: [{include: '#commentblock'}]
}
]
},
comments: {
patterns: [
{match: '//.*', name: 'comment.line.fstar'},
{include: '#commentblock'}
]
},
expr: {
patterns: [
{include: '#comments'},
{match: "'[a-zA-Z0-9_]+\\b", name: 'variable.other.generic-type.fstar'},
{include: '#strings'},
{
match: '\\b(int|nat|pos|bool|unit|string|Type|Type0|eqtype)\\b',
name: 'support.class.base.fstar'
},
{
match:
'(/\\\\|\\\\/|<:|<@|[(][|]|[|][)]|u#|`|~>|->|<--|<-|<==>|==>|[?][.]|[.]\\[|[.]\\(|[{][:]pattern|::|:=|;;|[!][{]|\\[[|]|[|]>|[|]\\]|[~+^&?$|#,.:;=\\[\\](){}-])',
name: 'support.class.base.fstar'
},
{
match:
'\\b(Pure|PURE|Tot|STATE|ST|St|Stack|StackInline|HST|ALL|All|EXN|Exn|Ex|DIV|Div|GHOST|Ghost|GTot|Lemma)\\b',
name: 'constant.language.monad.fstar'
},
{
match: '\\b(_|[(]\\s*[)]|\\[\\s*\\])\\b',
name: 'constant.language.fstar'
},
{
match:
'\\b(let|in|type|kind|val|rec|and|if|then|else|assume|admit|assert|assert_norm|squash|failwith|SMTPat|SMTPatOr|hasEq|fun|function|forall|exists|exception|by|new_effect|reify|try|synth|with|when)\\b',
name: 'keyword.other.fstar'
},
{
match:
'\\b(abstract|attributes|noeq|unopteq|inline|inline_for_extraction|irreducible|logic|mutable|new|noextract|private|reifiable|reflectable|total|unfold|unfoldable)\\b',
name: 'storage.modifier.fstar'
},
{
match: '\\b([tT]rue|[fF]alse)\\b',
name: 'constant.language.boolean.fstar'
},
{
match: '\\b0[xX][0-9a-fA-F]+[uU]?[zyslL]?\\b',
name: 'constant.numeric.hex.js'
},
{
match: '\\b[0-9]+[uU]?[zyslL]?\\b',
name: 'constant.numeric.decimal.js'
},
{
captures: {
0: {name: 'constant.numeric.decimal.fstar'},
1: {name: 'meta.delimiter.decimal.period.fstar'},
2: {name: 'meta.delimiter.decimal.period.fstar'},
3: {name: 'meta.delimiter.decimal.period.fstar'},
4: {name: 'meta.delimiter.decimal.period.fstar'},
5: {name: 'meta.delimiter.decimal.period.fstar'},
6: {name: 'meta.delimiter.decimal.period.fstar'}
},
match:
'(?x)\n(?:\n (?:\\b[0-9]+(\\.)[0-9]+[eE][+-]?[0-9]+\\b)| # 1.1E+3\n (?:\\b[0-9]+(\\.)[eE][+-]?[0-9]+\\b)| # 1.E+3\n (?:\\B(\\.)[0-9]+[eE][+-]?[0-9]+\\b)| # .1E+3\n (?:\\b[0-9]+[eE][+-]?[0-9]+\\b)| # 1E+3\n (?:\\b[0-9]+(\\.)[0-9]+\\b)| # 1.1\n (?:\\b[0-9]+(\\.)\\B)| # 1.\n (?:\\B(\\.)[0-9]+\\b)| # .1\n (?:\\b[0-9]+\\b(?!\\.)) # 1\n)[L]?[fF]?'
},
{
begin: '([(])\\s*(requires|ensures|decreases)?',
beginCaptures: {
1: {name: 'punctuation.definition.scope.begin.bracket.round.fstar'},
2: {name: 'keyword.other.fstar'}
},
end: '([)])',
endCaptures: {
1: {name: 'punctuation.definition.scope.end.bracket.round.fstar'}
},
patterns: [{include: '#expr'}]
},
{
begin: '([(])',
beginCaptures: {
1: {name: 'punctuation.definition.clause.begin.bracket.round.fstar'}
},
end: '([)])',
endCaptures: {
1: {name: 'punctuation.definition.clause.end.bracket.round.fstar'}
},
patterns: [{include: '#expr'}]
},
{
begin: '([%]\\[)',
beginCaptures: {1: {name: 'constant.language.termorder.begin.fstar'}},
end: '(\\])',
endCaptures: {1: {name: 'constant.language.termorder.end.fstar'}},
patterns: [{include: '#expr'}]
},
{
begin: '(\\[[@])',
beginCaptures: {1: {name: 'storage.modifier.attributes.begin.fstar'}},
end: '(\\])',
endCaptures: {1: {name: 'storage.modifier.attributes.end.fstar'}},
patterns: [{include: '#expr'}]
},
{
begin: '\\b(match)\\b',
beginCaptures: {1: {name: 'keyword.control.match.fstar'}},
end: '\\b(with)\\b',
endCaptures: {1: {name: 'keyword.control.with.fstar'}},
patterns: [{include: '#expr'}]
},
{
begin: '\\b(begin)\\b',
beginCaptures: {1: {name: 'keyword.control.begin.fstar'}},
end: '\\b(end)\\b',
endCaptures: {1: {name: 'keyword.control.end.fstar'}},
patterns: [{include: '#expr'}]
},
{
captures: {1: {name: 'support.function.constructor.fstar'}},
match:
"\\b([\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)\\b(?!\\s*[.])"
},
{
captures: {1: {name: 'variable.other.module.fstar'}},
match:
"\\b((?:[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*[.])+)"
},
{
captures: {1: {name: 'entity.name.function.fstar'}},
match: "\\b([\\p{Ll}_][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)"
}
]
},
modules: {
patterns: [
{
begin:
"\\b(module)\\s+([\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)\\s*(=)",
beginCaptures: {
1: {name: 'keyword.control.module.fstar'},
2: {name: 'variable.other.module-alias.fstar'},
3: {name: 'keyword.operator.assignment.fstar'}
},
end: "\\b((?<name>[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)(?:[.]\\g<name>)*)\\b",
endCaptures: {1: {name: 'variable.other.module.fstar'}}
},
{
begin: '\\b(module|open|include)\\b',
beginCaptures: {1: {name: 'keyword.control.module.fstar'}},
end: "\\b((?<name>[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)(?:[.]\\g<name>)*)\\b",
endCaptures: {1: {name: 'variable.other.module.fstar'}}
}
]
},
op_names: {
patterns: [
{
match:
'\\bop(?:_(?:Multiply|Star|Slash|Percent|Plus|Substraction|Equals|Less|Greater|Bang|Dollar|Amp|Dot|Hat|Colon|Pipe|Question))+\\b',
name: 'entity.name.tag.fstar'
}
]
},
options: {
patterns: [
{
captures: {
1: {name: 'keyword.control.setoption.fstar'},
2: {name: 'punctuation.definition.options.begin.fstar'},
3: {name: 'string.quoted.double.fstar'},
4: {name: 'punctuation.definition.options.end.fstar'}
},
match: '(#(?:re)?set-options)\\s*(["])((?:[^"]|\\\\")*)(["])'
}
]
},
string_escapes: {
patterns: [
{
match: '\\\\u(?![A-Fa-f0-9]{4}|{[A-Fa-f0-9]+})[^\'"]*',
name: 'invalid.illegal.unicode-escape.fstar'
},
{
captures: {
1: {
name: 'punctuation.definition.unicode-escape.begin.bracket.curly.fstar'
},
2: {
patterns: [
{
match: '[A-Fa-f\\d]{7,}|(?!10)[A-Fa-f\\d]{6}',
name: 'invalid.illegal.unicode-escape.fstar'
}
]
},
3: {
name: 'punctuation.definition.unicode-escape.end.bracket.curly.fstar'
}
},
match: '\\\\u(?:[A-Fa-f0-9]{4}|({)([A-Fa-f0-9]+)(}))',
name: 'constant.character.escape.js'
},
{
match:
'\\\\(x[0-9A-Fa-f]{2}|[0-2][0-7]{0,2}|3[0-6][0-7]?|37[0-7]?|[4-7][0-7]?|.)',
name: 'constant.character.escape.fstar'
}
]
},
strings: {
patterns: [
{
begin: '"',
beginCaptures: {
0: {name: 'punctuation.definition.string.begin.fstar'}
},
end: '"',
endCaptures: {0: {name: 'punctuation.definition.string.end.fstar'}},
name: 'string.quoted.double.fstar',
patterns: [{include: '#string_escapes'}]
},
{
begin: "'",
beginCaptures: {0: {name: 'punctuation.definition.char.begin.fstar'}},
end: "'",
endCaptures: {0: {name: 'punctuation.definition.char.end.fstar'}},
name: 'string.quoted.single.fstar',
patterns: [
{include: '#string_escapes'},
{match: '.{2,}', name: 'invalid.illegal.string.js'}
]
}
]
}
},
scopeName: 'source.fstar'
}
export default grammar