regex.bend
bend-kit-regex@0.8.0.0 · 2,352 lines · 316 definitions
1
2import Base
3import bend-kit-unicode@0.1.0.0/unicode.bend as U
4import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
5
6
7
8
9
10
11
12
13type Item is Data:
14 Rng{lo: U32, hi: U32}
15 Prop{neg: Bool, name: String}
16
17
18type Node is Data:
19 NEmpty{}
20 NSet{neg: Bool, items: List<&2, Item>}
21 NAssert{k: U32}
22 NCat{a: Node, b: Node}
23 NAlt{a: Node, b: Node}
24 NPlus{greedy: Bool, a: Node}
25 NQuest{greedy: Bool, a: Node}
26 NGroup{i: U32, a: Node}
27
28type Tok is Data:
29 TAtom{n: Node}
30 TOpen{cap: Bool}
31 TClose{}
32 TBar{}
33 TRep{min: U32, max: Maybe<&2, U32>, greedy: Bool}
34
35def lit(+c: U32) -> Node:
36 NSet{False{}, [Rng{c, c}]}
37
38def is_digit(+c: U32) -> Bool:
39 U32.is_le(48, c) && U32.is_le(c, 57)
40
41def is_word(+c: U32) -> Bool:
42 is_digit(c) || (U32.is_le(65, c) && U32.is_le(c, 90)) || (U32.is_le(97, c) && U32.is_le(c, 122)) || U32.is_eq(c, 95)
43
44def is_alnum(+c: U32) -> Bool:
45 Bool.and(is_word(c), U32.is_ne(c, 95))
46
47
48def perl.d() -> List<&2, Item>:
49 [Rng{48, 57}]
50
51def perl.D() -> List<&2, Item>:
52 [Rng{0, 47}, Rng{58, 1114111}]
53
54def perl.w() -> List<&2, Item>:
55 [Rng{48, 57}, Rng{65, 90}, Rng{95, 95}, Rng{97, 122}]
56
57def perl.W() -> List<&2, Item>:
58 [Rng{0, 47}, Rng{58, 64}, Rng{91, 94}, Rng{96, 96}, Rng{123, 1114111}]
59
60def perl.s() -> List<&2, Item>:
61 [Rng{9, 10}, Rng{12, 13}, Rng{32, 32}]
62
63def perl.S() -> List<&2, Item>:
64 [Rng{0, 8}, Rng{11, 11}, Rng{14, 31}, Rng{33, 1114111}]
65
66def cats() -> List<&2, String>:
67 ["L", "Lu", "Ll", "Lt", "Lm", "Lo", "M", "Mn", "Mc", "Me", "N", "Nd", "Nl", "No",
68 "P", "Pc", "Pd", "Ps", "Pe", "Pi", "Pf", "Po", "S", "Sm", "Sc", "Sk", "So",
69 "Z", "Zs", "Zl", "Zp", "C", "Cc", "Cf", "Cs", "Co", "Cn"]
70
71
72
73
74type Esc is Data:
75 EPoint{c: U32, rest: String}
76 EItems{items: List<&2, Item>, rest: String}
77 EAssert{k: U32, rest: String}
78 EBad{}
79
80def prop.if(ok: Bool, neg: Bool, name: String, t: String) -> Esc:
81 match ok:
82 case True{}:
83 EItems{[Prop{neg, name}], t}
84 case False{}:
85 EBad{}
86
87def prop.ok(neg: Bool, +name: String, t: String) -> Esc:
88 prop.if(List.contains(~String, ~String.eq, cats(), name), neg, name, t)
89
90def prop.name(s: String, neg: Bool, acc: String) -> Esc:
91 match s:
92 case SNil{}:
93 EBad{}
94 case SCon{'}', t}:
95 prop.ok(neg, String.reverse(acc), t)
96 case SCon{c, t}:
97 prop.name(t, neg, SCon{c, acc})
98
99
100def prop(neg: Bool, s: String) -> Esc:
101 match s:
102 case SNil{}:
103 EBad{}
104 case SCon{'{', t}:
105 prop.name(t, neg, SNil{})
106 case SCon{c, t}:
107 prop.ok(neg, SCon{c, SNil{}}, t)
108
109
110def esc.other(alnum: Bool, +c: U32, t: String) -> Esc:
111 match alnum:
112 case True{}:
113 EBad{}
114 case False{}:
115 EPoint{c, t}
116
117
118def esc(s: String) -> Esc:
119 match s:
120 case SNil{}:
121 EBad{}
122 case SCon{'d', t}:
123 EItems{perl.d(), t}
124 case SCon{'D', t}:
125 EItems{perl.D(), t}
126 case SCon{'w', t}:
127 EItems{perl.w(), t}
128 case SCon{'W', t}:
129 EItems{perl.W(), t}
130 case SCon{'s', t}:
131 EItems{perl.s(), t}
132 case SCon{'S', t}:
133 EItems{perl.S(), t}
134 case SCon{'p', t}:
135 prop(False{}, t)
136 case SCon{'P', t}:
137 prop(True{}, t)
138 case SCon{'A', t}:
139 EAssert{0, t}
140 case SCon{'z', t}:
141 EAssert{1, t}
142 case SCon{'b', t}:
143 EAssert{2, t}
144 case SCon{'B', t}:
145 EAssert{3, t}
146 case SCon{'n', t}:
147 EPoint{10, t}
148 case SCon{'t', t}:
149 EPoint{9, t}
150 case SCon{'r', t}:
151 EPoint{13, t}
152 case SCon{'f', t}:
153 EPoint{12, t}
154 case SCon{'v', t}:
155 EPoint{11, t}
156 case SCon{Chr{+c}, t}:
157 esc.other(is_alnum(c), c, t)
158
159
160
161
162type Cs is Data:
163 CsGo{s: String, first: Bool, items: List<&2, Item>}
164 CsDone{items: List<&2, Item>, rest: String}
165 CsFail{}
166
167def class.range(ok: Bool, +c: U32, +d: U32, u: String, items: List<&2, Item>) -> Cs:
168 match ok:
169 case True{}:
170 CsGo{u, False{}, Rng{c, d} <> items}
171 case False{}:
172 CsFail{}
173
174def class.hi(e: Esc, +c: U32, items: List<&2, Item>) -> Cs:
175 match e:
176 case EPoint{+d, u}:
177 class.range(U32.is_le(c, d), c, d, u, items)
178 case EItems{xs, u}:
179 CsFail{}
180 case EAssert{k, u}:
181 CsFail{}
182 case EBad{}:
183 CsFail{}
184
185
186def class.lo(+c: U32, t: String, items: List<&2, Item>) -> Cs:
187 match t:
188 case SCon{'-', SCon{']', u}}:
189 CsDone{Rng{45, 45} <> Rng{c, c} <> items, u}
190 case SCon{'-', SCon{'\\', u}}:
191 class.hi(esc(u), c, items)
192 case SCon{'-', SCon{Chr{+d}, u}}:
193 class.range(U32.is_le(c, d), c, d, u, items)
194 case _:
195 CsGo{t, False{}, Rng{c, c} <> items}
196
197def class.esc(e: Esc, items: List<&2, Item>) -> Cs:
198 match e:
199 case EPoint{+c, t}:
200 class.lo(c, t, items)
201 case EItems{xs, t}:
202 CsGo{t, False{}, List.append(&2, Item, xs, items)}
203 case EAssert{k, t}:
204 CsFail{}
205 case EBad{}:
206 CsFail{}
207
208
209def class.step(s: String, first: Bool, items: List<&2, Item>) -> Cs:
210 match s:
211 case SNil{}:
212 CsFail{}
213 case SCon{']', t}:
214 match first:
215 case True{}:
216 class.lo(93, t, items)
217 case False{}:
218 CsDone{items, t}
219 case SCon{'\\', t}:
220 class.esc(esc(t), items)
221 case SCon{Chr{+c}, t}:
222 class.lo(c, t, items)
223
224
225def class.run(fuel: Nat, st: Cs) -> Cs:
226 match fuel:
227 case 0n:
228 CsFail{}
229 case 1n+f:
230 match st:
231 case CsGo{s, first, items}:
232 class.run(f, class.step(s, first, items))
233 case CsDone{items, rest}:
234 CsDone{items, rest}
235 case CsFail{}:
236 CsFail{}
237
238def class(+s: String, first: Bool) -> Cs:
239 class.run(Nat.add(String.length(s), 1n), CsGo{s, first, Nil{}})
240
241
242
243
244type Lx is Data:
245 LGo{s: String, toks: List<&2, Tok>}
246 LDone{toks: List<&2, Tok>}
247 LFail{}
248
249
250type Num is Data:
251 Num{v: U32, n: U32, rest: String}
252
253def num.add(+acc: U32, +c: U32) -> U32:
254 Bool.pick(U32, U32.is_lt(acc, 100000), (acc * 10 + (c - 48) : U32), 100000)
255
256def num.go(t: String, +c: U32, +acc: U32, +n: U32, dig: Bool) -> Num:
257 match t:
258 case SNil{}:
259 match dig:
260 case True{}:
261 Num{num.add(acc, c), (n + 1 : U32), SNil{}}
262 case False{}:
263 Num{acc, n, SCon{Chr{c}, SNil{}}}
264 case SCon{Chr{+d}, u}:
265 match dig:
266 case True{}:
267 num.go(u, d, num.add(acc, c), (n + 1 : U32), is_digit(d))
268 case False{}:
269 Num{acc, n, SCon{Chr{c}, SCon{Chr{d}, u}}}
270
271def num(s: String) -> Num:
272 match s:
273 case SNil{}:
274 Num{0, 0, SNil{}}
275 case SCon{Chr{+c}, t}:
276 num.go(t, c, 0, 0, is_digit(c))
277
278
279def lex.rep(+min: U32, max: Maybe<&2, U32>, t: String, toks: List<&2, Tok>) -> Lx:
280 match t:
281 case SCon{'?', u}:
282 LGo{u, TRep{min, max, False{}} <> toks}
283 case _:
284 LGo{t, TRep{min, max, True{}} <> toks}
285
286def Num.n(m: Num) -> U32:
287 Num{v, n, r} = m
288 n
289
290
291def lex.brace.max(none: Bool, +min: U32, m: Num, orig: String, toks: List<&2, Tok>) -> Lx:
292 match none:
293 case True{}:
294 LGo{orig, TAtom{lit(123)} <> toks}
295 case False{}:
296 Num{+v, n, r} = m
297 match r:
298 case SCon{'}', u}:
299 lex.rep(min, Some{v}, u, toks)
300 case _:
301 LGo{orig, TAtom{lit(123)} <> toks}
302
303def lex.brace.min(none: Bool, m: Num, +orig: String, toks: List<&2, Tok>) -> Lx:
304 match none:
305 case True{}:
306 LGo{orig, TAtom{lit(123)} <> toks}
307 case False{}:
308 Num{+v, n, r} = m
309 match r:
310 case SCon{'}', u}:
311 lex.rep(v, Some{v}, u, toks)
312 case SCon{',', SCon{'}', u}}:
313 lex.rep(v, None{}, u, toks)
314 case SCon{',', u}:
315 +m2 = num(u)
316 lex.brace.max(U32.is_eq(Num.n(m2), 0), v, m2, orig, toks)
317 case _:
318 LGo{orig, TAtom{lit(123)} <> toks}
319
320def lex.class(neg: Bool, r: Cs, toks: List<&2, Tok>) -> Lx:
321 match r:
322 case CsDone{items, rest}:
323 LGo{rest, TAtom{NSet{neg, items}} <> toks}
324 case CsGo{s, first, items}:
325 LFail{}
326 case CsFail{}:
327 LFail{}
328
329def lex.esc(e: Esc, toks: List<&2, Tok>) -> Lx:
330 match e:
331 case EPoint{c, t}:
332 LGo{t, TAtom{lit(c)} <> toks}
333 case EItems{xs, t}:
334 LGo{t, TAtom{NSet{False{}, xs}} <> toks}
335 case EAssert{k, t}:
336 LGo{t, TAtom{NAssert{k}} <> toks}
337 case EBad{}:
338 LFail{}
339
340def lex.step(s: String, toks: List<&2, Tok>) -> Lx:
341 match s:
342 case SNil{}:
343 LDone{toks}
344 case SCon{'\\', t}:
345 lex.esc(esc(t), toks)
346 case SCon{'[', SCon{'^', t}}:
347 lex.class(True{}, class(t, True{}), toks)
348 case SCon{'[', t}:
349 lex.class(False{}, class(t, True{}), toks)
350 case SCon{'(', SCon{'?', SCon{':', t}}}:
351 LGo{t, TOpen{False{}} <> toks}
352 case SCon{'(', SCon{'?', t}}:
353 LFail{}
354 case SCon{'(', t}:
355 LGo{t, TOpen{True{}} <> toks}
356 case SCon{')', t}:
357 LGo{t, TClose{} <> toks}
358 case SCon{'|', t}:
359 LGo{t, TBar{} <> toks}
360 case SCon{'*', t}:
361 lex.rep(0, None{}, t, toks)
362 case SCon{'+', t}:
363 lex.rep(1, None{}, t, toks)
364 case SCon{'?', t}:
365 lex.rep(0, Some{1}, t, toks)
366 case SCon{'{', +t}:
367 +m = num(t)
368 lex.brace.min(U32.is_eq(Num.n(m), 0), m, t, toks)
369 case SCon{'.', t}:
370 LGo{t, TAtom{NSet{True{}, [Rng{10, 10}]}} <> toks}
371 case SCon{'^', t}:
372 LGo{t, TAtom{NAssert{0}} <> toks}
373 case SCon{'$', t}:
374 LGo{t, TAtom{NAssert{1}} <> toks}
375 case SCon{Chr{+c}, t}:
376 LGo{t, TAtom{lit(c)} <> toks}
377
378
379def lex(fuel: Nat, st: Lx) -> Maybe<&2, List<&2, Tok>>:
380 match fuel:
381 case 0n:
382 None{}
383 case 1n+f:
384 match st:
385 case LGo{s, toks}:
386 lex(f, lex.step(s, toks))
387 case LDone{toks}:
388 Some{List.reverse(&2, Tok, toks)}
389 case LFail{}:
390 None{}
391
392
393
394
395
396type Frame is Data:
397 Frame{cap: Maybe<&2, U32>, alts: List<&2, Node>, cur: List<&2, Node>}
398
399
400type Ps is Data:
401 Ps{n: U32, rep: Bool, stack: List<&2, Frame>, alts: List<&2, Node>, cur: List<&2, Node>}
402 PsFail{}
403def cat(a: Node, b: Node) -> Node:
404 match a:
405 case NEmpty{}:
406 b
407 case _:
408 match b:
409 case NEmpty{}:
410 a
411 case _:
412 NCat{a, b}
413
414def seq.go(xs: List<&2, Node>, acc: Node) -> Node:
415 match xs:
416 case Nil{}:
417 acc
418 case Con{h, t}:
419 seq.go(t, cat(h, acc))
420
421def seq(xs: List<&2, Node>) -> Node:
422 seq.go(xs, NEmpty{})
423
424def alt.go(xs: List<&2, Node>, acc: Node) -> Node:
425 match xs:
426 case Nil{}:
427 acc
428 case Con{h, t}:
429 alt.go(t, NAlt{h, acc})
430
431def group(cap: Maybe<&2, U32>, a: Node) -> Node:
432 match cap:
433 case None{}:
434 a
435 case Some{i}:
436 NGroup{i, a}
437
438def rep.copies(k: Nat, +h: Node, acc: Node) -> Node:
439 match k:
440 case 0n:
441 acc
442 case 1n+p:
443 rep.copies(p, h, cat(h, acc))
444
445def rep.opt(k: Nat, +g: Bool, +h: Node) -> Node:
446 match k:
447 case 0n:
448 NEmpty{}
449 case 1n+p:
450 NQuest{g, cat(h, rep.opt(p, g, h))}
451
452
453def rep.inf(k: Nat, +g: Bool, +h: Node) -> Node:
454 match k:
455 case 0n:
456 NQuest{g, NPlus{g, h}}
457 case 1n+p:
458 rep.copies(p, h, NPlus{g, h})
459
460def rep.fin(max: Maybe<&2, U32>, +min: U32, +g: Bool, +h: Node) -> Node:
461 match max:
462 case None{}:
463 rep.inf(U32.to_nat(min), g, h)
464 case Some{m}:
465 rep.copies(U32.to_nat(min), h, rep.opt(U32.to_nat((m - min : U32)), g, h))
466
467def rep(+h: Node, +min: U32, max: Maybe<&2, U32>, +g: Bool) -> Node:
468 rep.fin(max, min, g, h)
469
470
471def rep.ok(+min: U32, max: Maybe<&2, U32>) -> Bool:
472 match max:
473 case None{}:
474 U32.is_le(min, 1000)
475 case Some{+m}:
476 U32.is_le(m, 1000) && U32.is_le(min, m)
477
478def parse.rep(ok: Bool, cur: List<&2, Node>, +min: U32, max: Maybe<&2, U32>, +g: Bool, +n: U32, stack: List<&2, Frame>, alts: List<&2, Node>) -> Ps:
479 match ok:
480 case False{}:
481 PsFail{}
482 case True{}:
483 match cur:
484 case Nil{}:
485 PsFail{}
486 case Con{h, t}:
487 Ps{n, True{}, stack, alts, rep(h, min, max, g) <> t}
488
489def parse.open(cap: Bool, +n: U32, stack: List<&2, Frame>, alts: List<&2, Node>, cur: List<&2, Node>) -> Ps:
490 match cap:
491 case True{}:
492 Ps{(n + 1 : U32), False{}, Frame{Some{n}, alts, cur} <> stack, Nil{}, Nil{}}
493 case False{}:
494 Ps{n, False{}, Frame{None{}, alts, cur} <> stack, Nil{}, Nil{}}
495
496def parse.close(stack: List<&2, Frame>, +n: U32, alts: List<&2, Node>, cur: List<&2, Node>) -> Ps:
497 match stack:
498 case Nil{}:
499 PsFail{}
500 case Con{Frame{cap, fa, fc}, up}:
501 Ps{n, False{}, up, fa, group(cap, alt.go(alts, seq(cur))) <> fc}
502
503def parse.tok(tok: Tok, +n: U32, rep: Bool, stack: List<&2, Frame>, alts: List<&2, Node>, cur: List<&2, Node>) -> Ps:
504 match tok:
505 case TAtom{a}:
506 Ps{n, False{}, stack, alts, a <> cur}
507 case TRep{+min, +max, g}:
508 parse.rep(Bool.and(Bool.not(rep), rep.ok(min, max)), cur, min, max, g, n, stack, alts)
509 case TOpen{cap}:
510 parse.open(cap, n, stack, alts, cur)
511 case TClose{}:
512 parse.close(stack, n, alts, cur)
513 case TBar{}:
514 Ps{n, False{}, stack, seq(cur) <> alts, Nil{}}
515
516def parse.step(st: Ps, tok: Tok) -> Ps:
517 match st:
518 case PsFail{}:
519 PsFail{}
520 case Ps{n, rep, stack, alts, cur}:
521 parse.tok(tok, n, rep, stack, alts, cur)
522
523def parse(toks: List<&2, Tok>, st: Ps) -> Ps:
524 match toks:
525 case Nil{}:
526 st
527 case Con{tok, t}:
528 parse(t, parse.step(st, tok))
529
530
531
532
533type Inst is Data:
534 ISet{neg: Bool, items: List<&2, Item>}
535 IAssert{k: U32}
536 ISplit{x: U32, y: U32}
537 IJmp{x: U32}
538 ISave{k: U32}
539 IMatch{}
540
541
542def required.right(b: Maybe<&2, U32>, a: Maybe<&2, U32>) -> Maybe<&2, U32>:
543 match b:
544 case Some{c}:
545 Some{c}
546 case None{}:
547 a
548
549def required(n: Node) -> Maybe<&2, U32>:
550 match n:
551 case NEmpty{}:
552 None{}
553 case NSet{False{}, Con{Rng{+lo, +hi}, Nil{}}}:
554 Bool.pick(Maybe<&2, U32>, U32.is_eq(lo, hi) && U32.is_lt(lo, 128), Some{lo}, None{})
555 case NSet{neg, items}:
556 None{}
557 case NAssert{k}:
558 None{}
559 case NCat{a, b}:
560 required.right(required(b), required(a))
561 case NAlt{a, b}:
562 None{}
563 case NPlus{g, a}:
564 required(a)
565 case NQuest{g, a}:
566 None{}
567 case NGroup{i, a}:
568 required(a)
569
570def required.join(right: Maybe<&2, Node>, left: Maybe<&2, Node>, a: Node) -> Maybe<&2, Node>:
571 match right:
572 case Some{r}:
573 Some{NCat{a, r}}
574 case None{}:
575 left
576
577
578def required.prefix(n: Node) -> Maybe<&2, Node>:
579 match n:
580 case NSet{False{}, Con{Rng{+lo, +hi}, Nil{}}}:
581 Bool.pick(Maybe<&2, Node>, U32.is_eq(lo, hi) && U32.is_lt(lo, 128), Some{lit(lo)}, None{})
582 case NCat{+a, b}:
583 required.join(required.prefix(b), required.prefix(a), a)
584 case NPlus{g, a}:
585 required.prefix(a)
586 case NGroup{i, a}:
587 required.prefix(a)
588 case _:
589 None{}
590
591def reverse.ok(n: Node) -> Bool:
592 match n:
593 case NAssert{k}:
594 False{}
595 case NCat{a, b}:
596 reverse.ok(a) && reverse.ok(b)
597 case NAlt{a, b}:
598 reverse.ok(a) && reverse.ok(b)
599 case NPlus{g, a}:
600 reverse.ok(a)
601 case NQuest{g, a}:
602 reverse.ok(a)
603 case NGroup{i, a}:
604 reverse.ok(a)
605 case _:
606 True{}
607
608def reverse.node(n: Node) -> Node:
609 match n:
610 case NCat{a, b}:
611 NCat{reverse.node(b), reverse.node(a)}
612 case NAlt{a, b}:
613 NAlt{reverse.node(a), reverse.node(b)}
614 case NPlus{g, a}:
615 NPlus{g, reverse.node(a)}
616 case NQuest{g, a}:
617 NQuest{g, reverse.node(a)}
618 case NGroup{i, a}:
619 reverse.node(a)
620 case other:
621 other
622
623def size(n: Node) -> U32:
624 match n:
625 case NEmpty{}:
626 0
627 case NSet{neg, items}:
628 1
629 case NAssert{k}:
630 1
631 case NCat{a, b}:
632 (size(a) + size(b) : U32)
633 case NAlt{a, b}:
634 (2 + size(a) + size(b) : U32)
635 case NPlus{g, a}:
636 (1 + size(a) : U32)
637 case NQuest{g, a}:
638 (1 + size(a) : U32)
639 case NGroup{i, a}:
640 (2 + size(a) : U32)
641
642
643def emit(n: Node, +pc: U32, rest: List<&2, Inst>) -> List<&2, Inst>:
644 match n:
645 case NEmpty{}:
646 rest
647 case NSet{neg, items}:
648 ISet{neg, items} <> rest
649 case NAssert{k}:
650 IAssert{k} <> rest
651 case NCat{+a, b}:
652 emit(a, pc, emit(b, (pc + size(a) : U32), rest))
653 case NAlt{+a, +b}:
654 +j = (pc + 1 + size(a) : U32)
655 ISplit{(pc + 1 : U32), (j + 1 : U32)} <> emit(a, (pc + 1 : U32), IJmp{(j + 1 + size(b) : U32)} <> emit(b, (j + 1 : U32), rest))
656 case NPlus{+g, +a}:
657 +out = (pc + 1 + size(a) : U32)
658 emit(a, pc, ISplit{Bool.pick(U32, g, pc, out), Bool.pick(U32, g, out, pc)} <> rest)
659 case NQuest{+g, +a}:
660 +out = (pc + 1 + size(a) : U32)
661 ISplit{Bool.pick(U32, g, (pc + 1 : U32), out), Bool.pick(U32, g, out, (pc + 1 : U32))} <> emit(a, (pc + 1 : U32), rest)
662 case NGroup{+i, a}:
663 ISave{(2 * i : U32)} <> emit(a, (pc + 1 : U32), ISave{(2 * i + 1 : U32)} <> rest)
664
665
666
667type Trie<-V: Data> is Data:
668 TTip{}
669 TNode{val: Maybe<&2, V>, lo: Trie<V>, hi: Trie<V>}
670
671
672def trie.get(-V: Data, t: Trie<V>, here: Bool, left: Bool, +n: U32) -> Maybe<&2, V>:
673 match t:
674 case TTip{}:
675 None{}
676 case TNode{v, lo, hi}:
677 match here:
678 case True{}:
679 v
680 case False{}:
681 match left:
682 case True{}:
683 trie.get(V, lo, U32.is_eq(U32.shr(n), 1), U32.is_even(U32.shr(n)), U32.shr(n))
684 case False{}:
685 trie.get(V, hi, U32.is_eq(U32.shr(n), 1), U32.is_even(U32.shr(n)), U32.shr(n))
686
687
688def trie.put(-V: Data, fuel: Nat, t: Trie<V>, here: Bool, left: Bool, +n: U32, v: V) -> Trie<V>:
689 match fuel:
690 case 0n:
691 t
692 case 1n+f:
693 match t:
694 case TNode{x, lo, hi}:
695 match here:
696 case True{}:
697 TNode{Some{v}, lo, hi}
698 case False{}:
699 match left:
700 case True{}:
701 TNode{x, trie.put(V, f, lo, U32.is_eq(U32.shr(n), 1), U32.is_even(U32.shr(n)), U32.shr(n), v), hi}
702 case False{}:
703 TNode{x, lo, trie.put(V, f, hi, U32.is_eq(U32.shr(n), 1), U32.is_even(U32.shr(n)), U32.shr(n), v)}
704 case TTip{}:
705 match here:
706 case True{}:
707 TNode{Some{v}, TTip{}, TTip{}}
708 case False{}:
709 match left:
710 case True{}:
711 TNode{None{}, trie.put(V, f, TTip{}, U32.is_eq(U32.shr(n), 1), U32.is_even(U32.shr(n)), U32.shr(n), v), TTip{}}
712 case False{}:
713 TNode{None{}, TTip{}, trie.put(V, f, TTip{}, U32.is_eq(U32.shr(n), 1), U32.is_even(U32.shr(n)), U32.shr(n), v)}
714
715
716def trie.at(-V: Data, t: Trie<V>, +k: U32) -> Maybe<&2, V>:
717 +n = (k + 1 : U32)
718 trie.get(V, t, U32.is_eq(n, 1), U32.is_even(n), n)
719
720def trie.set(-V: Data, t: Trie<V>, +k: U32, v: V) -> Trie<V>:
721 +n = (k + 1 : U32)
722 trie.put(V, 32n, t, U32.is_eq(n, 1), U32.is_even(n), n, v)
723
724def trie.from(-V: Data, xs: List<&2, V>, +k: U32, t: Trie<V>) -> Trie<V>:
725 match xs:
726 case Nil{}:
727 t
728 case Con{h, r}:
729 trie.from(V, r, (k + 1 : U32), trie.set(V, t, k, h))
730
731
732
733type Fs is Data:
734 Fs{stack: List<&2, U32>, seen: List<&2, U32>, sets: List<&2, Inst>}
735 FsAny{}
736
737def first.inst(i: Maybe<&2, Inst>, +pc: U32, stack: List<&2, U32>, seen: List<&2, U32>, sets: List<&2, Inst>) -> Fs:
738 match i:
739 case Some{IJmp{x}}:
740 Fs{x <> stack, seen, sets}
741 case Some{ISplit{x, y}}:
742 Fs{x <> y <> stack, seen, sets}
743 case Some{ISave{k}}:
744 Fs{(pc + 1 : U32) <> stack, seen, sets}
745 case Some{ISet{neg, items}}:
746 Fs{stack, seen, ISet{neg, items} <> sets}
747 case _:
748 FsAny{}
749
750def first.seen(hit: Bool, +prog: List<&2, Inst>, +pc: U32, stack: List<&2, U32>, seen: List<&2, U32>, sets: List<&2, Inst>) -> Fs:
751 match hit:
752 case True{}:
753 Fs{stack, seen, sets}
754 case False{}:
755 first.inst(List.get(&2, Inst, prog, U32.to_nat(pc)), pc, stack, pc <> seen, sets)
756
757
758def first(fuel: Nat, +prog: List<&2, Inst>, st: Fs) -> Maybe<&2, List<&2, Inst>>:
759 match fuel:
760 case 0n:
761 None{}
762 case 1n+f:
763 match st:
764 case FsAny{}:
765 None{}
766 case Fs{Nil{}, seen, sets}:
767 Some{sets}
768 case Fs{Con{+pc, t}, +seen, sets}:
769 first(f, prog, first.seen(List.contains(~U32, ~U32.is_eq, seen, pc), prog, pc, t, seen, sets))
770
771
772
773
774type Ew is Data:
775 Ew{stack: List<&2, U32>, seen: List<&2, U32>, mask: U32, hit: Bool}
776
777def eps.ctx(k: U32, +at0: Bool, +at1: Bool) -> Bool:
778 match k:
779 case 0:
780 at0
781 case 1:
782 at1
783 case _:
784 False{}
785
786def eps.assert(ok: Bool, +pc: U32, stack: List<&2, U32>, seen: List<&2, U32>, mask: U32, hit: Bool) -> Ew:
787 match ok:
788 case True{}:
789 Ew{(pc + 1 : U32) <> stack, seen, mask, hit}
790 case False{}:
791 Ew{stack, seen, mask, hit}
792
793def eps.inst(i: Maybe<&2, Inst>, +pc: U32, +at0: Bool, +at1: Bool, stack: List<&2, U32>, seen: List<&2, U32>, +mask: U32, hit: Bool) -> Ew:
794 match i:
795 case Some{IJmp{x}}:
796 Ew{x <> stack, seen, mask, hit}
797 case Some{ISplit{x, y}}:
798 Ew{x <> y <> stack, seen, mask, hit}
799 case Some{ISave{k}}:
800 Ew{(pc + 1 : U32) <> stack, seen, mask, hit}
801 case Some{IAssert{k}}:
802 eps.assert(eps.ctx(k, at0, at1), pc, stack, seen, mask, hit)
803 case Some{ISet{neg, items}}:
804 Ew{stack, seen, (mask .|. (1 << U32.to_nat(pc)) : U32), hit}
805 case Some{IMatch{}}:
806 Ew{stack, seen, mask, True{}}
807 case None{}:
808 Ew{stack, seen, mask, hit}
809
810def eps.seen(hit: Bool, +prog: List<&2, Inst>, +pc: U32, +at0: Bool, +at1: Bool, w: Ew) -> Ew:
811 match hit:
812 case True{}:
813 w
814 case False{}:
815 Ew{stack, seen, mask, h} = w
816 eps.inst(List.get(&2, Inst, prog, U32.to_nat(pc)), pc, at0, at1, stack, pc <> seen, mask, h)
817
818
819def eps.go(fuel: Nat, +prog: List<&2, Inst>, +at0: Bool, +at1: Bool, w: Ew) -> Ew:
820 match fuel:
821 case 0n:
822 w
823 case 1n+f:
824 match w:
825 case Ew{Nil{}, seen, mask, hit}:
826 Ew{Nil{}, seen, mask, hit}
827 case Ew{Con{+pc, t}, +seen, mask, hit}:
828 eps.go(f, prog, at0, at1, eps.seen(List.contains(~U32, ~U32.is_eq, seen, pc), prog, pc, at0, at1, Ew{t, seen, mask, hit}))
829
830def eps(+fuel: Nat, +prog: List<&2, Inst>, +pc: U32, +at0: Bool, +at1: Bool) -> Ew:
831 eps.go(fuel, prog, at0, at1, Ew{[pc], Nil{}, 0, False{}})
832
833def Ew.mask(w: Ew) -> U32:
834 Ew{s, v, mask, hit} = w
835 mask
836
837def Ew.hit(w: Ew) -> Bool:
838 Ew{s, v, mask, hit} = w
839 hit
840
841
842
843type Bit is Data:
844 Bit{mask: U32, neg: Bool, items: List<&2, Item>, follow: U32, fin: Bool, end: Bool}
845
846
847
848type Bits is Data:
849 Bits{sets: List<&2, Bit>, at0: U32, hit0: Bool, hit01: Bool, atn: U32, hit1: Bool}
850
851def bits.set(+fuel: Nat, +prog: List<&2, Inst>, +pc: U32, neg: Bool, items: List<&2, Item>) -> Bit:
852 +w = eps(fuel, prog, (pc + 1 : U32), False{}, False{})
853 Bit{(1 << U32.to_nat(pc) : U32), neg, items, Ew.mask(w), Ew.hit(w), Ew.hit(eps(fuel, prog, (pc + 1 : U32), False{}, True{}))}
854
855def bits.sets(xs: List<&2, Inst>, +fuel: Nat, +prog: List<&2, Inst>, +pc: U32) -> List<&2, Bit>:
856 match xs:
857 case Nil{}:
858 Nil{}
859 case Con{ISet{neg, items}, t}:
860 bits.set(fuel, prog, pc, neg, items) <> bits.sets(t, fuel, prog, (pc + 1 : U32))
861 case Con{i, t}:
862 bits.sets(t, fuel, prog, (pc + 1 : U32))
863
864
865def bits.plain(xs: List<&2, Inst>) -> Bool:
866 match xs:
867 case Nil{}:
868 True{}
869 case Con{IAssert{+k}, t}:
870 U32.is_lt(k, 2) && bits.plain(t)
871 case Con{i, t}:
872 bits.plain(t)
873
874def bits.if(ok: Bool, +fuel: Nat, +prog: List<&2, Inst>) -> Maybe<&2, Bits>:
875 match ok:
876 case False{}:
877 None{}
878 case True{}:
879 +w0 = eps(fuel, prog, 0, True{}, False{})
880 +wn = eps(fuel, prog, 0, False{}, False{})
881 Some{Bits{bits.sets(prog, fuel, prog, 0), Ew.mask(w0), Ew.hit(w0), Ew.hit(eps(fuel, prog, 0, True{}, True{})), Ew.mask(wn), Ew.hit(eps(fuel, prog, 0, False{}, True{}))}}
882
883def bits(+fuel: Nat, +prog: List<&2, Inst>) -> Maybe<&2, Bits>:
884 bits.if(Nat.is_le(List.length(&2, Inst, prog), 32n) && bits.plain(prog), fuel, prog)
885
886def item.has(i: Item, +c: U32) -> Bool:
887 match i:
888 case Rng{+lo, +hi}:
889 U32.is_le(lo, c) && U32.is_le(c, hi)
890 case Prop{neg, name}:
891 Bool.xor(neg, String.starts_with(U.category(Chr{c}), name))
892
893def items.has(xs: List<&2, Item>, +c: U32) -> Bool:
894 match xs:
895 case Nil{}:
896 False{}
897 case Con{h, t}:
898 item.has(h, c) || items.has(t, c)
899
900def starts(xs: List<&2, Inst>, +c: U32) -> Bool:
901 match xs:
902 case Nil{}:
903 False{}
904 case Con{ISet{neg, set}, t}:
905 Bool.xor(neg, items.has(set, c)) || starts(t, c)
906 case Con{i, t}:
907 starts(t, c)
908
909
910type Asc is Data:
911 Asc{m0: U32, m1: U32, m2: U32, m3: U32}
912
913def asc.bit(hit: Bool, +c: U32, a: Asc) -> Asc:
914 match hit:
915 case False{}:
916 a
917 case True{}:
918 Asc{+m0, +m1, +m2, +m3} = a
919 +b = (1 << U32.to_nat((c .&. 31 : U32)) : U32)
920 Asc{Bool.pick(U32, U32.is_eq((c >> 5n : U32), 0), (m0 .|. b : U32), m0), Bool.pick(U32, U32.is_eq((c >> 5n : U32), 1), (m1 .|. b : U32), m1), Bool.pick(U32, U32.is_eq((c >> 5n : U32), 2), (m2 .|. b : U32), m2), Bool.pick(U32, U32.is_eq((c >> 5n : U32), 3), (m3 .|. b : U32), m3)}
921
922
923def asc.go(n: Nat, +c: U32, +sets: List<&2, Inst>, a: Asc) -> Asc:
924 match n:
925 case 0n:
926 a
927 case 1n+p:
928 asc.go(p, (c - 1 : U32), sets, asc.bit(starts(sets, c), c, a))
929
930def asc(start: Maybe<&2, List<&2, Inst>>) -> Maybe<&2, Asc>:
931 match start:
932 case None{}:
933 None{}
934 case Some{sets}:
935 Some{asc.go(128n, 127, sets, Asc{0, 0, 0, 0})}
936
937
938
939
940
941
942def rev.build(m: Maybe<&2, Node>) -> Maybe<&2, Bits>:
943 match m:
944 case None{}:
945 None{}
946 case Some{node}:
947 +insts = emit(reverse.node(node), 0, [IMatch{}])
948 +fuel = Nat.add(Nat.mul(3n, List.length(&2, Inst, insts)), 2n)
949 bits(fuel, insts)
950
951def rev.if(ok: Bool, node: Node) -> Maybe<&2, Bits>:
952 match ok:
953 case False{}:
954 None{}
955 case True{}:
956 rev.build(required.prefix(node))
957
958type Regex is Data:
959 Regex{prog: Trie<Inst>, fuel: Nat, slots: Nat, start: Maybe<&2, List<&2, Inst>>, bits: Maybe<&2, Bits>, asc: Maybe<&2, Asc>, plain: Bool, must: Maybe<&2, U32>, reverse: Maybe<&2, Bits>}
960
961def build(+node: Node, +n: U32) -> Regex:
962 +insts = {ISave{0} <> emit(node, 1, [ISave{1}, IMatch{}]) : List<&2, Inst>}
963 +fuel = Nat.add(Nat.mul(3n, List.length(&2, Inst, insts)), 2n)
964 +start = first(fuel, insts, Fs{[0], Nil{}, Nil{}})
965 Regex{trie.from(Inst, insts, 0, TTip{}), fuel, U32.to_nat((2 * n : U32)), start, bits(fuel, insts), asc(start), bits.plain(insts), required(node), rev.if(reverse.ok(node), node)}
966
967def compile.fin(st: Ps) -> Maybe<&2, Regex>:
968 match st:
969 case PsFail{}:
970 None{}
971 case Ps{n, rep, stack, alts, cur}:
972 match stack:
973 case Nil{}:
974 Some{build(alt.go(alts, seq(cur)), n)}
975 case Con{f, up}:
976 None{}
977
978def compile.parse(toks: Maybe<&2, List<&2, Tok>>) -> Maybe<&2, Regex>:
979 match toks:
980 case None{}:
981 None{}
982 case Some{ts}:
983 compile.fin(parse(ts, Ps{1, False{}, Nil{}, Nil{}, Nil{}}))
984
985
986def compile(+pat: String) -> Maybe<&2, Regex>:
987 compile.parse(lex(Nat.add(String.length(pat), 2n), LGo{pat, Nil{}}))
988
989
990
991
992def word(m: Maybe<&2, Char>) -> Bool:
993 match m:
994 case None{}:
995 False{}
996 case Some{Chr{+c}}:
997 is_word(c)
998
999def assert.ok(k: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>) -> Bool:
1000 match k:
1001 case 0:
1002 Maybe.is_none(&2, Char, prev)
1003 case 1:
1004 Maybe.is_none(&2, Char, next)
1005 case 2:
1006 Bool.xor(word(prev), word(next))
1007 case _:
1008 Bool.not(Bool.xor(word(prev), word(next)))
1009
1010
1011type Th is Data:
1012 Th{pc: U32, caps: List<&2, Maybe<&2, U32>>}
1013
1014
1015
1016type Cl is Data:
1017 Cl{stack: List<&2, Th>, seen: Trie<Unit>, out: List<&2, Th>}
1018
1019def close.assert(ok: Bool, +pc: U32, caps: List<&2, Maybe<&2, U32>>, stack: List<&2, Th>, seen: Trie<Unit>, out: List<&2, Th>) -> Cl:
1020 match ok:
1021 case True{}:
1022 Cl{Th{(pc + 1 : U32), caps} <> stack, seen, out}
1023 case False{}:
1024 Cl{stack, seen, out}
1025
1026def close.inst(i: Maybe<&2, Inst>, +pc: U32, +caps: List<&2, Maybe<&2, U32>>, stack: List<&2, Th>, seen: Trie<Unit>, out: List<&2, Th>, +pos: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>) -> Cl:
1027 match i:
1028 case None{}:
1029 Cl{stack, seen, out}
1030 case Some{IJmp{x}}:
1031 Cl{Th{x, caps} <> stack, seen, out}
1032 case Some{ISplit{x, y}}:
1033 Cl{Th{x, caps} <> Th{y, caps} <> stack, seen, out}
1034 case Some{ISave{k}}:
1035 Cl{Th{(pc + 1 : U32), List.set(&2, Maybe<&2, U32>, caps, U32.to_nat(k), Some{pos})} <> stack, seen, out}
1036 case Some{IAssert{k}}:
1037 close.assert(assert.ok(k, prev, next), pc, caps, stack, seen, out)
1038 case Some{ISet{neg, items}}:
1039 Cl{stack, seen, Th{pc, caps} <> out}
1040 case Some{IMatch{}}:
1041 Cl{stack, seen, Th{pc, caps} <> out}
1042
1043
1044
1045def close.seen(hit: Bool, +prog: Trie<Inst>, +pc: U32, caps: List<&2, Maybe<&2, U32>>, stack: List<&2, Th>, seen: Trie<Unit>, out: List<&2, Th>, +pos: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>) -> Cl:
1046 match hit:
1047 case True{}:
1048 Cl{stack, seen, out}
1049 case False{}:
1050 close.inst(trie.at(Inst, prog, pc), pc, caps, stack, trie.set(Unit, seen, pc, Unit{}), out, pos, prev, next)
1051
1052def close.step(th: Th, stack: List<&2, Th>, +seen: Trie<Unit>, out: List<&2, Th>, +prog: Trie<Inst>, +pos: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>) -> Cl:
1053 Th{+pc, caps} = th
1054 close.seen(Maybe.is_some(&2, Unit, trie.at(Unit, seen, pc)), prog, pc, caps, stack, seen, out, pos, prev, next)
1055
1056
1057def close(fuel: Nat, +prog: Trie<Inst>, +pos: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>, st: Cl) -> List<&2, Th>:
1058 match fuel:
1059 case 0n:
1060 Cl{stack, seen, out} = st
1061 List.reverse(&2, Th, out)
1062 case 1n+f:
1063 match st:
1064 case Cl{Nil{}, seen, out}:
1065 List.reverse(&2, Th, out)
1066 case Cl{Con{th, t}, seen, out}:
1067 close(f, prog, pos, prev, next, close.step(th, t, seen, out, prog, pos, prev, next))
1068
1069
1070
1071type Sc is Data:
1072 Sc{items: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>, stop: Bool}
1073
1074def scan.set(hit: Bool, +pc: U32, caps: List<&2, Maybe<&2, U32>>, items: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Sc:
1075 match hit:
1076 case True{}:
1077 Sc{Th{(pc + 1 : U32), caps} <> items, best, False{}}
1078 case False{}:
1079 Sc{items, best, False{}}
1080
1081def scan.char(c: Maybe<&2, Char>, neg: Bool, set: List<&2, Item>, +pc: U32, caps: List<&2, Maybe<&2, U32>>, items: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Sc:
1082 match c:
1083 case None{}:
1084 Sc{items, best, False{}}
1085 case Some{Chr{+x}}:
1086 scan.set(Bool.xor(neg, items.has(set, x)), pc, caps, items, best)
1087
1088
1089def scan.hit(any: Bool, caps: List<&2, Maybe<&2, U32>>, items: List<&2, Th>) -> Sc:
1090 match any:
1091 case True{}:
1092 Sc{Nil{}, Some{caps}, True{}}
1093 case False{}:
1094 Sc{items, Some{caps}, True{}}
1095
1096def scan.inst(i: Maybe<&2, Inst>, c: Maybe<&2, Char>, +any: Bool, +pc: U32, caps: List<&2, Maybe<&2, U32>>, items: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Sc:
1097 match i:
1098 case Some{IMatch{}}:
1099 scan.hit(any, caps, items)
1100 case Some{ISet{neg, set}}:
1101 scan.char(c, neg, set, pc, caps, items, best)
1102 case _:
1103 Sc{items, best, False{}}
1104
1105def scan.go(stop: Bool, th: Th, +prog: Trie<Inst>, c: Maybe<&2, Char>, +any: Bool, items: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Sc:
1106 match stop:
1107 case True{}:
1108 Sc{items, best, True{}}
1109 case False{}:
1110 Th{+pc, caps} = th
1111 scan.inst(trie.at(Inst, prog, pc), c, any, pc, caps, items, best)
1112
1113def scan.step(st: Sc, th: Th, +prog: Trie<Inst>, c: Maybe<&2, Char>, +any: Bool) -> Sc:
1114 Sc{items, best, stop} = st
1115 scan.go(stop, th, prog, c, any, items, best)
1116
1117def scan(xs: List<&2, Th>, +prog: Trie<Inst>, +c: Maybe<&2, Char>, +any: Bool, st: Sc) -> Sc:
1118 match xs:
1119 case Nil{}:
1120 st
1121 case Con{th, t}:
1122 scan(t, prog, c, any, scan.step(st, th, prog, c, any))
1123
1124
1125type Vm is Data:
1126 Vm{ths: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>}
1127
1128
1129def seed(best: Maybe<&2, List<&2, Maybe<&2, U32>>>, xs: List<&2, Th>, init: List<&2, Maybe<&2, U32>>) -> List<&2, Th>:
1130 match best:
1131 case None{}:
1132 List.append(&2, Th, xs, [Th{0, init}])
1133 case Some{b}:
1134 xs
1135
1136
1137def seed.skip(items: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>, start: Maybe<&2, List<&2, Inst>>, next: Maybe<&2, Char>) -> Bool:
1138 match items best start next:
1139 case Nil{} None{} Some{sets} None{}:
1140 True{}
1141 case Nil{} None{} Some{sets} Some{Chr{+c}}:
1142 Bool.not(starts(sets, c))
1143 case _ _ _ _:
1144 False{}
1145
1146def run.seed(skip: Bool, items: List<&2, Th>, +best: Maybe<&2, List<&2, Maybe<&2, U32>>>, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +pos: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>) -> Vm:
1147 match skip:
1148 case True{}:
1149 Vm{Nil{}, None{}}
1150 case False{}:
1151 Vm{close(fuel, prog, pos, prev, next, Cl{seed(best, List.reverse(&2, Th, items), init), TTip{}, Nil{}}), best}
1152
1153def run.close(sc: Sc, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +pos: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>) -> Vm:
1154 Sc{+items, +best, stop} = sc
1155 run.seed(seed.skip(items, best, start, next), items, best, prog, fuel, init, pos, prev, next)
1156
1157def run.step(st: Vm, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool, +pos: U32, +c: Char, +next: Maybe<&2, Char>) -> Vm:
1158 Vm{ths, best} = st
1159 run.close(scan(ths, prog, Some{c}, any, Sc{Nil{}, best, False{}}), prog, fuel, init, start, pos, Some{c}, next)
1160
1161def run.end(sc: Sc) -> Maybe<&2, List<&2, Maybe<&2, U32>>>:
1162 Sc{items, best, stop} = sc
1163 best
1164
1165
1166def run(s: String, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool, +pos: U32, st: Vm) -> Maybe<&2, List<&2, Maybe<&2, U32>>>:
1167 match s:
1168 case SNil{}:
1169 Vm{ths, best} = st
1170 run.end(scan(ths, prog, None{}, any, Sc{Nil{}, best, False{}}))
1171 case SCon{+c, +t}:
1172 match st:
1173 case Vm{Nil{}, Some{b}}:
1174 Some{b}
1175 case Vm{ths, best}:
1176 +p = (pos + 1 : U32)
1177 run(t, prog, fuel, init, start, any, p, run.step(Vm{ths, best}, prog, fuel, init, start, any, p, c, String.get(t, 0n)))
1178
1179type Span is Data:
1180 Span{start: U32, end: U32}
1181
1182def spans(caps: List<&2, Maybe<&2, U32>>) -> List<&2, Maybe<&2, Span>>:
1183 match caps:
1184 case Con{Some{a}, Con{Some{b}, t}}:
1185 Some{Span{a, b}} <> spans(t)
1186 case Con{x, Con{y, t}}:
1187 None{} <> spans(t)
1188 case _:
1189 Nil{}
1190
1191def find.spans(m: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Maybe<&2, List<&2, Maybe<&2, Span>>>:
1192 match m:
1193 case None{}:
1194 None{}
1195 case Some{caps}:
1196 Some{spans(caps)}
1197
1198
1199def exec(re: Regex, +s: String, +any: Bool) -> Maybe<&2, List<&2, Maybe<&2, U32>>>:
1200 Regex{+prog, +fuel, +slots, +start, bits, asc, plain, must, reverse} = re
1201 +init = List.replicate(Maybe<&2, U32>, Bool.pick(Nat, any, 0n, slots), None{})
1202 run(s, prog, fuel, init, start, any, 0, run.close(Sc{Nil{}, None{}, False{}}, prog, fuel, init, start, 0, None{}, String.get(s, 0n)))
1203
1204
1205def find(re: Regex, +s: String) -> Maybe<&2, List<&2, Maybe<&2, Span>>>:
1206 find.spans(exec(re, s, False{}))
1207
1208
1209def is_match.vm(re: Regex, +s: String) -> Bool:
1210 Maybe.is_some(&2, List<&2, Maybe<&2, U32>>, exec(re, s, True{}))
1211
1212
1213type Bs is Data:
1214 Bs{next: U32, fin: Bool, end: Bool}
1215
1216def bits.take(hit: Bool, +follow: U32, +fin: Bool, +end: Bool, acc: Bs) -> Bs:
1217 match hit:
1218 case False{}:
1219 acc
1220 case True{}:
1221 Bs{+nx, f, e} = acc
1222 Bs{(nx .|. follow : U32), f || fin, e || end}
1223
1224def bits.char(live: Bool, +c: U32, neg: Bool, items: List<&2, Item>, +follow: U32, +fin: Bool, +end: Bool, acc: Bs) -> Bs:
1225 match live:
1226 case False{}:
1227 acc
1228 case True{}:
1229 bits.take(Bool.xor(neg, items.has(items, c)), follow, fin, end, acc)
1230
1231
1232def bits.step(xs: List<&2, Bit>, +cur: U32, +c: U32, acc: Bs) -> Bs:
1233 match xs:
1234 case Nil{}:
1235 acc
1236 case Con{Bit{+mask, neg, items, follow, fin, end}, t}:
1237 bits.step(t, cur, c, bits.char(U32.is_ne((cur .&. mask : U32), 0), c, neg, items, follow, fin, end, acc))
1238
1239
1240def bits.idle(start: Maybe<&2, List<&2, Inst>>, +cur: U32, +atn: U32, +c: U32) -> Bool:
1241 match start:
1242 case None{}:
1243 False{}
1244 case Some{sets}:
1245 U32.is_eq(cur, atn) && Bool.not(starts(sets, c))
1246
1247
1248def bits.go(idle: Bool, +sets: List<&2, Bit>, +atn: U32, +hit1: Bool, +cur: U32, +c: U32) -> Bs:
1249 match idle:
1250 case True{}:
1251 Bs{atn, False{}, hit1}
1252 case False{}:
1253 bits.step(sets, cur, c, Bs{atn, False{}, hit1})
1254
1255
1256
1257
1258def bits.run(s: String, +sets: List<&2, Bit>, +start: Maybe<&2, List<&2, Inst>>, +atn: U32, +hit1: Bool, r: Bs) -> Bool:
1259 match s:
1260 case SNil{}:
1261 Bs{cur, done, ok} = r
1262 done || ok
1263 case SCon{Chr{+c}, t}:
1264 match r:
1265 case Bs{cur, True{}, ok}:
1266 True{}
1267 case Bs{+cur, False{}, ok}:
1268 bits.run(t, sets, start, atn, hit1, bits.go(bits.idle(start, cur, atn, c), sets, atn, hit1, cur, c))
1269
1270def bits.is_match(b: Bits, start: Maybe<&2, List<&2, Inst>>, s: String) -> Bool:
1271 Bits{sets, at0, hit0, hit01, atn, hit1} = b
1272 bits.run(s, sets, start, atn, hit1, Bs{at0, hit0, hit01})
1273
1274
1275def is_match.bits(re: Regex, s: String) -> Maybe<&2, Bool>:
1276 Regex{prog, fuel, slots, start, bits, asc, plain, must, reverse} = re
1277 match bits:
1278 case None{}:
1279 None{}
1280 case Some{b}:
1281 Some{bits.is_match(b, start, s)}
1282
1283def is_match.pick(m: Maybe<&2, Bool>, re: Regex, +s: String) -> Bool:
1284 match m:
1285 case Some{x}:
1286 x
1287 case None{}:
1288 is_match.vm(re, s)
1289
1290
1291def is_match(+re: Regex, +s: String) -> Bool:
1292 is_match.pick(is_match.bits(re, s), re, s)
1293
1294
1295
1296
1297
1298
1299
1300type Dc is Data:
1301 Dc{c: U32, w: U32}
1302 DEnd{}
1303
1304def Dc.char(d: Dc) -> Maybe<&2, Char>:
1305 match d:
1306 case DEnd{}:
1307 None{}
1308 case Dc{c, w}:
1309 Some{Chr{c}}
1310
1311def pk.if(ok: Bool, a: Array<U32>, +i: U32) -> Array<U32> & U32:
1312 match ok:
1313 case True{}:
1314 Bytes.peek(a, i)
1315 case False{}:
1316 (a, 0)
1317
1318
1319def pk(a: Array<U32>, +len: U32, +i: U32) -> Array<U32> & U32:
1320 pk.if(U32.is_lt(i, len), a, i)
1321
1322def cont(+b: U32) -> Bool:
1323 U32.is_eq((b .&. 192 : U32), 128)
1324
1325def dec.pick(ok2: Bool, ok3: Bool, ok4: Bool, +c2: U32, +c3: U32, +c4: U32) -> Dc:
1326 match ok2:
1327 case True{}:
1328 Dc{c2, 2}
1329 case False{}:
1330 match ok3:
1331 case True{}:
1332 Dc{c3, 3}
1333 case False{}:
1334 match ok4:
1335 case True{}:
1336 Dc{c4, 4}
1337 case False{}:
1338 Dc{65533, 1}
1339
1340
1341def dec.n(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> Dc:
1342 +x1 = (b1 .&. 63 : U32)
1343 +x2 = (b2 .&. 63 : U32)
1344 +x3 = (b3 .&. 63 : U32)
1345 +c2 = (((b0 .&. 31) << 6n) .|. x1 : U32)
1346 +c3 = ((((b0 .&. 15) << 12n) .|. (x1 << 6n)) .|. x2 : U32)
1347 +c4 = (((((b0 .&. 7) << 18n) .|. (x1 << 12n)) .|. (x2 << 6n)) .|. x3 : U32)
1348 +ok2 = U32.is_le(192, b0) && U32.is_lt(b0, 224) && cont(b1) && U32.is_le(128, c2)
1349 +ok3 = U32.is_le(224, b0) && U32.is_lt(b0, 240) && cont(b1) && cont(b2) && U32.is_le(2048, c3) && (U32.is_lt(c3, 55296) || U32.is_lt(57343, c3))
1350 +ok4 = U32.is_le(240, b0) && U32.is_lt(b0, 248) && cont(b1) && cont(b2) && cont(b3) && U32.is_le(65536, c4) && U32.is_le(c4, 1114111)
1351 dec.pick(ok2, ok3, ok4, c2, c3, c4)
1352
1353def dec.b3(+b0: U32, +b1: U32, +b2: U32, r: Array<U32> & U32) -> Array<U32> & Dc:
1354 (a, +b3) = r
1355 (a, dec.n(b0, b1, b2, b3))
1356
1357def dec.b2(+len: U32, +i: U32, +b0: U32, +b1: U32, r: Array<U32> & U32) -> Array<U32> & Dc:
1358 (a, +b2) = r
1359 dec.b3(b0, b1, b2, pk(a, len, (i + 3 : U32)))
1360
1361def dec.b1(+len: U32, +i: U32, +b0: U32, r: Array<U32> & U32) -> Array<U32> & Dc:
1362 (a, +b1) = r
1363 dec.b2(len, i, b0, b1, pk(a, len, (i + 2 : U32)))
1364
1365def dec.lead(ascii: Bool, +len: U32, +i: U32, +b0: U32, a: Array<U32>) -> Array<U32> & Dc:
1366 match ascii:
1367 case True{}:
1368 (a, Dc{b0, 1})
1369 case False{}:
1370 dec.b1(len, i, b0, pk(a, len, (i + 1 : U32)))
1371
1372def dec.at(+len: U32, +i: U32, r: Array<U32> & U32) -> Array<U32> & Dc:
1373 (a, +b0) = r
1374 dec.lead(U32.is_lt(b0, 128), len, i, b0, a)
1375
1376def dec.if(ok: Bool, a: Array<U32>, +len: U32, +i: U32) -> Array<U32> & Dc:
1377 match ok:
1378 case True{}:
1379 dec.at(len, i, Bytes.peek(a, i))
1380 case False{}:
1381 (a, DEnd{})
1382
1383
1384def dec(a: Array<U32>, +len: U32, +i: U32) -> Array<U32> & Dc:
1385 dec.if(U32.is_lt(i, len), a, len, i)
1386
1387def asc.word(k: U32, a: Asc) -> U32:
1388 match k:
1389 case 0:
1390 Asc{m0, m1, m2, m3} = a
1391 m0
1392 case 1:
1393 Asc{m0, m1, m2, m3} = a
1394 m1
1395 case 2:
1396 Asc{m0, m1, m2, m3} = a
1397 m2
1398 case _:
1399 Asc{m0, m1, m2, m3} = a
1400 m3
1401
1402
1403def asc.has(+b: U32, a: Asc) -> Bool:
1404 U32.is_le(128, b) || U32.is_ne((U32.shrn(asc.word((b >> 5n : U32), a), U32.to_nat((b .&. 31 : U32))) .&. 1 : U32), 0)
1405
1406def probe.of(+m: Asc, r: Array<U32> & U32) -> Array<U32> & Bool:
1407 (a, +v) = r
1408 (a, asc.has(v, m))
1409
1410
1411def probe.if(ok: Bool, a: Array<U32>, +k: U32, +m: Asc) -> Array<U32> & Bool:
1412 match ok:
1413 case True{}:
1414 probe.of(m, Bytes.peek(a, k))
1415 case False{}:
1416 (a, True{})
1417
1418def probe(a: Array<U32>, +len: U32, +k: U32, +m: Asc) -> Array<U32> & Bool:
1419 probe.if(U32.is_lt(k, len), a, k, m)
1420
1421
1422def skip(fuel: Nat, r: Array<U32> & Bool, +len: U32, +k: U32, +m: Asc) -> Array<U32> & U32:
1423 match fuel:
1424 case 0n:
1425 (a, h) = r
1426 (a, k)
1427 case 1n+f:
1428 (a, hit) = r
1429 match hit:
1430 case True{}:
1431 (a, k)
1432 case False{}:
1433 skip(f, probe(a, len, (k + 1 : U32), m), len, (k + 1 : U32), m)
1434
1435def skip.from(a: Array<U32>, +len: U32, +k: U32, +m: Asc) -> Array<U32> & U32:
1436 skip(U32.to_nat((len - k : U32)), probe(a, len, k, m), len, k, m)
1437
1438
1439type Rb is Type:
1440 Rb{a: Array<U32>, i: U32, d: Dc, st: Vm}
1441
1442def rb.step(r: Array<U32> & Dc, +j: U32, st: Vm, +c: U32, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool) -> Rb:
1443 (a, +d) = r
1444 Rb{a, j, d, run.step(st, prog, fuel, init, start, any, j, Chr{c}, Dc.char(d))}
1445
1446
1447def rb.seed(r: Array<U32> & Dc, +k: U32, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>) -> Rb:
1448 (a, +d) = r
1449 Rb{a, k, d, run.close(Sc{Nil{}, None{}, False{}}, prog, fuel, init, start, k, None{}, Dc.char(d))}
1450
1451def rb.skip(r: Array<U32> & U32, +len: U32, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>) -> Rb:
1452 (a, +k) = r
1453 rb.seed(dec(a, len, k), k, prog, fuel, init, start)
1454
1455
1456
1457
1458def rb.idle(asc: Maybe<&2, Asc>, a: Array<U32>, +len: U32, +j: U32, +c: U32, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool) -> Rb:
1459 match asc:
1460 case None{}:
1461 rb.step(dec(a, len, j), j, Vm{Nil{}, None{}}, c, prog, fuel, init, start, any)
1462 case Some{+m}:
1463 rb.skip(skip.from(a, len, j, m), len, prog, fuel, init, start)
1464
1465
1466def runb(fuel: Nat, r: Rb, +len: U32, +prog: Trie<Inst>, +cfuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1467 match fuel:
1468 case 0n:
1469 Rb{a, i, d, st} = r
1470 (a, None{})
1471 case 1n+f:
1472 Rb{a, +i, d, st} = r
1473 match d:
1474 case DEnd{}:
1475 Vm{ths, best} = st
1476 (a, run.end(scan(ths, prog, None{}, any, Sc{Nil{}, best, False{}})))
1477 case Dc{+c, +w}:
1478 match st:
1479 case Vm{Nil{}, Some{b}}:
1480 (a, Some{b})
1481 case Vm{Nil{}, None{}}:
1482 runb(f, rb.idle(asc, a, len, (i + w : U32), c, prog, cfuel, init, start, any), len, prog, cfuel, init, start, asc, any)
1483 case Vm{ths, best}:
1484 +j = (i + w : U32)
1485 runb(f, rb.step(dec(a, len, j), j, Vm{ths, best}, c, prog, cfuel, init, start, any), len, prog, cfuel, init, start, asc, any)
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498def seed.id() -> U32:
1499 4294967295
1500
1501
1502type Op is Data:
1503 Op{src: U32, pc: U32, saves: List<&2, U32>}
1504
1505
1506
1507type Tr is Data:
1508 TrNo{}
1509 TrSame{}
1510 Tr{next: U32, hit: U32, outs: List<&2, Op>, fresh: Bool}
1511
1512type Sk is Data:
1513 Sk{pcs: List<&2, U32>, done: Bool}
1514
1515type Ix is Data:
1516 Ix{key: Sk, id: U32}
1517
1518
1519type Ik is Data:
1520 Ik{keys: Trie<List<&2, Ix>>, n: U32, id: U32}
1521
1522
1523type Lr is Data:
1524 Lr{hit: U32, outs: List<&2, Op>, key: Sk, fresh: Bool}
1525
1526def vm.pcs(xs: List<&2, Th>) -> List<&2, U32>:
1527 match xs:
1528 case Nil{}:
1529 Nil{}
1530 case Con{Th{pc, caps}, t}:
1531 pc <> vm.pcs(t)
1532
1533def vm.key(st: Vm) -> Sk:
1534 Vm{ths, best} = st
1535 Sk{vm.pcs(ths), Maybe.is_some(&2, List<&2, Maybe<&2, U32>>, best)}
1536
1537def pcs.eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
1538 match xs ys:
1539 case Nil{} Nil{}:
1540 True{}
1541 case Con{+a, s} Con{+b, t}:
1542 U32.is_eq(a, b) && pcs.eq(s, t)
1543 case _ _:
1544 False{}
1545
1546def sk.eq(a: Sk, b: Sk) -> Bool:
1547 Sk{p, x} = a
1548 Sk{q, y} = b
1549 Bool.not(Bool.xor(x, y)) && pcs.eq(p, q)
1550
1551def pcs.hash(xs: List<&2, U32>, +h: U32) -> U32:
1552 match xs:
1553 case Nil{}:
1554 h
1555 case Con{+pc, rest}:
1556 pcs.hash(rest, (U32.xor(h, pc) * 16777619 : U32))
1557
1558def sk.hash(k: Sk) -> U32:
1559 Sk{pcs, done} = k
1560 U32.and(pcs.hash(pcs, Bool.pick(U32, done, 2166136260, 2166136261)), 2147483647)
1561
1562def ix.find(xs: List<&2, Ix>, +k: Sk) -> U32:
1563 match xs:
1564 case Nil{}:
1565 seed.id()
1566 case Con{Ix{key, +id}, t}:
1567 Bool.pick(U32, sk.eq(key, k), id, ix.find(t, k))
1568
1569def intern.bucket(m: Maybe<&2, List<&2, Ix>>, +k: Sk) -> U32:
1570 match m:
1571 case None{}:
1572 seed.id()
1573 case Some{xs}:
1574 ix.find(xs, k)
1575
1576def intern.add(m: Maybe<&2, List<&2, Ix>>, +k: Sk, +n: U32) -> List<&2, Ix>:
1577 match m:
1578 case None{}:
1579 [Ix{k, n}]
1580 case Some{xs}:
1581 Ix{k, n} <> xs
1582
1583def intern.if(miss: Bool, +found: U32, +keys: Trie<List<&2, Ix>>, +n: U32, +k: Sk, +hash: U32) -> Ik:
1584 match miss:
1585 case True{}:
1586 Ik{trie.set(List<&2, Ix>, keys, hash, intern.add(trie.at(List<&2, Ix>, keys, hash), k, n)), (n + 1 : U32), n}
1587 case False{}:
1588 Ik{keys, n, found}
1589
1590def intern.full(room: Bool, +keys: Trie<List<&2, Ix>>, +n: U32, +k: Sk) -> Ik:
1591 match room:
1592 case True{}:
1593 +hash = sk.hash(k)
1594 +found = intern.bucket(trie.at(List<&2, Ix>, keys, hash), k)
1595 intern.if(U32.is_eq(found, seed.id()), found, keys, n, k, hash)
1596 case False{}:
1597 Ik{keys, n, seed.id()}
1598
1599
1600def intern(+keys: Trie<List<&2, Ix>>, +n: U32, +cap: U32, +k: Sk) -> Ik:
1601 intern.full(U32.is_lt(n, cap), keys, n, k)
1602
1603def sym.caps(+slots: Nat, +i: U32) -> List<&2, Maybe<&2, U32>>:
1604 List.append(&2, Maybe<&2, U32>, List.replicate(Maybe<&2, U32>, slots, None{}), [Some{i}])
1605
1606def sym.ths(xs: List<&2, Th>, +slots: Nat, +i: U32) -> List<&2, Th>:
1607 match xs:
1608 case Nil{}:
1609 Nil{}
1610 case Con{Th{pc, caps}, t}:
1611 Th{pc, sym.caps(slots, i)} <> sym.ths(t, slots, (i + 1 : U32))
1612
1613
1614def sym.src(xs: List<&2, Maybe<&2, U32>>) -> U32:
1615 match xs:
1616 case Con{Some{x}, Nil{}}:
1617 x
1618 case Con{h, t}:
1619 sym.src(t)
1620 case Nil{}:
1621 seed.id()
1622
1623
1624def sym.saves(xs: List<&2, Maybe<&2, U32>>, +k: U32) -> List<&2, U32>:
1625 match xs:
1626 case Con{h, Nil{}}:
1627 Nil{}
1628 case Con{Some{x}, t}:
1629 k <> sym.saves(t, (k + 1 : U32))
1630 case Con{None{}, t}:
1631 sym.saves(t, (k + 1 : U32))
1632 case Nil{}:
1633 Nil{}
1634
1635def sym.outs(xs: List<&2, Th>) -> List<&2, Op>:
1636 match xs:
1637 case Nil{}:
1638 Nil{}
1639 case Con{Th{+pc, +caps}, t}:
1640 Op{sym.src(caps), pc, sym.saves(caps, 0)} <> sym.outs(t)
1641
1642def sym.fresh(xs: List<&2, Op>) -> Bool:
1643 match xs:
1644 case Nil{}:
1645 True{}
1646 case Con{Op{+src, pc, saves}, t}:
1647 U32.is_eq(src, seed.id()) && sym.fresh(t)
1648
1649def op.same(saves: List<&2, U32>, +src: U32, +pc: U32, +i: U32, +old: U32) -> Bool:
1650 match saves:
1651 case Nil{}:
1652 U32.is_eq(src, i) && U32.is_eq(pc, old)
1653 case Con{h, t}:
1654 False{}
1655
1656def ops.same(xs: List<&2, Op>, ths: List<&2, Th>, +i: U32) -> Bool:
1657 match xs ths:
1658 case Nil{} Nil{}:
1659 True{}
1660 case Con{Op{+src, +pc, saves}, t} Con{Th{+old, caps}, rest}:
1661 op.same(saves, src, pc, i, old) && ops.same(t, rest, (i + 1 : U32))
1662 case _ _:
1663 False{}
1664
1665def tr.of(same: Bool, +next: U32, +hit: U32, +outs: List<&2, Op>, +fresh: Bool) -> Tr:
1666 match same:
1667 case True{}:
1668 TrSame{}
1669 case False{}:
1670 Tr{next, hit, outs, fresh}
1671
1672def sym.lr(+hit: U32, +done: Bool, v: Vm) -> Lr:
1673 Vm{+ths, best} = v
1674 +outs = sym.outs(ths)
1675 Lr{hit, outs, Sk{vm.pcs(ths), done}, Bool.not(done) && sym.fresh(outs)}
1676
1677def sym.hit(stop: Bool, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> U32:
1678 match stop:
1679 case True{}:
1680 match best:
1681 case None{}:
1682 0
1683 case Some{caps}:
1684 (sym.src(caps) + 1 : U32)
1685 case False{}:
1686 0
1687
1688
1689
1690def sym.close(sc: Sc, +done: Bool, +prog: Trie<Inst>, +fuel: Nat, +slots: Nat, +c: U32) -> Lr:
1691 Sc{items, +best, +stop} = sc
1692 sym.lr(sym.hit(stop, best), done || stop, run.close(Sc{items, best, stop}, prog, fuel, sym.caps(slots, seed.id()), None{}, 0, Some{Chr{c}}, Some{Chr{c}}))
1693
1694
1695def sym.best(best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Maybe<&2, List<&2, Maybe<&2, U32>>>:
1696 match best:
1697 case None{}:
1698 None{}
1699 case Some{b}:
1700 Some{Nil{}}
1701
1702def learn(st: Vm, +c: U32, +prog: Trie<Inst>, +fuel: Nat, +slots: Nat, +any: Bool) -> Lr:
1703 Vm{ths, +best} = st
1704 sym.close(scan(sym.ths(ths, slots, 0), prog, Some{Chr{c}}, any, Sc{Nil{}, sym.best(best), False{}}), Maybe.is_some(&2, List<&2, Maybe<&2, U32>>, best), prog, fuel, slots, c)
1705
1706def caps.at(m: Maybe<&2, Th>, +init: List<&2, Maybe<&2, U32>>) -> List<&2, Maybe<&2, U32>>:
1707 match m:
1708 case None{}:
1709 init
1710 case Some{Th{pc, caps}}:
1711 caps
1712
1713def caps.of.if(seed: Bool, +src: U32, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>) -> List<&2, Maybe<&2, U32>>:
1714 match seed:
1715 case True{}:
1716 init
1717 case False{}:
1718 caps.at(List.get(&2, Th, ths, U32.to_nat(src)), init)
1719
1720def caps.of(+src: U32, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>) -> List<&2, Maybe<&2, U32>>:
1721 caps.of.if(U32.is_eq(src, seed.id()), src, ths, init)
1722
1723def saves.put(xs: List<&2, U32>, caps: List<&2, Maybe<&2, U32>>, +pos: U32) -> List<&2, Maybe<&2, U32>>:
1724 match xs:
1725 case Nil{}:
1726 caps
1727 case Con{+k, t}:
1728 saves.put(t, List.set(&2, Maybe<&2, U32>, caps, U32.to_nat(k), Some{pos}), pos)
1729
1730def replay(xs: List<&2, Op>, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>, +pos: U32) -> List<&2, Th>:
1731 match xs:
1732 case Nil{}:
1733 Nil{}
1734 case Con{Op{+src, pc, saves}, t}:
1735 Th{pc, saves.put(saves, caps.of(src, ths, init), pos)} <> replay(t, ths, init, pos)
1736
1737def replay.best(none: Bool, +hit: U32, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Maybe<&2, List<&2, Maybe<&2, U32>>>:
1738 match none:
1739 case True{}:
1740 best
1741 case False{}:
1742 Some{caps.of((hit - 1 : U32), ths, init)}
1743
1744
1745def replay.fresh(skip: Bool, outs: List<&2, Op>, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>, +pos: U32) -> Vm:
1746 match skip:
1747 case True{}:
1748 Vm{Nil{}, None{}}
1749 case False{}:
1750 Vm{replay(outs, ths, init, pos), None{}}
1751
1752
1753def replay.vm(fresh: Bool, +hit: U32, outs: List<&2, Op>, st: Vm, +init: List<&2, Maybe<&2, U32>>, +pos: U32, +start: Maybe<&2, List<&2, Inst>>, +next: Maybe<&2, Char>) -> Vm:
1754 match fresh:
1755 case True{}:
1756 Vm{+ths, best} = st
1757 replay.fresh(seed.skip(Nil{}, None{}, start, next), outs, ths, init, pos)
1758 case False{}:
1759 Vm{+ths, best} = st
1760 Vm{replay(outs, ths, init, pos), replay.best(U32.is_eq(hit, 0), hit, ths, init, best)}
1761
1762
1763
1764type Rq is Type:
1765 Rq{a: Array<U32>, tab: Array<Tr>, keys: Trie<List<&2, Ix>>, n: U32, id: U32, i: U32, d: Dc, st: Vm, same: Bool}
1766
1767def rq.ik(ik: Ik, a: Array<U32>, tab: Array<Tr>, +j: U32, +d: Dc, st: Vm) -> Rq:
1768 Ik{keys, n, id} = ik
1769 Rq{a, tab, keys, n, id, j, d, st, False{}}
1770
1771def rq.of(r: Rb, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +cap: U32) -> Rq:
1772 Rb{a, +i, +d, +st} = r
1773 rq.ik(intern(keys, n, cap, vm.key(st)), a, tab, i, d, st)
1774
1775def rq.store(ik: Ik, a: Array<U32>, tab: Array<Tr>, +idx: U32, +old: U32, +hit: U32, +outs: List<&2, Op>, +fresh: Bool, +j: U32, +d: Dc, st: Vm, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>) -> Rq:
1776 Ik{keys, +n, +id} = ik
1777 Vm{+ths, +best} = st
1778 +same = U32.is_eq(id, old) && U32.is_eq(hit, 0) && ops.same(outs, ths, 0)
1779 Rq{a, Array.set(Tr, tab, idx, tr.of(same, id, hit, outs, fresh)), keys, n, id, j, d, replay.vm(fresh, hit, outs, Vm{ths, best}, init, j, start, Dc.char(d)), same}
1780
1781def rq.learn(lr: Lr, a: Array<U32>, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +idx: U32, +old: U32, +j: U32, +d: Dc, st: Vm, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +cap: U32) -> Rq:
1782 Lr{+hit, +outs, +key, +fresh} = lr
1783 rq.store(intern(keys, n, cap, key), a, tab, idx, old, hit, outs, fresh, j, d, st, init, start)
1784
1785
1786def rq.real(room: Bool, a: Array<U32>, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +j: U32, +d: Dc, +st: Vm, +cap: U32) -> Rq:
1787 match room:
1788 case True{}:
1789 rq.ik(intern(keys, n, cap, vm.key(st)), a, tab, j, d, st)
1790 case False{}:
1791 Rq{a, tab, keys, n, seed.id(), j, d, st, False{}}
1792
1793
1794
1795type Spin is Type:
1796 Spin{a: Array<U32>, tab: Array<Tr>, i: U32}
1797
1798type SpinStep is Type:
1799 SpinStep{a: Array<U32>, tab: Array<Tr>, i: U32, tr: Tr}
1800
1801def spin.byte(last: Bool, a: Array<U32>, +i: U32) -> Array<U32> & U32:
1802 match last:
1803 case True{}:
1804 (a, 128)
1805 case False{}:
1806 Bytes.peek(a, i)
1807
1808def spin.tr(ascii: Bool, tab: Array<Tr>, +id: U32, +c: U32) -> Array<Tr> & Tr:
1809 match ascii:
1810 case True{}:
1811 Array.get(Tr, tab, ((id * 128) + c : U32))
1812 case False{}:
1813 (tab, TrNo{})
1814
1815def spin.state.tr(r: Array<Tr> & Tr, a: Array<U32>, +i: U32) -> SpinStep:
1816 (tab, tr) = r
1817 SpinStep{a, tab, i, tr}
1818
1819def spin.state(r: Array<U32> & U32, tab: Array<Tr>, +i: U32, +id: U32, +cap: U32) -> SpinStep:
1820 (a, +c) = r
1821 spin.state.tr(spin.tr(U32.is_lt(c, 128) && U32.is_lt(id, cap), tab, id, c), a, i)
1822
1823def spin(fuel: Nat, s: SpinStep, +len: U32, +id: U32, +cap: U32) -> Spin:
1824 match fuel:
1825 case 0n:
1826 SpinStep{a, tab, i, tr} = s
1827 Spin{a, tab, i}
1828 case 1n+f:
1829 SpinStep{a, tab, +i, tr} = s
1830 match tr:
1831 case TrSame{}:
1832 +j = (i + 1 : U32)
1833 spin(f, spin.state(spin.byte(Bool.not(U32.is_lt((j + 1 : U32), len)), a, j), tab, j, id, cap), len, id, cap)
1834 case TrNo{}:
1835 Spin{a, tab, i}
1836 case Tr{next, hit, outs, fresh}:
1837 Spin{a, tab, i}
1838
1839
1840type Ar is Type:
1841 Ar{old: Array<Th>, spare: Array<Th>, count: U32, cap: U32, best: Maybe<&2, List<&2, Maybe<&2, U32>>>}
1842
1843def ar.fill(xs: List<&2, Th>, a: Array<Th>, +i: U32) -> Array<Th>:
1844 match xs:
1845 case Nil{}:
1846 a
1847 case Con{th, rest}:
1848 ar.fill(rest, Array.set(Th, a, i, th), (i + 1 : U32))
1849
1850def ar.reset.size(fits: Bool, ths: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>, old: Array<Th>, spare: Array<Th>, +count: U32, +cap: U32, +init: List<&2, Maybe<&2, U32>>) -> Ar:
1851 match fits:
1852 case True{}:
1853 Ar{ar.fill(ths, old, 0), spare, count, cap, best}
1854 case False{}:
1855 +depth = Nat.add(U32.log2(count), 1n)
1856 Ar{ar.fill(ths, Array.new(Th, depth, Th{0, init}), 0), Array.new(Th, depth, Th{0, init}), count, U32.shln(1, depth), best}
1857
1858def ar.reset.put(vm: Vm, old: Array<Th>, spare: Array<Th>, +cap: U32, +init: List<&2, Maybe<&2, U32>>) -> Ar:
1859 Vm{+ths, best} = vm
1860 +count = U32.from_nat(List.length(&2, Th, ths))
1861 ar.reset.size(U32.is_le(count, cap), ths, best, old, spare, count, cap, init)
1862
1863def ar.reset(vm: Vm, ar: Ar, +init: List<&2, Maybe<&2, U32>>) -> Ar:
1864 Ar{old, spare, count, cap, best} = ar
1865 ar.reset.put(vm, old, spare, cap, init)
1866
1867def ar.new(vm: Vm, +init: List<&2, Maybe<&2, U32>>) -> Ar:
1868 ar.reset(vm, Ar{Array.new(Th, 2n, Th{0, init}), Array.new(Th, 2n, Th{0, init}), 0, 4, None{}}, init)
1869
1870def ar.list.go(fuel: Nat, r: Array<Th> & Th, +i: U32, acc: List<&2, Th>) -> Array<Th> & List<&2, Th>:
1871 match fuel:
1872 case 0n:
1873 (a, th) = r
1874 (a, acc)
1875 case 1n+f:
1876 (a, th) = r
1877 ar.list.go(f, Array.get(Th, a, (i - 1 : U32)), (i - 1 : U32), th <> acc)
1878
1879def ar.vm.put(r: Array<Th> & List<&2, Th>, spare: Array<Th>, +count: U32, +cap: U32, +best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Ar & Vm:
1880 (old, ths) = r
1881 (Ar{old, spare, count, cap, best}, Vm{ths, best})
1882
1883def ar.vm(ar: Ar) -> Ar & Vm:
1884 Ar{old, spare, +count, +cap, +best} = ar
1885 ar.vm.put(ar.list.go(U32.to_nat(count), Array.get(Th, old, (count - 1 : U32)), (count - 1 : U32), Nil{}), spare, count, cap, best)
1886
1887def ar.src.get(r: Array<Th> & Th) -> Array<Th> & List<&2, Maybe<&2, U32>>:
1888 (old, Th{pc, caps}) = r
1889 (old, caps)
1890
1891def ar.src(seed: Bool, old: Array<Th>, +src: U32, +init: List<&2, Maybe<&2, U32>>) -> Array<Th> & List<&2, Maybe<&2, U32>>:
1892 match seed:
1893 case True{}:
1894 (old, init)
1895 case False{}:
1896 ar.src.get(Array.get(Th, old, src))
1897
1898def ar.put(r: Array<Th> & List<&2, Maybe<&2, U32>>, spare: Array<Th>, +pc: U32, saves: List<&2, U32>, +pos: U32, +i: U32) -> Array<Th> & Array<Th>:
1899 (old, caps) = r
1900 (old, Array.set(Th, spare, i, Th{pc, saves.put(saves, caps, pos)}))
1901
1902def ar.replay(xs: List<&2, Op>, r: Array<Th> & Array<Th>, +init: List<&2, Maybe<&2, U32>>, +pos: U32, +i: U32, +cap: U32, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Ar:
1903 match xs:
1904 case Nil{}:
1905 (old, spare) = r
1906 Ar{spare, old, i, cap, best}
1907 case Con{Op{+src, +pc, saves}, rest}:
1908 (old, spare) = r
1909 ar.replay(rest, ar.put(ar.src(U32.is_eq(src, seed.id()), old, src, init), spare, pc, saves, pos, i), init, pos, (i + 1 : U32), cap, best)
1910
1911def ar.best.get(r: Array<Th> & List<&2, Maybe<&2, U32>>) -> Array<Th> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1912 (old, caps) = r
1913 (old, Some{caps})
1914
1915def ar.best.none(no_hit: Bool, old: Array<Th>, +hit: U32, +init: List<&2, Maybe<&2, U32>>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Array<Th> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1916 match no_hit:
1917 case True{}:
1918 (old, best)
1919 case False{}:
1920 ar.best.get(ar.src(U32.is_eq((hit - 1 : U32), seed.id()), old, (hit - 1 : U32), init))
1921
1922def ar.replay.best(r: Array<Th> & Maybe<&2, List<&2, Maybe<&2, U32>>>, spare: Array<Th>, outs: List<&2, Op>, +cap: U32, +init: List<&2, Maybe<&2, U32>>, +pos: U32) -> Ar:
1923 (old, best) = r
1924 ar.replay(outs, (old, spare), init, pos, 0, cap, best)
1925
1926def ar.cached.fresh(skip: Bool, ar: Ar, outs: List<&2, Op>, +init: List<&2, Maybe<&2, U32>>, +pos: U32) -> Ar:
1927 match skip:
1928 case True{}:
1929 Ar{old, spare, size, +cap, best} = ar
1930 Ar{old, spare, 0, cap, None{}}
1931 case False{}:
1932 Ar{old, spare, size, +cap, best} = ar
1933 ar.replay.best((old, None{}), spare, outs, cap, init, pos)
1934
1935
1936def ar.cached(fresh: Bool, +hit: U32, outs: List<&2, Op>, ar: Ar, +init: List<&2, Maybe<&2, U32>>, +pos: U32, +start: Maybe<&2, List<&2, Inst>>, +next: Maybe<&2, Char>) -> Ar:
1937 match fresh:
1938 case True{}:
1939 ar.cached.fresh(seed.skip(Nil{}, None{}, start, next), ar, outs, init, pos)
1940 case False{}:
1941 Ar{old, spare, size, +cap, best} = ar
1942 ar.replay.best(ar.best.none(U32.is_eq(hit, 0), old, hit, init, best), spare, outs, cap, init, pos)
1943
1944type Qst is Type:
1945 QDone{best: List<&2, Maybe<&2, U32>>}
1946 QIdle{ar: Ar}
1947 QLive{ar: Ar}
1948 QPlain{st: Vm}
1949
1950def qa.status.if(zero: Bool, old: Array<Th>, spare: Array<Th>, +count: U32, +cap: U32, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Qst:
1951 match zero:
1952 case False{}:
1953 QLive{Ar{old, spare, count, cap, best}}
1954 case True{}:
1955 match best:
1956 case Some{caps}:
1957 QDone{caps}
1958 case None{}:
1959 QIdle{Ar{old, spare, count, cap, None{}}}
1960
1961def qa.status(ar: Ar) -> Qst:
1962 Ar{old, spare, +count, +cap, best} = ar
1963 qa.status.if(U32.is_zero(count), old, spare, count, cap, best)
1964
1965type Qa is Type:
1966 Qa{a: Array<U32>, tab: Array<Tr>, keys: Trie<List<&2, Ix>>, n: U32, id: U32, i: U32, d: Dc, ar: Qst, same: Bool}
1967
1968def qa.seed(r: Rq, +init: List<&2, Maybe<&2, U32>>) -> Qa:
1969 Rq{a, tab, keys, n, id, i, d, st, same} = r
1970 Qa{a, tab, keys, n, id, i, d, qa.status(ar.new(st, init)), same}
1971
1972def qa.from.state(cached: Bool, st: Vm, ar: Ar, +init: List<&2, Maybe<&2, U32>>) -> Qst:
1973 match cached:
1974 case True{}:
1975 qa.status(ar.reset(st, ar, init))
1976 case False{}:
1977 QPlain{st}
1978
1979def qa.from(r: Rq, ar: Ar, +init: List<&2, Maybe<&2, U32>>, +cap: U32) -> Qa:
1980 Rq{a, tab, keys, n, +id, i, d, st, same} = r
1981 Qa{a, tab, keys, n, id, i, d, qa.from.state(U32.is_lt(id, cap), st, ar, init), same}
1982
1983def qa.learn.vm(r: Ar & Vm, a: Array<U32>, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +idx: U32, +j: U32, +d: Dc, +c: U32, +prog: Trie<Inst>, +cfuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool, +slots: Nat, +cap: U32) -> Qa:
1984 (ar, +st) = r
1985 qa.from(rq.learn(learn(st, c, prog, cfuel, slots, any), a, tab, keys, n, idx, (idx / 128 : U32), j, d, st, init, start, cap), ar, init, cap)
1986
1987def qa.real.vm(r: Ar & Vm, s: Array<U32> & Dc, +j: U32, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +c: U32, +prog: Trie<Inst>, +cfuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool, +cap: U32) -> Qa:
1988 (ar, st) = r
1989 (a, +d) = s
1990 qa.from(rq.real(U32.is_lt(n, cap), a, tab, keys, n, j, d, run.step(st, prog, cfuel, init, start, any, j, Chr{c}, Dc.char(d)), cap), ar, init, cap)
1991
1992def qa.real(s: Array<U32> & Dc, +j: U32, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, ar: Ar, +c: U32, +prog: Trie<Inst>, +cfuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool, +cap: U32) -> Qa:
1993 qa.real.vm(ar.vm(ar), s, j, tab, keys, n, c, prog, cfuel, init, start, any, cap)
1994
1995def qa.cached(r: Array<Tr> & Tr, a: Array<U32>, +keys: Trie<List<&2, Ix>>, +n: U32, +idx: U32, +j: U32, +d: Dc, ar: Ar, +c: U32, +prog: Trie<Inst>, +cfuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool, +slots: Nat, +cap: U32) -> Qa:
1996 (tab, tr) = r
1997 match tr:
1998 case TrNo{}:
1999 qa.learn.vm(ar.vm(ar), a, tab, keys, n, idx, j, d, c, prog, cfuel, init, start, any, slots, cap)
2000 case TrSame{}:
2001 Qa{a, tab, keys, n, (idx / 128 : U32), j, d, qa.status(ar), True{}}
2002 case Tr{+next, +hit, +outs, +fresh}:
2003 Qa{a, tab, keys, n, next, j, d, qa.status(ar.cached(fresh, hit, outs, ar, init, j, start, Dc.char(d))), False{}}
2004
2005def qa.pick(ok: Bool, a: Array<U32>, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +id: U32, +j: U32, +d: Dc, ar: Ar, +c: U32, +prog: Trie<Inst>, +cfuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool, +slots: Nat, +cap: U32) -> Qa:
2006 match ok:
2007 case True{}:
2008 +idx = ((id * 128) + c : U32)
2009 qa.cached(Array.get(Tr, tab, idx), a, keys, n, idx, j, d, ar, c, prog, cfuel, init, start, any, slots, cap)
2010 case False{}:
2011 qa.real((a, d), j, tab, keys, n, ar, c, prog, cfuel, init, start, any, cap)
2012
2013def qa.step(s: Array<U32> & Dc, +j: U32, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +id: U32, ar: Ar, +c: U32, +prog: Trie<Inst>, +cfuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +any: Bool, +slots: Nat, +cap: U32) -> Qa:
2014 (a, +d) = s
2015 qa.pick(U32.is_lt(c, 128) && U32.is_lt(id, cap) && Maybe.is_some(&2, Char, Dc.char(d)), a, tab, keys, n, id, j, d, ar, c, prog, cfuel, init, start, any, slots, cap)
2016
2017def qa.spin.read(s: Array<U32> & Dc, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +id: U32, +i: U32, ar: Qst) -> Qa:
2018 (a, d) = s
2019 Qa{a, tab, keys, n, id, i, d, ar, False{}}
2020
2021def qa.spin.dec(moved: Bool, a: Array<U32>, tab: Array<Tr>, +len: U32, +keys: Trie<List<&2, Ix>>, +n: U32, +id: U32, +i: U32, d: Dc, ar: Qst) -> Qa:
2022 match moved:
2023 case True{}:
2024 qa.spin.read(dec(a, len, i), tab, keys, n, id, i, ar)
2025 case False{}:
2026 Qa{a, tab, keys, n, id, i, d, ar, False{}}
2027
2028def qa.spin.at(s: Spin, +old: U32, +len: U32, +keys: Trie<List<&2, Ix>>, +n: U32, +id: U32, d: Dc, ar: Qst) -> Qa:
2029 Spin{a, tab, +i} = s
2030 qa.spin.dec(U32.is_ne(i, old), a, tab, len, keys, n, id, i, d, ar)
2031
2032def qa.spin.if(same: Bool, a: Array<U32>, tab: Array<Tr>, +keys: Trie<List<&2, Ix>>, +n: U32, +id: U32, +i: U32, d: Dc, ar: Qst, +fuel: Nat, +len: U32, +cap: U32) -> Qa:
2033 match same:
2034 case True{}:
2035 qa.spin.at(spin(fuel, spin.state(spin.byte(Bool.not(U32.is_lt((i + 1 : U32), len)), a, i), tab, i, id, cap), len, id, cap), i, len, keys, n, id, d, ar)
2036 case False{}:
2037 Qa{a, tab, keys, n, id, i, d, ar, False{}}
2038
2039def qa.spin(r: Qa, +fuel: Nat, +len: U32, +cap: U32) -> Qa:
2040 Qa{a, tab, keys, n, +id, +i, d, ar, same} = r
2041 qa.spin.if(same, a, tab, keys, n, id, i, d, ar, fuel, len, cap)
2042
2043def qa.end.vm(st: Vm, a: Array<U32>, +prog: Trie<Inst>, +any: Bool) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2044 Vm{ths, best} = st
2045 (a, run.end(scan(ths, prog, None{}, any, Sc{Nil{}, best, False{}})))
2046
2047def qa.end(r: Ar & Vm, a: Array<U32>, +prog: Trie<Inst>, +any: Bool) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2048 (ar, st) = r
2049 qa.end.vm(st, a, prog, any)
2050
2051def qa.end.status(st: Qst, a: Array<U32>, +prog: Trie<Inst>, +any: Bool) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2052 match st:
2053 case QDone{best}:
2054 (a, Some{best})
2055 case QIdle{ar}:
2056 qa.end(ar.vm(ar), a, prog, any)
2057 case QLive{ar}:
2058 qa.end(ar.vm(ar), a, prog, any)
2059 case QPlain{st}:
2060 qa.end.vm(st, a, prog, any)
2061
2062
2063def runqa(+fuel: Nat, r: Qa, +len: U32, +prog: Trie<Inst>, +cfuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat, +cap: U32) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2064 match fuel:
2065 case 0n:
2066 Qa{a, tab, keys, n, id, i, d, ar, same} = r
2067 (a, None{})
2068 case 1n+f:
2069 Qa{a, tab, +keys, +n, +id, +i, d, ar, same} = r
2070 match d:
2071 case DEnd{}:
2072 qa.end.status(ar, a, prog, any)
2073 case Dc{+c, +w}:
2074 match ar:
2075 case QDone{best}:
2076 (a, Some{best})
2077 case QIdle{ar}:
2078 runqa(f, qa.from(rq.of(rb.idle(asc, a, len, (i + w : U32), c, prog, cfuel, init, start, any), tab, keys, n, cap), ar, init, cap), len, prog, cfuel, init, start, asc, any, slots, cap)
2079 case QLive{ar}:
2080 +j = (i + w : U32)
2081 runqa(f, qa.spin(qa.step(dec(a, len, j), j, tab, keys, n, id, ar, c, prog, cfuel, init, start, any, slots, cap), f, len, cap), len, prog, cfuel, init, start, asc, any, slots, cap)
2082 case QPlain{st}:
2083 runb(Nat.add(f, 1n), Rb{a, i, Dc{c, w}, st}, len, prog, cfuel, init, start, asc, any)
2084
2085def exec.bytes.fin(+len: U32, r: Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2086 (a, m) = r
2087 (Bytes.Bytes{len, a}, m)
2088
2089
2090def exec.bytes.go.if(use: Bool, +len: U32, +from: U32, buf: Array<U32>, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2091 match use:
2092 case True{}:
2093 +small = U32.is_lt(len, 4096)
2094 +wide = Nat.is_ge(fuel, 300n)
2095 +cap = Bool.pick(U32, small, 8, Bool.pick(U32, wide, 2048, 256))
2096 runqa(Nat.add(U32.to_nat((len - from : U32)), 2n), qa.seed(rq.of(rb.seed(dec(buf, len, from), from, prog, fuel, init, start), Array.new(Tr, Bool.pick(Nat, small, 10n, Bool.pick(Nat, wide, 18n, 15n)), TrNo{}), TTip{}, 0, cap), init), len, prog, fuel, init, start, asc, any, slots, cap)
2097 case False{}:
2098 runb(Nat.add(U32.to_nat((len - from : U32)), 2n), rb.seed(dec(buf, len, from), from, prog, fuel, init, start), len, prog, fuel, init, start, asc, any)
2099
2100def exec.bytes.go(plain: Bool, +len: U32, +from: U32, buf: Array<U32>, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2101 exec.bytes.go.if(plain && (U32.is_le(4096, len) || Bool.not(Nat.is_ge(fuel, 300n))), len, from, buf, prog, fuel, init, start, asc, any, slots)
2102
2103def exec.bytes.run(b: Bytes.Bytes, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2104 Bytes.Bytes{+len, buf} = b
2105 exec.bytes.fin(len, exec.bytes.go(plain, len, 0, buf, prog, fuel, init, start, asc, any, slots))
2106
2107
2108def rev.best(hit: Bool, +i: U32, prev: Maybe<&2, U32>) -> Maybe<&2, U32>:
2109 match hit:
2110 case True{}:
2111 Some{i}
2112 case False{}:
2113 prev
2114
2115
2116type Rv is Type:
2117 Rv{a: Array<U32>, best: Maybe<&2, U32>, ascii: Bool}
2118
2119type RevBits is Type:
2120 RevBits{running: Bool, a: Array<U32>, mask: U32, best: Maybe<&2, U32>, ascii: Bool}
2121
2122def rev.bits.after(step: Bs, a: Array<U32>, best: Maybe<&2, U32>, +i: U32) -> RevBits:
2123 Bs{+next, fin, end} = step
2124 RevBits{U32.is_ne(next, 0), a, next, rev.best(fin, i, best), True{}}
2125
2126def rev.bits.char(valid: Bool, a: Array<U32>, +mask: U32, best: Maybe<&2, U32>, +c: U32, +i: U32, +sets: List<&2, Bit>) -> RevBits:
2127 match valid:
2128 case False{}:
2129 RevBits{False{}, a, mask, best, False{}}
2130 case True{}:
2131 rev.bits.after(bits.step(sets, mask, c, Bs{0, False{}, False{}}), a, best, i)
2132
2133def rev.bits.read(r: Array<U32> & U32, +mask: U32, best: Maybe<&2, U32>, +i: U32, +sets: List<&2, Bit>) -> RevBits:
2134 (a, +c) = r
2135 rev.bits.char(U32.is_lt(c, 128), a, mask, best, c, i, sets)
2136
2137def rev.bits.walk(fuel: Nat, r: RevBits, +i: U32, +sets: List<&2, Bit>) -> RevBits:
2138 match fuel:
2139 case 0n:
2140 r
2141 case 1n+f:
2142 RevBits{running, a, +mask, best, ascii} = r
2143 match running:
2144 case False{}:
2145 RevBits{False{}, a, mask, best, ascii}
2146 case True{}:
2147 rev.bits.walk(f, rev.bits.read(Bytes.peek(a, (i - 1 : U32)), mask, best, (i - 1 : U32), sets), (i - 1 : U32), sets)
2148
2149def rev.bits.result(done: Bool, r: RevBits) -> Rv:
2150 RevBits{running, a, mask, best, ascii} = r
2151 Rv{a, best, ascii && (done || U32.is_eq(mask, 0))}
2152
2153def rev.bits.run(a: Array<U32>, +end: U32, bits: Bits) -> Rv:
2154 Bits{+sets, +at0, hit0, hit01, atn, hit1} = bits
2155 +limit = Bool.pick(U32, U32.is_lt(end, 4096), end, 4096)
2156 rev.bits.result(U32.is_le(end, 4096), rev.bits.walk(U32.to_nat(limit), RevBits{True{}, a, at0, None{}, True{}}, end, sets))
2157
2158
2159type RevPhase is Type:
2160 Seek{hit: Maybe<&2, U32>, b: Bytes.Bytes, best: Maybe<&2, U32>}
2161 Check{run: Rv, len: U32, at: U32, best: Maybe<&2, U32>}
2162
2163type RevFound is Type:
2164 RevFound{b: Bytes.Bytes, best: Maybe<&2, U32>, safe: Bool}
2165
2166def rev.min(m: Maybe<&2, U32>, prev: Maybe<&2, U32>) -> Maybe<&2, U32>:
2167 match m:
2168 case None{}:
2169 prev
2170 case Some{+i}:
2171 match prev:
2172 case None{}:
2173 Some{i}
2174 case Some{+j}:
2175 Some{Bool.pick(U32, U32.is_lt(i, j), i, j)}
2176
2177def rev.seek(r: Bytes.Bytes & Maybe<&2, U32>, best: Maybe<&2, U32>) -> RevPhase:
2178 (b, hit) = r
2179 Seek{hit, b, best}
2180
2181def rev.abort(r: RevPhase) -> RevFound:
2182 match r:
2183 case Seek{hit, b, best}:
2184 RevFound{b, best, False{}}
2185 case Check{Rv{a, found, ascii}, len, at, best}:
2186 RevFound{Bytes.Bytes{len, a}, best, False{}}
2187
2188def rev.candidates(fuel: Nat, r: RevPhase, +needle: String, +bits: Bits) -> RevFound:
2189 match fuel:
2190 case 0n:
2191 rev.abort(r)
2192 case 1n+f:
2193 match r:
2194 case Seek{hit, b, best}:
2195 match hit:
2196 case None{}:
2197 RevFound{b, best, True{}}
2198 case Some{+i}:
2199 Bytes.Bytes{+len, a} = b
2200 rev.candidates(f, Check{rev.bits.run(a, (i + 1 : U32), bits), len, i, best}, needle, bits)
2201 case Check{Rv{a, found, ascii}, +len, +at, best}:
2202 match ascii:
2203 case False{}:
2204 RevFound{Bytes.Bytes{len, a}, best, False{}}
2205 case True{}:
2206 rev.candidates(f, rev.seek(Bytes.find.from(Bytes.Bytes{len, a}, needle, (at + 1 : U32)), rev.min(found, best)), needle, bits)
2207
2208def exec.bytes.at(b: Bytes.Bytes, +k: U32, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2209 Bytes.Bytes{+len, buf} = b
2210 exec.bytes.fin(len, exec.bytes.go(plain, len, k, buf, prog, fuel, init, start, asc, any, slots))
2211
2212def rev.confirm.best(best: Maybe<&2, U32>, b: Bytes.Bytes, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2213 match best:
2214 case None{}:
2215 (b, None{})
2216 case Some{k}:
2217 exec.bytes.at(b, k, plain, prog, fuel, init, start, asc, any, slots)
2218
2219
2220def rev.confirm(r: RevFound, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2221 RevFound{b, best, safe} = r
2222 match safe:
2223 case False{}:
2224 exec.bytes.run(b, plain, prog, fuel, init, start, asc, any, slots)
2225 case True{}:
2226 rev.confirm.best(best, b, plain, prog, fuel, init, start, asc, any, slots)
2227
2228def exec.bytes.candidate(r: Bytes.Bytes & Maybe<&2, U32>, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2229 (b, hit) = r
2230 match hit:
2231 case None{}:
2232 (b, None{})
2233 case Some{i}:
2234 exec.bytes.run(b, plain, prog, fuel, init, start, asc, any, slots)
2235
2236def exec.bytes.reverse(r: Bytes.Bytes & Maybe<&2, U32>, bits: Bits, +needle: String, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2237 (b, hit) = r
2238 rev.confirm(rev.candidates(16n, Seek{hit, b, None{}}, needle, bits), plain, prog, fuel, init, start, asc, any, slots)
2239
2240def exec.bytes.select(rev: Maybe<&2, Bits>, r: Bytes.Bytes & Maybe<&2, U32>, +needle: String, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2241 match rev:
2242 case None{}:
2243 exec.bytes.candidate(r, plain, prog, fuel, init, start, asc, any, slots)
2244 case Some{x}:
2245 exec.bytes.reverse(r, x, needle, plain, prog, fuel, init, start, asc, any, slots)
2246
2247
2248def exec.bytes.must.hit(b: Bytes.Bytes, rev: Maybe<&2, Bits>, +c: U32, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2249 +needle = {SCon{Chr{c}, SNil{}} : String}
2250 exec.bytes.select(rev, Bytes.find(b, needle), needle, plain, prog, fuel, init, start, asc, any, slots)
2251
2252def exec.bytes.must(m: Maybe<&2, U32>, rev: Maybe<&2, Bits>, b: Bytes.Bytes, +plain: Bool, +prog: Trie<Inst>, +fuel: Nat, +init: List<&2, Maybe<&2, U32>>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +any: Bool, +slots: Nat) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2253 match m:
2254 case None{}:
2255 exec.bytes.run(b, plain, prog, fuel, init, start, asc, any, slots)
2256 case Some{c}:
2257 exec.bytes.must.hit(b, rev, c, plain, prog, fuel, init, start, asc, any, slots)
2258
2259def exec.bytes(re: Regex, b: Bytes.Bytes, +any: Bool) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
2260 Regex{+prog, +fuel, +slots, +start, bits, +asc, plain, must, reverse} = re
2261 +sl = Bool.pick(Nat, any, 0n, slots)
2262 exec.bytes.must(must, reverse, b, plain, prog, fuel, List.replicate(Maybe<&2, U32>, sl, None{}), start, asc, any, sl)
2263
2264def find.bytes.fin(r: Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, Span>>>:
2265 (b, m) = r
2266 (b, find.spans(m))
2267
2268
2269def find.bytes(re: Regex, b: Bytes.Bytes) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, Span>>>:
2270 find.bytes.fin(exec.bytes(re, b, False{}))
2271
2272def is_match.bytes.fin(r: Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Bytes.Bytes & Bool:
2273 (b, m) = r
2274 (b, Maybe.is_some(&2, List<&2, Maybe<&2, U32>>, m))
2275
2276def is_match.bytes.vm(re: Regex, b: Bytes.Bytes) -> Bytes.Bytes & Bool:
2277 is_match.bytes.fin(exec.bytes(re, b, True{}))
2278
2279
2280type Rt is Type:
2281 Rt{a: Array<U32>, i: U32, d: Dc, st: Bs}
2282
2283def rt.at(r: Array<U32> & Dc, +j: U32, st: Bs) -> Rt:
2284 (a, +d) = r
2285 Rt{a, j, d, st}
2286
2287def rt.skip(r: Array<U32> & U32, +len: U32, +atn: U32, +hit1: Bool) -> Rt:
2288 (a, +k) = r
2289 rt.at(dec(a, len, k), k, Bs{atn, False{}, hit1})
2290
2291
2292def rt.next(idle: Bool, asc: Maybe<&2, Asc>, a: Array<U32>, +len: U32, +j: U32, +sets: List<&2, Bit>, +atn: U32, +hit1: Bool, +cur: U32, +c: U32) -> Rt:
2293 match idle:
2294 case True{}:
2295 match asc:
2296 case None{}:
2297 rt.at(dec(a, len, j), j, Bs{atn, False{}, hit1})
2298 case Some{+m}:
2299 rt.skip(skip.from(a, len, j, m), len, atn, hit1)
2300 case False{}:
2301 rt.at(dec(a, len, j), j, bits.step(sets, cur, c, Bs{atn, False{}, hit1}))
2302
2303def bitsb(fuel: Nat, r: Rt, +len: U32, +sets: List<&2, Bit>, +start: Maybe<&2, List<&2, Inst>>, +asc: Maybe<&2, Asc>, +atn: U32, +hit1: Bool) -> Array<U32> & Bool:
2304 match fuel:
2305 case 0n:
2306 Rt{a, i, d, st} = r
2307 (a, False{})
2308 case 1n+f:
2309 Rt{a, +i, d, st} = r
2310 match d:
2311 case DEnd{}:
2312 Bs{cur, done, ok} = st
2313 (a, done || ok)
2314 case Dc{+c, +w}:
2315 match st:
2316 case Bs{cur, True{}, ok}:
2317 (a, True{})
2318 case Bs{+cur, False{}, ok}:
2319 bitsb(f, rt.next(bits.idle(start, cur, atn, c), asc, a, len, (i + w : U32), sets, atn, hit1, cur, c), len, sets, start, asc, atn, hit1)
2320
2321def bits.bytes.fin(+len: U32, r: Array<U32> & Bool) -> Bytes.Bytes & Maybe<&2, Bool>:
2322 (a, x) = r
2323 (Bytes.Bytes{len, a}, Some{x})
2324
2325def bits.bytes(b: Bits, start: Maybe<&2, List<&2, Inst>>, asc: Maybe<&2, Asc>, +len: U32, buf: Array<U32>) -> Bytes.Bytes & Maybe<&2, Bool>:
2326 Bits{sets, at0, hit0, hit01, atn, hit1} = b
2327 bits.bytes.fin(len, bitsb(Nat.add(U32.to_nat(len), 2n), rt.at(dec(buf, len, 0), 0, Bs{at0, hit0, hit01}), len, sets, start, asc, atn, hit1))
2328
2329def bits.bytes.if(m: Maybe<&2, Bits>, start: Maybe<&2, List<&2, Inst>>, asc: Maybe<&2, Asc>, b: Bytes.Bytes) -> Bytes.Bytes & Maybe<&2, Bool>:
2330 match m:
2331 case None{}:
2332 (b, None{})
2333 case Some{x}:
2334 Bytes.Bytes{+len, buf} = b
2335 bits.bytes(x, start, asc, len, buf)
2336
2337
2338def is_match.bytes.bits(re: Regex, b: Bytes.Bytes) -> Bytes.Bytes & Maybe<&2, Bool>:
2339 Regex{prog, fuel, slots, start, bt, asc, plain, must, reverse} = re
2340 bits.bytes.if(bt, start, asc, b)
2341
2342def is_match.bytes.pick(r: Bytes.Bytes & Maybe<&2, Bool>, re: Regex) -> Bytes.Bytes & Bool:
2343 (b, m) = r
2344 match m:
2345 case Some{x}:
2346 (b, x)
2347 case None{}:
2348 is_match.bytes.vm(re, b)
2349
2350
2351def is_match.bytes(+re: Regex, b: Bytes.Bytes) -> Bytes.Bytes & Bool:
2352 is_match.bytes.pick(is_match.bytes.bits(re, b), re)