-
Notifications
You must be signed in to change notification settings - Fork 0
/
parse.ml
414 lines (348 loc) · 9.5 KB
/
parse.ml
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
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
open Utils
open Lang
open Bark
open Bark.Syntax
(* === Parser specialization === *)
type problem =
| Expecting of string
type context =
string
type 'a parser =
(context, problem, 'a) Bark.parser
(* === Parser helpers === *)
let chainl1 : 'a 'b .
context -> 'a parser -> 'b parser -> ('a -> 'b -> 'a) parser -> 'a parser =
fun chain_context p_head p_arg op ->
let rec next acc =
one_of
[ in_context chain_context
( let* combiner =
op
in
p_arg |> and_then (combiner acc >> next)
)
; succeed acc
]
in
p_head |> and_then next
let chainr1 : 'a .
context -> 'a parser -> ('a -> 'a -> 'a) parser -> 'a parser =
fun chain_context p op ->
let rec rest acc =
one_of
[ in_context chain_context
( let* combiner =
op
in
map (combiner acc) (p |> and_then rest)
)
; succeed acc
]
in
p |> (and_then rest)
let ignore_with : 'a -> unit parser -> 'a parser =
fun x p ->
map (fun _ -> x) p
let make_token : string -> problem token =
fun tok ->
Token (tok, Expecting tok)
let space_symbol =
make_token " "
let spaces1 : unit parser =
succeed ()
|. symbol space_symbol
|. spaces
(* === Symbols and Keywords === *)
(* Paths and numbers *)
let val_keyword =
make_token "val"
let path_sep_symbol =
make_token "."
let len_keyword =
make_token "len"
let plus_symbol =
make_token "+"
(* Patterns *)
let left_keyword =
make_token "Left"
let right_keyword =
make_token "Right"
let prod_constrains_symbol =
make_token "~"
let nil_symbol =
make_token "[]"
let cons_symbol =
make_token "::"
(* Formulae *)
let false_keyword =
make_token "F"
let true_keyword =
make_token "T"
let match_keyword =
make_token "match"
let lparen_symbol =
make_token "("
let rparen_symbol =
make_token ")"
let leq_symbol =
make_token "<="
let or_symbol =
make_token "V"
(* Types *)
let void_symbol =
make_token "_|_"
let sum_symbol =
make_token "+"
let list_left_symbol =
make_token "["
let list_right_symbol =
make_token "]"
let prod_left_symbol =
make_token "<"
let prod_sep_symbol =
make_token ","
let prod_ascription_symbol =
make_token ":"
let prod_right_symbol =
make_token ">"
let refine_left_symbol =
make_token "{"
let refine_mid_symbol =
make_token "|"
let refine_right_symbol =
make_token "}"
(* === Parsing === *)
(* Paths *)
let inner_char : char -> bool =
fun c ->
Utils.lowercase_char c
|| Utils.uppercase_char c
|| Utils.digit_char c
|| Char.equal c '_'
let reserved_words =
String_set.of_list []
let variable_name : string parser =
variable
~start:Utils.lowercase_char
~inner:inner_char
~reserved:reserved_words
~expecting:(Expecting "variable name")
let path : path parser =
succeed (fun p -> p)
|= chainl1 "path"
( ignore_with Val (keyword val_keyword)
)
variable_name
( ignore_with (fun base ext -> Dot (base, ext))
( succeed ()
|. symbol path_sep_symbol
|. spaces
)
)
|. spaces
(* Numbers *)
let unscaled_length : path parser =
succeed (fun p -> p)
|. keyword len_keyword
|. spaces1
|= path
let scaled_length : (path * int) parser =
succeed (fun n p -> (p, n))
|= one_of
[ int (Expecting "scalar")
; succeed 1
]
|= unscaled_length
let number : number parser =
let linear : (path * int) list parser =
map List.rev @@
chainl1 "number"
( succeed (fun n -> [n])
|= scaled_length
)
scaled_length
( ignore_with (fun ns n -> n :: ns)
( succeed ()
|. symbol plus_symbol
|. spaces
)
)
in
let optionally_plus_linear : (path * int) list parser =
one_of
[ succeed (fun l -> l)
|. symbol plus_symbol
|. spaces
|= linear
; succeed []
]
in
one_of
[ succeed (fun n f -> f n)
|= int (Expecting "constant")
|= one_of
[ succeed (* clen p [+ linear] *)
(fun first_path linear n -> (0, (first_path, n) :: linear))
|= unscaled_length
|= optionally_plus_linear
; succeed (fun linear n -> (n, linear)) (* c [+ linear] *)
|. spaces
|= optionally_plus_linear
]
; succeed (fun l -> (0, l))
|= linear (* lenp + linear *)
]
(* Formulae *)
let rec pattern' : unit -> pattern parser = fun () ->
succeed (fun p -> p)
|= one_of
[ in_context "left pattern"
( succeed (fun phi -> MLeft phi)
|. keyword left_keyword
|. spaces1
|= lazily formula'
)
; in_context "right pattern"
( succeed (fun phi -> MRight phi)
|. keyword right_keyword
|. spaces1
|= lazily formula'
)
; in_context "product pattern"
( map (fun branches -> MTuple branches)
( sequence
~start:prod_left_symbol
~separator:prod_sep_symbol
~endd:prod_right_symbol
~spaces:spaces
~item:
( succeed (fun name r -> (name, r))
|= variable_name
|. spaces
|. symbol prod_constrains_symbol
|. spaces
|= lazily formula'
)
~trailing:Forbidden
)
)
; in_context "nil pattern"
( ignore_with MNil (symbol nil_symbol)
)
; in_context "cons pattern"
( succeed (fun phi phis -> MCons(phi, phis))
|= lazily formula'
|. spaces
|. symbol cons_symbol
|. spaces
|= lazily formula'
)
]
|. spaces
and atom' : unit -> formula parser = fun () ->
succeed (fun a -> a)
|= one_of
[ in_context "false formula"
( ignore_with False (keyword false_keyword)
)
; in_context "true formula"
( ignore_with True (keyword true_keyword)
)
; in_context "leq formula"
( succeed (fun n1 n2 -> LEq (n1, n2))
|= number
|. spaces
|. symbol leq_symbol
|. spaces
|= number
)
; in_context "match formula"
( succeed (fun p -> Match p)
|. keyword match_keyword
|. spaces
|. symbol lparen_symbol
|= lazily pattern'
|. symbol rparen_symbol
)
]
|. spaces
and disjunction_clause' : unit -> formula parser = fun () ->
chainr1 "disjunction" (lazily atom')
( ignore_with (fun phi1 phi2 -> Or (phi1, phi2))
( succeed ()
|. symbol or_symbol
|. spaces
)
)
and formula' : unit -> formula parser = fun () ->
lazily disjunction_clause'
let formula : formula parser =
lazily formula'
(* Refinement types *)
let rec refine_atom' : unit -> refine parser = fun () ->
succeed (fun a -> a)
|= one_of
[ in_context "void type"
( ignore_with RVoid (symbol void_symbol)
)
; in_context "list type"
( succeed (fun inner -> RLst inner)
|. symbol list_left_symbol
|. spaces
|= lazily refine'
|. symbol list_right_symbol
)
; in_context "refinement"
( succeed (fun r phi -> Refine (r, phi))
|. symbol refine_left_symbol
|. spaces
|= lazily refine'
|. symbol refine_mid_symbol
|. spaces
|= formula
|. symbol refine_right_symbol
)
; in_context "product type"
( map (fun ts -> RProd ts)
( sequence
~start:prod_left_symbol
~separator:prod_sep_symbol
~endd:prod_right_symbol
~spaces:spaces
~item:
( succeed (fun name r -> (name, r))
|= variable_name
|. spaces
|. symbol prod_ascription_symbol
|. spaces
|= lazily refine'
)
~trailing:Forbidden
)
)
]
|. spaces
and refine_sum' : unit -> refine parser = fun () ->
chainr1 "sum type" (lazily refine_atom')
( ignore_with (fun r1 r2 -> RSum (r1, r2))
( succeed ()
|. symbol sum_symbol
|. spaces
)
)
and refine' : unit -> refine parser = fun () ->
lazily refine_sum'
let refine : refine parser =
lazily refine'
let parse parser s =
match Bark.run parser s with
| Ok r -> Ok r
| Error dead_ends ->
let show_dead_end dead_end =
match dead_end.Bark.problem with
| Expecting s -> "'" ^ s ^ "'" in
let msg = dead_ends
|> List.map show_dead_end
|> String.concat " | "
|> (^) "Expecting " in
Error msg