regex.bend

bend-kit-regex@0.6.0.2 · 2,070 lines · 0 definitions

1# Linear-time regular expressions: RE2 syntax, Pike VM, capture groups. Source: https://github.com/paymog/bend-kit/tree/main/regex
2import Base
3import bend-kit-unicode@0.1.0.0/unicode.bend as U
4import bend-kit-bytes@0.3.0.0/bytes.bend as Bytes
5
6# Positions count code points of the String, not octets.
7# Leftmost-first semantics, as RE2 and Perl: the first alternative that matches wins.
8
9# Syntax
10# ------
11
12# A set member: a code point range, or a Unicode general category ("L", "Lu", ...).
13type Item is Data:
14  Rng{lo: U32, hi: U32}
15  Prop{neg: Bool, name: String}
16
17# Assertion kinds: 0 start of text, 1 end of text, 2 word boundary, 3 not a word boundary.
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# \d \w \s are ASCII, as in RE2.
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# Escapes
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# \pL or \p{Lu}; \P negates.
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# An escaped letter or digit with no meaning is an error, as in RE2.
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# The text after a backslash.
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# Classes
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# c is one member; a "-" and a code point after it make a range.
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# A "]" right after "[" or "[^" is a member.
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# fuel: every step eats at least one char.
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# Lexer
242# -----
243
244type Lx is Data:
245  LGo{s: String, toks: List<&2, Tok>}
246  LDone{toks: List<&2, Tok>}
247  LFail{}
248
249# A run of decimal digits: its value (capped at 100000), its length, and the rest.
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# A trailing "?" makes a repetition lazy.
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# A "{" that does not start {n}, {n,} or {n,m} is a literal, as in RE2.
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# fuel: every step but the last eats at least one char.
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# Parser
393# ------
394
395# An open group: its capture index (None for (?:...)), and the enclosing alternatives and sequence.
396type Frame is Data:
397  Frame{cap: Maybe<&2, U32>, alts: List<&2, Node>, cur: List<&2, Node>}
398
399# n: the next capture index. rep: the last token was a repetition. alts and cur are reversed.
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# x* is (x+)?, so an empty x cannot loop; x{n,} is n-1 copies then x+; x{n,m} is n copies then (x(x...)?)?, as RE2 builds them.
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# Counts go up to 1000, and a repetition cannot repeat, as in RE2.
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# Compiler
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
541def size(n: Node) -> U32:
542  match n:
543    case NEmpty{}:
544      0
545    case NSet{neg, items}:
546      1
547    case NAssert{k}:
548      1
549    case NCat{a, b}:
550      (size(a) + size(b) : U32)
551    case NAlt{a, b}:
552      (2 + size(a) + size(b) : U32)
553    case NPlus{g, a}:
554      (1 + size(a) : U32)
555    case NQuest{g, a}:
556      (1 + size(a) : U32)
557    case NGroup{i, a}:
558      (2 + size(a) : U32)
559
560# The instructions of n, placed at pc, in front of rest. ISplit tries x first.
561def emit(n: Node, +pc: U32, rest: List<&2, Inst>) -> List<&2, Inst>:
562  match n:
563    case NEmpty{}:
564      rest
565    case NSet{neg, items}:
566      ISet{neg, items} <> rest
567    case NAssert{k}:
568      IAssert{k} <> rest
569    case NCat{+a, b}:
570      emit(a, pc, emit(b, (pc + size(a) : U32), rest))
571    case NAlt{+a, +b}:
572      +j = (pc + 1 + size(a) : U32)
573      ISplit{(pc + 1 : U32), (j + 1 : U32)} <> emit(a, (pc + 1 : U32), IJmp{(j + 1 + size(b) : U32)} <> emit(b, (j + 1 : U32), rest))
574    case NPlus{+g, +a}:
575      +out = (pc + 1 + size(a) : U32)
576      emit(a, pc, ISplit{Bool.pick(U32, g, pc, out), Bool.pick(U32, g, out, pc)} <> rest)
577    case NQuest{+g, +a}:
578      +out = (pc + 1 + size(a) : U32)
579      ISplit{Bool.pick(U32, g, (pc + 1 : U32), out), Bool.pick(U32, g, out, (pc + 1 : U32))} <> emit(a, (pc + 1 : U32), rest)
580    case NGroup{+i, a}:
581      ISave{(2 * i : U32)} <> emit(a, (pc + 1 : U32), ISave{(2 * i + 1 : U32)} <> rest)
582
583# A binary trie keyed by n >= 1: the path is the bits of n below its top bit, low bit
584# first, so key n costs log2(n) steps and small keys stay near the root.
585type Trie<-V: Data> is Data:
586  TTip{}
587  TNode{val: Maybe<&2, V>, lo: Trie<V>, hi: Trie<V>}
588
589# here: n is 1. left: n is even.
590def trie.get(-V: Data, t: Trie<V>, here: Bool, left: Bool, +n: U32) -> Maybe<&2, V>:
591  match t:
592    case TTip{}:
593      None{}
594    case TNode{v, lo, hi}:
595      match here:
596        case True{}:
597          v
598        case False{}:
599          match left:
600            case True{}:
601              trie.get(V, lo, U32.is_eq(U32.shr(n), 1), U32.is_even(U32.shr(n)), U32.shr(n))
602            case False{}:
603              trie.get(V, hi, U32.is_eq(U32.shr(n), 1), U32.is_even(U32.shr(n)), U32.shr(n))
604
605# fuel: a U32 key has at most 32 bits.
606def trie.put(-V: Data, fuel: Nat, t: Trie<V>, here: Bool, left: Bool, +n: U32, v: V) -> Trie<V>:
607  match fuel:
608    case 0n:
609      t
610    case 1n+f:
611      match t:
612        case TNode{x, lo, hi}:
613          match here:
614            case True{}:
615              TNode{Some{v}, lo, hi}
616            case False{}:
617              match left:
618                case True{}:
619                  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}
620                case False{}:
621                  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)}
622        case TTip{}:
623          match here:
624            case True{}:
625              TNode{Some{v}, TTip{}, TTip{}}
626            case False{}:
627              match left:
628                case True{}:
629                  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{}}
630                case False{}:
631                  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)}
632
633# The value at key k, stored as n = k + 1.
634def trie.at(-V: Data, t: Trie<V>, +k: U32) -> Maybe<&2, V>:
635  +n = (k + 1 : U32)
636  trie.get(V, t, U32.is_eq(n, 1), U32.is_even(n), n)
637
638def trie.set(-V: Data, t: Trie<V>, +k: U32, v: V) -> Trie<V>:
639  +n = (k + 1 : U32)
640  trie.put(V, 32n, t, U32.is_eq(n, 1), U32.is_even(n), n, v)
641
642def trie.from(-V: Data, xs: List<&2, V>, +k: U32, t: Trie<V>) -> Trie<V>:
643  match xs:
644    case Nil{}:
645      t
646    case Con{h, r}:
647      trie.from(V, r, (k + 1 : U32), trie.set(V, t, k, h))
648
649# The walk from pc 0 over the instructions that consume no char: the sets it reaches, or
650# FsAny when it reaches an assertion or a match, so that any char may start a match.
651type Fs is Data:
652  Fs{stack: List<&2, U32>, seen: List<&2, U32>, sets: List<&2, Inst>}
653  FsAny{}
654
655def first.inst(i: Maybe<&2, Inst>, +pc: U32, stack: List<&2, U32>, seen: List<&2, U32>, sets: List<&2, Inst>) -> Fs:
656  match i:
657    case Some{IJmp{x}}:
658      Fs{x <> stack, seen, sets}
659    case Some{ISplit{x, y}}:
660      Fs{x <> y <> stack, seen, sets}
661    case Some{ISave{k}}:
662      Fs{(pc + 1 : U32) <> stack, seen, sets}
663    case Some{ISet{neg, items}}:
664      Fs{stack, seen, ISet{neg, items} <> sets}
665    case _:
666      FsAny{}
667
668def first.seen(hit: Bool, +prog: List<&2, Inst>, +pc: U32, stack: List<&2, U32>, seen: List<&2, U32>, sets: List<&2, Inst>) -> Fs:
669  match hit:
670    case True{}:
671      Fs{stack, seen, sets}
672    case False{}:
673      first.inst(List.get(&2, Inst, prog, U32.to_nat(pc)), pc, stack, pc <> seen, sets)
674
675# fuel: each pc expands once and pushes at most two pcs.
676def first(fuel: Nat, +prog: List<&2, Inst>, st: Fs) -> Maybe<&2, List<&2, Inst>>:
677  match fuel:
678    case 0n:
679      None{}
680    case 1n+f:
681      match st:
682        case FsAny{}:
683          None{}
684        case Fs{Nil{}, seen, sets}:
685          Some{sets}
686        case Fs{Con{+pc, t}, +seen, sets}:
687          first(f, prog, first.seen(List.contains(~U32, ~U32.is_eq, seen, pc), prog, pc, t, seen, sets))
688
689# Bit-parallel NFA for is_match: bit pc stands for the set at pc, waiting on the next char.
690# The epsilon walk from a pc: the sets it reaches and whether it reaches the match, where at0
691# says the position is the start of the text and at1 the end.
692type Ew is Data:
693  Ew{stack: List<&2, U32>, seen: List<&2, U32>, mask: U32, hit: Bool}
694
695def eps.ctx(k: U32, +at0: Bool, +at1: Bool) -> Bool:
696  match k:
697    case 0:
698      at0
699    case 1:
700      at1
701    case _:
702      False{}
703
704def eps.assert(ok: Bool, +pc: U32, stack: List<&2, U32>, seen: List<&2, U32>, mask: U32, hit: Bool) -> Ew:
705  match ok:
706    case True{}:
707      Ew{(pc + 1 : U32) <> stack, seen, mask, hit}
708    case False{}:
709      Ew{stack, seen, mask, hit}
710
711def 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:
712  match i:
713    case Some{IJmp{x}}:
714      Ew{x <> stack, seen, mask, hit}
715    case Some{ISplit{x, y}}:
716      Ew{x <> y <> stack, seen, mask, hit}
717    case Some{ISave{k}}:
718      Ew{(pc + 1 : U32) <> stack, seen, mask, hit}
719    case Some{IAssert{k}}:
720      eps.assert(eps.ctx(k, at0, at1), pc, stack, seen, mask, hit)
721    case Some{ISet{neg, items}}:
722      Ew{stack, seen, (mask .|. (1 << U32.to_nat(pc)) : U32), hit}
723    case Some{IMatch{}}:
724      Ew{stack, seen, mask, True{}}
725    case None{}:
726      Ew{stack, seen, mask, hit}
727
728def eps.seen(hit: Bool, +prog: List<&2, Inst>, +pc: U32, +at0: Bool, +at1: Bool, w: Ew) -> Ew:
729  match hit:
730    case True{}:
731      w
732    case False{}:
733      Ew{stack, seen, mask, h} = w
734      eps.inst(List.get(&2, Inst, prog, U32.to_nat(pc)), pc, at0, at1, stack, pc <> seen, mask, h)
735
736# fuel: each pc expands once and pushes at most two pcs.
737def eps.go(fuel: Nat, +prog: List<&2, Inst>, +at0: Bool, +at1: Bool, w: Ew) -> Ew:
738  match fuel:
739    case 0n:
740      w
741    case 1n+f:
742      match w:
743        case Ew{Nil{}, seen, mask, hit}:
744          Ew{Nil{}, seen, mask, hit}
745        case Ew{Con{+pc, t}, +seen, mask, hit}:
746          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}))
747
748def eps(+fuel: Nat, +prog: List<&2, Inst>, +pc: U32, +at0: Bool, +at1: Bool) -> Ew:
749  eps.go(fuel, prog, at0, at1, Ew{[pc], Nil{}, 0, False{}})
750
751def Ew.mask(w: Ew) -> U32:
752  Ew{s, v, mask, hit} = w
753  mask
754
755def Ew.hit(w: Ew) -> Bool:
756  Ew{s, v, mask, hit} = w
757  hit
758
759# The set at bit mask; follow: the sets live after it takes a char; fin, end: whether the match
760# is then reached inside the text, or at its end.
761type Bit is Data:
762  Bit{mask: U32, neg: Bool, items: List<&2, Item>, follow: U32, fin: Bool, end: Bool}
763
764# at0: the sets live at the start of the text, and hit0 whether the empty match is there;
765# hit01 the same for the empty text; atn and hitn the same inside the text, hit1 at its end.
766type Bits is Data:
767  Bits{sets: List<&2, Bit>, at0: U32, hit0: Bool, hit01: Bool, atn: U32, hit1: Bool}
768
769def bits.set(+fuel: Nat, +prog: List<&2, Inst>, +pc: U32, neg: Bool, items: List<&2, Item>) -> Bit:
770  +w = eps(fuel, prog, (pc + 1 : U32), False{}, False{})
771  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{}))}
772
773def bits.sets(xs: List<&2, Inst>, +fuel: Nat, +prog: List<&2, Inst>, +pc: U32) -> List<&2, Bit>:
774  match xs:
775    case Nil{}:
776      Nil{}
777    case Con{ISet{neg, items}, t}:
778      bits.set(fuel, prog, pc, neg, items) <> bits.sets(t, fuel, prog, (pc + 1 : U32))
779    case Con{i, t}:
780      bits.sets(t, fuel, prog, (pc + 1 : U32))
781
782# Word boundaries depend on the chars on both sides, which one mask per set cannot track.
783def bits.plain(xs: List<&2, Inst>) -> Bool:
784  match xs:
785    case Nil{}:
786      True{}
787    case Con{IAssert{+k}, t}:
788      U32.is_lt(k, 2) && bits.plain(t)
789    case Con{i, t}:
790      bits.plain(t)
791
792def bits.if(ok: Bool, +fuel: Nat, +prog: List<&2, Inst>) -> Maybe<&2, Bits>:
793  match ok:
794    case False{}:
795      None{}
796    case True{}:
797      +w0 = eps(fuel, prog, 0, True{}, False{})
798      +wn = eps(fuel, prog, 0, False{}, False{})
799      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{}))}}
800
801def bits(+fuel: Nat, +prog: List<&2, Inst>) -> Maybe<&2, Bits>:
802  bits.if(Nat.is_le(List.length(&2, Inst, prog), 32n) && bits.plain(prog), fuel, prog)
803
804def item.has(i: Item, +c: U32) -> Bool:
805  match i:
806    case Rng{+lo, +hi}:
807      U32.is_le(lo, c) && U32.is_le(c, hi)
808    case Prop{neg, name}:
809      Bool.xor(neg, String.starts_with(U.category(Chr{c}), name))
810
811def items.has(xs: List<&2, Item>, +c: U32) -> Bool:
812  match xs:
813    case Nil{}:
814      False{}
815    case Con{h, t}:
816      item.has(h, c) || items.has(t, c)
817
818def starts(xs: List<&2, Inst>, +c: U32) -> Bool:
819  match xs:
820    case Nil{}:
821      False{}
822    case Con{ISet{neg, set}, t}:
823      Bool.xor(neg, items.has(set, c)) || starts(t, c)
824    case Con{i, t}:
825      starts(t, c)
826
827# The ASCII bytes that may start a match, one bit per byte, 32 to a word.
828type Asc is Data:
829  Asc{m0: U32, m1: U32, m2: U32, m3: U32}
830
831def asc.bit(hit: Bool, +c: U32, a: Asc) -> Asc:
832  match hit:
833    case False{}:
834      a
835    case True{}:
836      Asc{+m0, +m1, +m2, +m3} = a
837      +b = (1 << U32.to_nat((c .&. 31 : U32)) : U32)
838      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)}
839
840# c: the byte for step n, counting down from 127 to 0.
841def asc.go(n: Nat, +c: U32, +sets: List<&2, Inst>, a: Asc) -> Asc:
842  match n:
843    case 0n:
844      a
845    case 1n+p:
846      asc.go(p, (c - 1 : U32), sets, asc.bit(starts(sets, c), c, a))
847
848def asc(start: Maybe<&2, List<&2, Inst>>) -> Maybe<&2, Asc>:
849  match start:
850    case None{}:
851      None{}
852    case Some{sets}:
853      Some{asc.go(128n, 127, sets, Asc{0, 0, 0, 0})}
854
855# prog: the instructions by pc; fuel: enough steps for one closure; slots: two per group, group 0 included;
856# start: the sets one of which the first char of a match is in, or None when a match may start anywhere;
857# bits: the bit-parallel form, for programs of at most 32 instructions without word boundaries;
858# asc: start as a table of ASCII bytes, for skipping through Bytes; plain: no word boundary.
859type Regex is Data:
860  Regex{prog: Trie<Inst>, fuel: Nat, slots: Nat, start: Maybe<&2, List<&2, Inst>>, bits: Maybe<&2, Bits>, asc: Maybe<&2, Asc>, plain: Bool}
861
862def build(+node: Node, +n: U32) -> Regex:
863  +insts = {ISave{0} <> emit(node, 1, [ISave{1}, IMatch{}]) : List<&2, Inst>}
864  +fuel = Nat.add(Nat.mul(3n, List.length(&2, Inst, insts)), 2n)
865  +start = first(fuel, insts, Fs{[0], Nil{}, Nil{}})
866  Regex{trie.from(Inst, insts, 0, TTip{}), fuel, U32.to_nat((2 * n : U32)), start, bits(fuel, insts), asc(start), bits.plain(insts)}
867
868def compile.fin(st: Ps) -> Maybe<&2, Regex>:
869  match st:
870    case PsFail{}:
871      None{}
872    case Ps{n, rep, stack, alts, cur}:
873      match stack:
874        case Nil{}:
875          Some{build(alt.go(alts, seq(cur)), n)}
876        case Con{f, up}:
877          None{}
878
879def compile.parse(toks: Maybe<&2, List<&2, Tok>>) -> Maybe<&2, Regex>:
880  match toks:
881    case None{}:
882      None{}
883    case Some{ts}:
884      compile.fin(parse(ts, Ps{1, False{}, Nil{}, Nil{}, Nil{}}))
885
886# The pattern, or None for a syntax error.
887def compile(+pat: String) -> Maybe<&2, Regex>:
888  compile.parse(lex(Nat.add(String.length(pat), 2n), LGo{pat, Nil{}}))
889
890# Matcher
891# -------
892
893def word(m: Maybe<&2, Char>) -> Bool:
894  match m:
895    case None{}:
896      False{}
897    case Some{Chr{+c}}:
898      is_word(c)
899
900def assert.ok(k: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>) -> Bool:
901  match k:
902    case 0:
903      Maybe.is_none(&2, Char, prev)
904    case 1:
905      Maybe.is_none(&2, Char, next)
906    case 2:
907      Bool.xor(word(prev), word(next))
908    case _:
909      Bool.not(Bool.xor(word(prev), word(next)))
910
911# A thread: its pc and its capture slots.
912type Th is Data:
913  Th{pc: U32, caps: List<&2, Maybe<&2, U32>>}
914
915# The epsilon closure as a depth-first walk: stack is the work left, seen the pcs
916# visited at this position, out the threads that wait on a char or match (reversed).
917type Cl is Data:
918  Cl{stack: List<&2, Th>, seen: Trie<Unit>, out: List<&2, Th>}
919
920def close.assert(ok: Bool, +pc: U32, caps: List<&2, Maybe<&2, U32>>, stack: List<&2, Th>, seen: Trie<Unit>, out: List<&2, Th>) -> Cl:
921  match ok:
922    case True{}:
923      Cl{Th{(pc + 1 : U32), caps} <> stack, seen, out}
924    case False{}:
925      Cl{stack, seen, out}
926
927def 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:
928  match i:
929    case None{}:
930      Cl{stack, seen, out}
931    case Some{IJmp{x}}:
932      Cl{Th{x, caps} <> stack, seen, out}
933    case Some{ISplit{x, y}}:
934      Cl{Th{x, caps} <> Th{y, caps} <> stack, seen, out}
935    case Some{ISave{k}}:
936      Cl{Th{(pc + 1 : U32), List.set(&2, Maybe<&2, U32>, caps, U32.to_nat(k), Some{pos})} <> stack, seen, out}
937    case Some{IAssert{k}}:
938      close.assert(assert.ok(k, prev, next), pc, caps, stack, seen, out)
939    case Some{ISet{neg, items}}:
940      Cl{stack, seen, Th{pc, caps} <> out}
941    case Some{IMatch{}}:
942      Cl{stack, seen, Th{pc, caps} <> out}
943
944# ponytail: trie lookup and membership cost O(log m) per thread step, so a char costs
945# O(m log m) for m instructions; a sparse set over an Array would make a step O(1).
946def 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:
947  match hit:
948    case True{}:
949      Cl{stack, seen, out}
950    case False{}:
951      close.inst(trie.at(Inst, prog, pc), pc, caps, stack, trie.set(Unit, seen, pc, Unit{}), out, pos, prev, next)
952
953def 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:
954  Th{+pc, caps} = th
955  close.seen(Maybe.is_some(&2, Unit, trie.at(Unit, seen, pc)), prog, pc, caps, stack, seen, out, pos, prev, next)
956
957# fuel: each pc expands once and pushes at most two threads.
958def close(fuel: Nat, +prog: Trie<Inst>, +pos: U32, +prev: Maybe<&2, Char>, +next: Maybe<&2, Char>, st: Cl) -> List<&2, Th>:
959  match fuel:
960    case 0n:
961      Cl{stack, seen, out} = st
962      List.reverse(&2, Th, out)
963    case 1n+f:
964      match st:
965        case Cl{Nil{}, seen, out}:
966          List.reverse(&2, Th, out)
967        case Cl{Con{th, t}, seen, out}:
968          close(f, prog, pos, prev, next, close.step(th, t, seen, out, prog, pos, prev, next))
969
970# A scan of the threads at one char, in priority order: items are the threads that
971# step past it (reversed), best the latest match. A match drops every later thread.
972type Sc is Data:
973  Sc{items: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>, stop: Bool}
974
975def 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:
976  match hit:
977    case True{}:
978      Sc{Th{(pc + 1 : U32), caps} <> items, best, False{}}
979    case False{}:
980      Sc{items, best, False{}}
981
982def 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:
983  match c:
984    case None{}:
985      Sc{items, best, False{}}
986    case Some{Chr{+x}}:
987      scan.set(Bool.xor(neg, items.has(set, x)), pc, caps, items, best)
988
989# any: only whether a match exists counts, so a match also drops the earlier threads.
990def scan.hit(any: Bool, caps: List<&2, Maybe<&2, U32>>, items: List<&2, Th>) -> Sc:
991  match any:
992    case True{}:
993      Sc{Nil{}, Some{caps}, True{}}
994    case False{}:
995      Sc{items, Some{caps}, True{}}
996
997def 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:
998  match i:
999    case Some{IMatch{}}:
1000      scan.hit(any, caps, items)
1001    case Some{ISet{neg, set}}:
1002      scan.char(c, neg, set, pc, caps, items, best)
1003    case _:
1004      Sc{items, best, False{}}
1005
1006def 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:
1007  match stop:
1008    case True{}:
1009      Sc{items, best, True{}}
1010    case False{}:
1011      Th{+pc, caps} = th
1012      scan.inst(trie.at(Inst, prog, pc), c, any, pc, caps, items, best)
1013
1014def scan.step(st: Sc, th: Th, +prog: Trie<Inst>, c: Maybe<&2, Char>, +any: Bool) -> Sc:
1015  Sc{items, best, stop} = st
1016  scan.go(stop, th, prog, c, any, items, best)
1017
1018def scan(xs: List<&2, Th>, +prog: Trie<Inst>, +c: Maybe<&2, Char>, +any: Bool, st: Sc) -> Sc:
1019  match xs:
1020    case Nil{}:
1021      st
1022    case Con{th, t}:
1023      scan(t, prog, c, any, scan.step(st, th, prog, c, any))
1024
1025# The live threads and the best match so far.
1026type Vm is Data:
1027  Vm{ths: List<&2, Th>, best: Maybe<&2, List<&2, Maybe<&2, U32>>>}
1028
1029# Until a match is found, a new thread starts at each position, below every other.
1030def seed(best: Maybe<&2, List<&2, Maybe<&2, U32>>>, xs: List<&2, Th>, init: List<&2, Maybe<&2, U32>>) -> List<&2, Th>:
1031  match best:
1032    case None{}:
1033      List.append(&2, Th, xs, [Th{0, init}])
1034    case Some{b}:
1035      xs
1036
1037# No live thread and no match yet: the seed is the only thread, and it dies unless next is in start.
1038def 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:
1039  match items best start next:
1040    case Nil{} None{} Some{sets} None{}:
1041      True{}
1042    case Nil{} None{} Some{sets} Some{Chr{+c}}:
1043      Bool.not(starts(sets, c))
1044    case _ _ _ _:
1045      False{}
1046
1047def 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:
1048  match skip:
1049    case True{}:
1050      Vm{Nil{}, None{}}
1051    case False{}:
1052      Vm{close(fuel, prog, pos, prev, next, Cl{seed(best, List.reverse(&2, Th, items), init), TTip{}, Nil{}}), best}
1053
1054def 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:
1055  Sc{+items, +best, stop} = sc
1056  run.seed(seed.skip(items, best, start, next), items, best, prog, fuel, init, pos, prev, next)
1057
1058def 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:
1059  Vm{ths, best} = st
1060  run.close(scan(ths, prog, Some{c}, any, Sc{Nil{}, best, False{}}), prog, fuel, init, start, pos, Some{c}, next)
1061
1062def run.end(sc: Sc) -> Maybe<&2, List<&2, Maybe<&2, U32>>>:
1063  Sc{items, best, stop} = sc
1064  best
1065
1066# pos: the position of s's head. Once a match exists and no thread is live, the rest of s cannot change it.
1067def 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>>>:
1068  match s:
1069    case SNil{}:
1070      Vm{ths, best} = st
1071      run.end(scan(ths, prog, None{}, any, Sc{Nil{}, best, False{}}))
1072    case SCon{+c, +t}:
1073      match st:
1074        case Vm{Nil{}, Some{b}}:
1075          Some{b}
1076        case Vm{ths, best}:
1077          +p = (pos + 1 : U32)
1078          run(t, prog, fuel, init, start, any, p, run.step(Vm{ths, best}, prog, fuel, init, start, any, p, c, String.get(t, 0n)))
1079
1080type Span is Data:
1081  Span{start: U32, end: U32}
1082
1083def spans(caps: List<&2, Maybe<&2, U32>>) -> List<&2, Maybe<&2, Span>>:
1084  match caps:
1085    case Con{Some{a}, Con{Some{b}, t}}:
1086      Some{Span{a, b}} <> spans(t)
1087    case Con{x, Con{y, t}}:
1088      None{} <> spans(t)
1089    case _:
1090      Nil{}
1091
1092def find.spans(m: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Maybe<&2, List<&2, Maybe<&2, Span>>>:
1093  match m:
1094    case None{}:
1095      None{}
1096    case Some{caps}:
1097      Some{spans(caps)}
1098
1099# slots: capture slots to keep; is_match keeps none, so each ISave is free.
1100def exec(re: Regex, +s: String, +any: Bool) -> Maybe<&2, List<&2, Maybe<&2, U32>>>:
1101  Regex{+prog, +fuel, +slots, +start, bits, asc, plain} = re
1102  +init = List.replicate(Maybe<&2, U32>, Bool.pick(Nat, any, 0n, slots), None{})
1103  run(s, prog, fuel, init, start, any, 0, run.close(Sc{Nil{}, None{}, False{}}, prog, fuel, init, start, 0, None{}, String.get(s, 0n)))
1104
1105# The leftmost match in s: the span of group 0, then of each group; None for a group that did not take part.
1106def find(re: Regex, +s: String) -> Maybe<&2, List<&2, Maybe<&2, Span>>>:
1107  find.spans(exec(re, s, False{}))
1108
1109# The Pike VM form of is_match: stops at the first match of any priority and records no captures.
1110def is_match.vm(re: Regex, +s: String) -> Bool:
1111  Maybe.is_some(&2, List<&2, Maybe<&2, U32>>, exec(re, s, True{}))
1112
1113# One char through the bit NFA: next the sets live after it, fin and end as in Bit.
1114type Bs is Data:
1115  Bs{next: U32, fin: Bool, end: Bool}
1116
1117def bits.take(hit: Bool, +follow: U32, +fin: Bool, +end: Bool, acc: Bs) -> Bs:
1118  match hit:
1119    case False{}:
1120      acc
1121    case True{}:
1122      Bs{+nx, f, e} = acc
1123      Bs{(nx .|. follow : U32), f || fin, e || end}
1124
1125def bits.char(live: Bool, +c: U32, neg: Bool, items: List<&2, Item>, +follow: U32, +fin: Bool, +end: Bool, acc: Bs) -> Bs:
1126  match live:
1127    case False{}:
1128      acc
1129    case True{}:
1130      bits.take(Bool.xor(neg, items.has(items, c)), follow, fin, end, acc)
1131
1132# ponytail: one test per set in the program, not a table lookup; use per-byte tables if sets grow many.
1133def bits.step(xs: List<&2, Bit>, +cur: U32, +c: U32, acc: Bs) -> Bs:
1134  match xs:
1135    case Nil{}:
1136      acc
1137    case Con{Bit{+mask, neg, items, follow, fin, end}, t}:
1138      bits.step(t, cur, c, bits.char(U32.is_ne((cur .&. mask : U32), 0), c, neg, items, follow, fin, end, acc))
1139
1140# Only the sets live at a fresh start wait on c, and c starts none of them: nothing moves.
1141def bits.idle(start: Maybe<&2, List<&2, Inst>>, +cur: U32, +atn: U32, +c: U32) -> Bool:
1142  match start:
1143    case None{}:
1144      False{}
1145    case Some{sets}:
1146      U32.is_eq(cur, atn) && Bool.not(starts(sets, c))
1147
1148# hit1: a match starts and ends at the end of the text, so end starts from it.
1149def bits.go(idle: Bool, +sets: List<&2, Bit>, +atn: U32, +hit1: Bool, +cur: U32, +c: U32) -> Bs:
1150  match idle:
1151    case True{}:
1152      Bs{atn, False{}, hit1}
1153    case False{}:
1154      bits.step(sets, cur, c, Bs{atn, False{}, hit1})
1155
1156# r: the sets live at s's head, whether a match was found, and whether one ends at the end of
1157# the text, if the text ends here. Inside the text an assertion can only fail, so fin implies end,
1158# and a match at fin is final.
1159def bits.run(s: String, +sets: List<&2, Bit>, +start: Maybe<&2, List<&2, Inst>>, +atn: U32, +hit1: Bool, r: Bs) -> Bool:
1160  match s:
1161    case SNil{}:
1162      Bs{cur, done, ok} = r
1163      done || ok
1164    case SCon{Chr{+c}, t}:
1165      match r:
1166        case Bs{cur, True{}, ok}:
1167          True{}
1168        case Bs{+cur, False{}, ok}:
1169          bits.run(t, sets, start, atn, hit1, bits.go(bits.idle(start, cur, atn, c), sets, atn, hit1, cur, c))
1170
1171def bits.is_match(b: Bits, start: Maybe<&2, List<&2, Inst>>, s: String) -> Bool:
1172  Bits{sets, at0, hit0, hit01, atn, hit1} = b
1173  bits.run(s, sets, start, atn, hit1, Bs{at0, hit0, hit01})
1174
1175# The bit NFA form of is_match, or None when the program is too large or has a word boundary.
1176def is_match.bits(re: Regex, s: String) -> Maybe<&2, Bool>:
1177  Regex{prog, fuel, slots, start, bits, asc, plain} = re
1178  match bits:
1179    case None{}:
1180      None{}
1181    case Some{b}:
1182      Some{bits.is_match(b, start, s)}
1183
1184def is_match.pick(m: Maybe<&2, Bool>, re: Regex, +s: String) -> Bool:
1185  match m:
1186    case Some{x}:
1187      x
1188    case None{}:
1189      is_match.vm(re, s)
1190
1191# Whether s has a match; the bit NFA runs when the program allows it, else the Pike VM.
1192def is_match(+re: Regex, +s: String) -> Bool:
1193  is_match.pick(is_match.bits(re, s), re, s)
1194
1195# Bytes
1196# -----
1197# The same matchers over a UTF-8 Bytes buffer; positions are byte offsets, as in RE2 and Go.
1198
1199# A code point decoded from UTF-8 and its width in bytes, or DEnd at the end of the buffer.
1200# An invalid byte is U+FFFD of width 1, as in RE2.
1201type Dc is Data:
1202  Dc{c: U32, w: U32}
1203  DEnd{}
1204
1205def Dc.char(d: Dc) -> Maybe<&2, Char>:
1206  match d:
1207    case DEnd{}:
1208      None{}
1209    case Dc{c, w}:
1210      Some{Chr{c}}
1211
1212def pk.if(ok: Bool, a: Array<U32>, +i: U32) -> Array<U32> & U32:
1213  match ok:
1214    case True{}:
1215      Bytes.peek(a, i)
1216    case False{}:
1217      (a, 0)
1218
1219# Byte i, or 0 past len, which is no continuation byte.
1220def pk(a: Array<U32>, +len: U32, +i: U32) -> Array<U32> & U32:
1221  pk.if(U32.is_lt(i, len), a, i)
1222
1223def cont(+b: U32) -> Bool:
1224  U32.is_eq((b .&. 192 : U32), 128)
1225
1226def dec.pick(ok2: Bool, ok3: Bool, ok4: Bool, +c2: U32, +c3: U32, +c4: U32) -> Dc:
1227  match ok2:
1228    case True{}:
1229      Dc{c2, 2}
1230    case False{}:
1231      match ok3:
1232        case True{}:
1233          Dc{c3, 3}
1234        case False{}:
1235          match ok4:
1236            case True{}:
1237              Dc{c4, 4}
1238            case False{}:
1239              Dc{65533, 1}
1240
1241# Overlong forms, surrogates, and code points past U+10FFFF are invalid.
1242def dec.n(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> Dc:
1243  +x1 = (b1 .&. 63 : U32)
1244  +x2 = (b2 .&. 63 : U32)
1245  +x3 = (b3 .&. 63 : U32)
1246  +c2 = (((b0 .&. 31) << 6n) .|. x1 : U32)
1247  +c3 = ((((b0 .&. 15) << 12n) .|. (x1 << 6n)) .|. x2 : U32)
1248  +c4 = (((((b0 .&. 7) << 18n) .|. (x1 << 12n)) .|. (x2 << 6n)) .|. x3 : U32)
1249  +ok2 = U32.is_le(192, b0) && U32.is_lt(b0, 224) && cont(b1) && U32.is_le(128, c2)
1250  +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))
1251  +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)
1252  dec.pick(ok2, ok3, ok4, c2, c3, c4)
1253
1254def dec.b3(+b0: U32, +b1: U32, +b2: U32, r: Array<U32> & U32) -> Array<U32> & Dc:
1255  (a, +b3) = r
1256  (a, dec.n(b0, b1, b2, b3))
1257
1258def dec.b2(+len: U32, +i: U32, +b0: U32, +b1: U32, r: Array<U32> & U32) -> Array<U32> & Dc:
1259  (a, +b2) = r
1260  dec.b3(b0, b1, b2, pk(a, len, (i + 3 : U32)))
1261
1262def dec.b1(+len: U32, +i: U32, +b0: U32, r: Array<U32> & U32) -> Array<U32> & Dc:
1263  (a, +b1) = r
1264  dec.b2(len, i, b0, b1, pk(a, len, (i + 2 : U32)))
1265
1266def dec.lead(ascii: Bool, +len: U32, +i: U32, +b0: U32, a: Array<U32>) -> Array<U32> & Dc:
1267  match ascii:
1268    case True{}:
1269      (a, Dc{b0, 1})
1270    case False{}:
1271      dec.b1(len, i, b0, pk(a, len, (i + 1 : U32)))
1272
1273def dec.at(+len: U32, +i: U32, r: Array<U32> & U32) -> Array<U32> & Dc:
1274  (a, +b0) = r
1275  dec.lead(U32.is_lt(b0, 128), len, i, b0, a)
1276
1277def dec.if(ok: Bool, a: Array<U32>, +len: U32, +i: U32) -> Array<U32> & Dc:
1278  match ok:
1279    case True{}:
1280      dec.at(len, i, Bytes.peek(a, i))
1281    case False{}:
1282      (a, DEnd{})
1283
1284# The char at byte i, or DEnd at len.
1285def dec(a: Array<U32>, +len: U32, +i: U32) -> Array<U32> & Dc:
1286  dec.if(U32.is_lt(i, len), a, len, i)
1287
1288def asc.word(k: U32, a: Asc) -> U32:
1289  match k:
1290    case 0:
1291      Asc{m0, m1, m2, m3} = a
1292      m0
1293    case 1:
1294      Asc{m0, m1, m2, m3} = a
1295      m1
1296    case 2:
1297      Asc{m0, m1, m2, m3} = a
1298      m2
1299    case _:
1300      Asc{m0, m1, m2, m3} = a
1301      m3
1302
1303# Any non-ASCII byte may start a match: it may lead a char in start.
1304def asc.has(+b: U32, a: Asc) -> Bool:
1305  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)
1306
1307def probe.of(+m: Asc, r: Array<U32> & U32) -> Array<U32> & Bool:
1308  (a, +v) = r
1309  (a, asc.has(v, m))
1310
1311# Past len counts as a hit, so a skip stops there.
1312def probe.if(ok: Bool, a: Array<U32>, +k: U32, +m: Asc) -> Array<U32> & Bool:
1313  match ok:
1314    case True{}:
1315      probe.of(m, Bytes.peek(a, k))
1316    case False{}:
1317      (a, True{})
1318
1319def probe(a: Array<U32>, +len: U32, +k: U32, +m: Asc) -> Array<U32> & Bool:
1320  probe.if(U32.is_lt(k, len), a, k, m)
1321
1322# The first offset at or after k whose byte may start a match, or len; r holds the probe of k.
1323def skip(fuel: Nat, r: Array<U32> & Bool, +len: U32, +k: U32, +m: Asc) -> Array<U32> & U32:
1324  match fuel:
1325    case 0n:
1326      (a, h) = r
1327      (a, k)
1328    case 1n+f:
1329      (a, hit) = r
1330      match hit:
1331        case True{}:
1332          (a, k)
1333        case False{}:
1334          skip(f, probe(a, len, (k + 1 : U32), m), len, (k + 1 : U32), m)
1335
1336def skip.from(a: Array<U32>, +len: U32, +k: U32, +m: Asc) -> Array<U32> & U32:
1337  skip(U32.to_nat((len - k : U32)), probe(a, len, k, m), len, k, m)
1338
1339# The Pike VM over Bytes: the buffer, the offset i of the next char, that char, and the threads waiting on it.
1340type Rb is Type:
1341  Rb{a: Array<U32>, i: U32, d: Dc, st: Vm}
1342
1343def 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:
1344  (a, +d) = r
1345  Rb{a, j, d, run.step(st, prog, fuel, init, start, any, j, Chr{c}, Dc.char(d))}
1346
1347# A fresh seed at k. start is Some here, so no assertion is reachable before a char and prev does not count.
1348def 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:
1349  (a, +d) = r
1350  Rb{a, k, d, run.close(Sc{Nil{}, None{}, False{}}, prog, fuel, init, start, k, None{}, Dc.char(d))}
1351
1352def 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:
1353  (a, +k) = r
1354  rb.seed(dec(a, len, k), k, prog, fuel, init, start)
1355
1356# No thread is live and no match exists. With asc, the seed at the char before j was skipped
1357# because that char cannot start a match: jump to the next byte that may. Without asc, the
1358# seed died on an assertion, so step on as usual; prev matters then.
1359def 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:
1360  match asc:
1361    case None{}:
1362      rb.step(dec(a, len, j), j, Vm{Nil{}, None{}}, c, prog, fuel, init, start, any)
1363    case Some{+m}:
1364      rb.skip(skip.from(a, len, j, m), len, prog, fuel, init, start)
1365
1366# fuel: each step eats at least one byte, and the last one sees DEnd.
1367def 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>>>:
1368  match fuel:
1369    case 0n:
1370      Rb{a, i, d, st} = r
1371      (a, None{})
1372    case 1n+f:
1373      Rb{a, +i, d, st} = r
1374      match d:
1375        case DEnd{}:
1376          Vm{ths, best} = st
1377          (a, run.end(scan(ths, prog, None{}, any, Sc{Nil{}, best, False{}})))
1378        case Dc{+c, +w}:
1379          match st:
1380            case Vm{Nil{}, Some{b}}:
1381              (a, Some{b})
1382            case Vm{Nil{}, None{}}:
1383              runb(f, rb.idle(asc, a, len, (i + w : U32), c, prog, cfuel, init, start, any), len, prog, cfuel, init, start, asc, any)
1384            case Vm{ths, best}:
1385              +j = (i + w : U32)
1386              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)
1387
1388# Lazy DFA
1389# --------
1390# The Pike VM step over Bytes, cached per state and ASCII char. A state is the ordered pcs of
1391# the threads and whether a match was found. A transition is learned once, by running the step
1392# on symbolic captures: each thread holds only its own index, in an extra last slot, so after the
1393# step each new thread shows the thread it came from and the slots it saved. Later steps replay
1394# that on the real captures. Inside the text ^ and $ always fail, so a transition does not depend
1395# on the chars around it; the last char, which sees the end, takes the plain step. Word boundaries
1396# read the chars on both sides, so programs with them keep the plain Pike VM.
1397
1398# The seed thread's index, and the id of a state the full cache could not add.
1399def seed.id() -> U32:
1400  4294967295
1401
1402# A new thread: pc, the thread at src it came from (or the seed), and the slots it saved.
1403type Op is Data:
1404  Op{src: U32, pc: U32, saves: List<&2, U32>}
1405
1406# next: the state after the char; hit: 1 + the index of the thread that matched, or 0;
1407# fresh: no match yet and every new thread comes from the seed, so the next state is a fresh start.
1408type Tr is Data:
1409  TrNo{}
1410  TrSame{}
1411  Tr{next: U32, hit: U32, outs: List<&2, Op>, fresh: Bool}
1412
1413type Sk is Data:
1414  Sk{pcs: List<&2, U32>, done: Bool}
1415
1416type Ix is Data:
1417  Ix{key: Sk, id: U32}
1418
1419# The interned states, how many there are, and the id of one.
1420type Ik is Data:
1421  Ik{keys: List<&2, Ix>, n: U32, id: U32}
1422
1423# A learned transition, with the next state's key in place of its id.
1424type Lr is Data:
1425  Lr{hit: U32, outs: List<&2, Op>, key: Sk, fresh: Bool}
1426
1427def vm.pcs(xs: List<&2, Th>) -> List<&2, U32>:
1428  match xs:
1429    case Nil{}:
1430      Nil{}
1431    case Con{Th{pc, caps}, t}:
1432      pc <> vm.pcs(t)
1433
1434def vm.key(st: Vm) -> Sk:
1435  Vm{ths, best} = st
1436  Sk{vm.pcs(ths), Maybe.is_some(&2, List<&2, Maybe<&2, U32>>, best)}
1437
1438def pcs.eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
1439  match xs ys:
1440    case Nil{} Nil{}:
1441      True{}
1442    case Con{+a, s} Con{+b, t}:
1443      U32.is_eq(a, b) && pcs.eq(s, t)
1444    case _ _:
1445      False{}
1446
1447def sk.eq(a: Sk, b: Sk) -> Bool:
1448  Sk{p, x} = a
1449  Sk{q, y} = b
1450  Bool.not(Bool.xor(x, y)) && pcs.eq(p, q)
1451
1452# ponytail: a linear scan over at most cap states, run only when a transition is learned; hash the keys if cap grows.
1453def ix.find(xs: List<&2, Ix>, +k: Sk) -> U32:
1454  match xs:
1455    case Nil{}:
1456      seed.id()
1457    case Con{Ix{key, +id}, t}:
1458      Bool.pick(U32, sk.eq(key, k), id, ix.find(t, k))
1459
1460def intern.if(miss: Bool, +found: U32, keys: List<&2, Ix>, +n: U32, +k: Sk) -> Ik:
1461  match miss:
1462    case True{}:
1463      Ik{Ix{k, n} <> keys, (n + 1 : U32), n}
1464    case False{}:
1465      Ik{keys, n, found}
1466
1467def intern.full(room: Bool, +keys: List<&2, Ix>, +n: U32, +k: Sk) -> Ik:
1468  match room:
1469    case True{}:
1470      +found = ix.find(keys, k)
1471      intern.if(U32.is_eq(found, seed.id()), found, keys, n, k)
1472    case False{}:
1473      Ik{keys, n, seed.id()}
1474
1475# The id of state k, added when new; seed.id() when the cache is full. A full cache is not
1476# searched: with many states the search would cost more than the step it saves.
1477def intern(+keys: List<&2, Ix>, +n: U32, +cap: U32, +k: Sk) -> Ik:
1478  intern.full(U32.is_lt(n, cap), keys, n, k)
1479
1480def sym.caps(+slots: Nat, +i: U32) -> List<&2, Maybe<&2, U32>>:
1481  List.append(&2, Maybe<&2, U32>, List.replicate(Maybe<&2, U32>, slots, None{}), [Some{i}])
1482
1483def sym.ths(xs: List<&2, Th>, +slots: Nat, +i: U32) -> List<&2, Th>:
1484  match xs:
1485    case Nil{}:
1486      Nil{}
1487    case Con{Th{pc, caps}, t}:
1488      Th{pc, sym.caps(slots, i)} <> sym.ths(t, slots, (i + 1 : U32))
1489
1490# The index in the last slot.
1491def sym.src(xs: List<&2, Maybe<&2, U32>>) -> U32:
1492  match xs:
1493    case Con{Some{x}, Nil{}}:
1494      x
1495    case Con{h, t}:
1496      sym.src(t)
1497    case Nil{}:
1498      seed.id()
1499
1500# The slots before the last that hold a position.
1501def sym.saves(xs: List<&2, Maybe<&2, U32>>, +k: U32) -> List<&2, U32>:
1502  match xs:
1503    case Con{h, Nil{}}:
1504      Nil{}
1505    case Con{Some{x}, t}:
1506      k <> sym.saves(t, (k + 1 : U32))
1507    case Con{None{}, t}:
1508      sym.saves(t, (k + 1 : U32))
1509    case Nil{}:
1510      Nil{}
1511
1512def sym.outs(xs: List<&2, Th>) -> List<&2, Op>:
1513  match xs:
1514    case Nil{}:
1515      Nil{}
1516    case Con{Th{+pc, +caps}, t}:
1517      Op{sym.src(caps), pc, sym.saves(caps, 0)} <> sym.outs(t)
1518
1519def sym.fresh(xs: List<&2, Op>) -> Bool:
1520  match xs:
1521    case Nil{}:
1522      True{}
1523    case Con{Op{+src, pc, saves}, t}:
1524      U32.is_eq(src, seed.id()) && sym.fresh(t)
1525
1526def op.same(saves: List<&2, U32>, +src: U32, +pc: U32, +i: U32, +old: U32) -> Bool:
1527  match saves:
1528    case Nil{}:
1529      U32.is_eq(src, i) && U32.is_eq(pc, old)
1530    case Con{h, t}:
1531      False{}
1532
1533def ops.same(xs: List<&2, Op>, ths: List<&2, Th>, +i: U32) -> Bool:
1534  match xs ths:
1535    case Nil{} Nil{}:
1536      True{}
1537    case Con{Op{+src, +pc, saves}, t} Con{Th{+old, caps}, rest}:
1538      op.same(saves, src, pc, i, old) && ops.same(t, rest, (i + 1 : U32))
1539    case _ _:
1540      False{}
1541
1542def tr.of(same: Bool, +next: U32, +hit: U32, +outs: List<&2, Op>, +fresh: Bool) -> Tr:
1543  match same:
1544    case True{}:
1545      TrSame{}
1546    case False{}:
1547      Tr{next, hit, outs, fresh}
1548
1549def sym.lr(+hit: U32, +done: Bool, v: Vm) -> Lr:
1550  Vm{+ths, best} = v
1551  +outs = sym.outs(ths)
1552  Lr{hit, outs, Sk{vm.pcs(ths), done}, Bool.not(done) && sym.fresh(outs)}
1553
1554def sym.hit(stop: Bool, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> U32:
1555  match stop:
1556    case True{}:
1557      match best:
1558        case None{}:
1559          0
1560        case Some{caps}:
1561          (sym.src(caps) + 1 : U32)
1562    case False{}:
1563      0
1564
1565# The closure after the char, inside the text: prev and next are any chars, and start is None
1566# so the seed always runs; replay.vm skips a fresh start the way seed.skip does.
1567def sym.close(sc: Sc, +done: Bool, +prog: Trie<Inst>, +fuel: Nat, +slots: Nat, +c: U32) -> Lr:
1568  Sc{items, +best, +stop} = sc
1569  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}}))
1570
1571# Once a match is found no seed starts, so a done state scans with some best.
1572def sym.best(best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Maybe<&2, List<&2, Maybe<&2, U32>>>:
1573  match best:
1574    case None{}:
1575      None{}
1576    case Some{b}:
1577      Some{Nil{}}
1578
1579def learn(st: Vm, +c: U32, +prog: Trie<Inst>, +fuel: Nat, +slots: Nat, +any: Bool) -> Lr:
1580  Vm{ths, +best} = st
1581  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)
1582
1583def caps.at(m: Maybe<&2, Th>, +init: List<&2, Maybe<&2, U32>>) -> List<&2, Maybe<&2, U32>>:
1584  match m:
1585    case None{}:
1586      init
1587    case Some{Th{pc, caps}}:
1588      caps
1589
1590def caps.of.if(seed: Bool, +src: U32, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>) -> List<&2, Maybe<&2, U32>>:
1591  match seed:
1592    case True{}:
1593      init
1594    case False{}:
1595      caps.at(List.get(&2, Th, ths, U32.to_nat(src)), init)
1596
1597def caps.of(+src: U32, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>) -> List<&2, Maybe<&2, U32>>:
1598  caps.of.if(U32.is_eq(src, seed.id()), src, ths, init)
1599
1600def saves.put(xs: List<&2, U32>, caps: List<&2, Maybe<&2, U32>>, +pos: U32) -> List<&2, Maybe<&2, U32>>:
1601  match xs:
1602    case Nil{}:
1603      caps
1604    case Con{+k, t}:
1605      saves.put(t, List.set(&2, Maybe<&2, U32>, caps, U32.to_nat(k), Some{pos}), pos)
1606
1607def replay(xs: List<&2, Op>, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>, +pos: U32) -> List<&2, Th>:
1608  match xs:
1609    case Nil{}:
1610      Nil{}
1611    case Con{Op{+src, pc, saves}, t}:
1612      Th{pc, saves.put(saves, caps.of(src, ths, init), pos)} <> replay(t, ths, init, pos)
1613
1614def 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>>>:
1615  match none:
1616    case True{}:
1617      best
1618    case False{}:
1619      Some{caps.of((hit - 1 : U32), ths, init)}
1620
1621# fresh: no match yet and every thread starts at the seed; skip it when next cannot start a match.
1622def replay.fresh(skip: Bool, outs: List<&2, Op>, +ths: List<&2, Th>, +init: List<&2, Maybe<&2, U32>>, +pos: U32) -> Vm:
1623  match skip:
1624    case True{}:
1625      Vm{Nil{}, None{}}
1626    case False{}:
1627      Vm{replay(outs, ths, init, pos), None{}}
1628
1629# A learned transition on the real threads; next is the char after the new position.
1630def 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:
1631  match fresh:
1632    case True{}:
1633      Vm{+ths, best} = st
1634      replay.fresh(seed.skip(Nil{}, None{}, start, next), outs, ths, init, pos)
1635    case False{}:
1636      Vm{+ths, best} = st
1637      Vm{replay(outs, ths, init, pos), replay.best(U32.is_eq(hit, 0), hit, ths, init, best)}
1638
1639# The DFA over Bytes: the buffer, the transitions by state and ASCII char, the interned states,
1640# the current state, the offset i of the next char, that char, and the threads waiting on it.
1641type Rq is Type:
1642  Rq{a: Array<U32>, tab: Array<Tr>, keys: List<&2, Ix>, n: U32, id: U32, i: U32, d: Dc, st: Vm, same: Bool}
1643
1644def rq.ik(ik: Ik, a: Array<U32>, tab: Array<Tr>, +j: U32, +d: Dc, st: Vm) -> Rq:
1645  Ik{keys, n, id} = ik
1646  Rq{a, tab, keys, n, id, j, d, st, False{}}
1647
1648def rq.of(r: Rb, tab: Array<Tr>, +keys: List<&2, Ix>, +n: U32, +cap: U32) -> Rq:
1649  Rb{a, +i, +d, +st} = r
1650  rq.ik(intern(keys, n, cap, vm.key(st)), a, tab, i, d, st)
1651
1652def 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:
1653  Ik{keys, +n, +id} = ik
1654  Vm{+ths, +best} = st
1655  +same = U32.is_eq(id, old) && U32.is_eq(hit, 0) && ops.same(outs, ths, 0)
1656  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}
1657
1658def rq.learn(lr: Lr, a: Array<U32>, tab: Array<Tr>, +keys: 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:
1659  Lr{+hit, +outs, +key, +fresh} = lr
1660  rq.store(intern(keys, n, cap, key), a, tab, idx, old, hit, outs, fresh, j, d, st, init, start)
1661
1662# With a full cache, skip building the key too.
1663def rq.real(room: Bool, a: Array<U32>, tab: Array<Tr>, +keys: List<&2, Ix>, +n: U32, +j: U32, +d: Dc, +st: Vm, +cap: U32) -> Rq:
1664  match room:
1665    case True{}:
1666      rq.ik(intern(keys, n, cap, vm.key(st)), a, tab, j, d, st)
1667    case False{}:
1668      Rq{a, tab, keys, n, seed.id(), j, d, st, False{}}
1669
1670# A same transition leaves the VM and state id intact. Stop before the last byte:
1671# its following end-of-text context needs the plain Pike step.
1672type Spin is Type:
1673  Spin{a: Array<U32>, tab: Array<Tr>, i: U32}
1674
1675type SpinStep is Type:
1676  SpinStep{a: Array<U32>, tab: Array<Tr>, i: U32, tr: Tr}
1677
1678def spin.byte(last: Bool, a: Array<U32>, +i: U32) -> Array<U32> & U32:
1679  match last:
1680    case True{}:
1681      (a, 128)
1682    case False{}:
1683      Bytes.peek(a, i)
1684
1685def spin.tr(ascii: Bool, tab: Array<Tr>, +id: U32, +c: U32) -> Array<Tr> & Tr:
1686  match ascii:
1687    case True{}:
1688      Array.get(Tr, tab, ((id * 128) + c : U32))
1689    case False{}:
1690      (tab, TrNo{})
1691
1692def spin.state.tr(r: Array<Tr> & Tr, a: Array<U32>, +i: U32) -> SpinStep:
1693  (tab, tr) = r
1694  SpinStep{a, tab, i, tr}
1695
1696def spin.state(r: Array<U32> & U32, tab: Array<Tr>, +i: U32, +id: U32, +cap: U32) -> SpinStep:
1697  (a, +c) = r
1698  spin.state.tr(spin.tr(U32.is_lt(c, 128) && U32.is_lt(id, cap), tab, id, c), a, i)
1699
1700def spin(fuel: Nat, s: SpinStep, +len: U32, +id: U32, +cap: U32) -> Spin:
1701  match fuel:
1702    case 0n:
1703      SpinStep{a, tab, i, tr} = s
1704      Spin{a, tab, i}
1705    case 1n+f:
1706      SpinStep{a, tab, +i, tr} = s
1707      match tr:
1708        case TrSame{}:
1709          +j = (i + 1 : U32)
1710          spin(f, spin.state(spin.byte(Bool.not(U32.is_lt((j + 1 : U32), len)), a, j), tab, j, id, cap), len, id, cap)
1711        case TrNo{}:
1712          Spin{a, tab, i}
1713        case Tr{next, hit, outs, fresh}:
1714          Spin{a, tab, i}
1715
1716# Cached DFA steps reuse two thread buffers; the Pike VM handles learning and text boundaries.
1717type Ar is Type:
1718  Ar{old: Array<Th>, spare: Array<Th>, count: U32, cap: U32, best: Maybe<&2, List<&2, Maybe<&2, U32>>>}
1719
1720def ar.fill(xs: List<&2, Th>, a: Array<Th>, +i: U32) -> Array<Th>:
1721  match xs:
1722    case Nil{}:
1723      a
1724    case Con{th, rest}:
1725      ar.fill(rest, Array.set(Th, a, i, th), (i + 1 : U32))
1726
1727def 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:
1728  match fits:
1729    case True{}:
1730      Ar{ar.fill(ths, old, 0), spare, count, cap, best}
1731    case False{}:
1732      +depth = Nat.add(U32.log2(count), 1n)
1733      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}
1734
1735def ar.reset.put(vm: Vm, old: Array<Th>, spare: Array<Th>, +cap: U32, +init: List<&2, Maybe<&2, U32>>) -> Ar:
1736  Vm{+ths, best} = vm
1737  +count = U32.from_nat(List.length(&2, Th, ths))
1738  ar.reset.size(U32.is_le(count, cap), ths, best, old, spare, count, cap, init)
1739
1740def ar.reset(vm: Vm, ar: Ar, +init: List<&2, Maybe<&2, U32>>) -> Ar:
1741  Ar{old, spare, count, cap, best} = ar
1742  ar.reset.put(vm, old, spare, cap, init)
1743
1744def ar.new(vm: Vm, +init: List<&2, Maybe<&2, U32>>) -> Ar:
1745  ar.reset(vm, Ar{Array.new(Th, 2n, Th{0, init}), Array.new(Th, 2n, Th{0, init}), 0, 4, None{}}, init)
1746
1747def ar.list.go(fuel: Nat, r: Array<Th> & Th, +i: U32, acc: List<&2, Th>) -> Array<Th> & List<&2, Th>:
1748  match fuel:
1749    case 0n:
1750      (a, th) = r
1751      (a, acc)
1752    case 1n+f:
1753      (a, th) = r
1754      ar.list.go(f, Array.get(Th, a, (i - 1 : U32)), (i - 1 : U32), th <> acc)
1755
1756def 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:
1757  (old, ths) = r
1758  (Ar{old, spare, count, cap, best}, Vm{ths, best})
1759
1760def ar.vm(ar: Ar) -> Ar & Vm:
1761  Ar{old, spare, +count, +cap, +best} = ar
1762  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)
1763
1764def ar.src.get(r: Array<Th> & Th) -> Array<Th> & List<&2, Maybe<&2, U32>>:
1765  (old, Th{pc, caps}) = r
1766  (old, caps)
1767
1768def ar.src(seed: Bool, old: Array<Th>, +src: U32, +init: List<&2, Maybe<&2, U32>>) -> Array<Th> & List<&2, Maybe<&2, U32>>:
1769  match seed:
1770    case True{}:
1771      (old, init)
1772    case False{}:
1773      ar.src.get(Array.get(Th, old, src))
1774
1775def 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>:
1776  (old, caps) = r
1777  (old, Array.set(Th, spare, i, Th{pc, saves.put(saves, caps, pos)}))
1778
1779def 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:
1780  match xs:
1781    case Nil{}:
1782      (old, spare) = r
1783      Ar{spare, old, i, cap, best}
1784    case Con{Op{+src, +pc, saves}, rest}:
1785      (old, spare) = r
1786      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)
1787
1788def ar.best.get(r: Array<Th> & List<&2, Maybe<&2, U32>>) -> Array<Th> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1789  (old, caps) = r
1790  (old, Some{caps})
1791
1792def 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>>>:
1793  match no_hit:
1794    case True{}:
1795      (old, best)
1796    case False{}:
1797      ar.best.get(ar.src(U32.is_eq((hit - 1 : U32), seed.id()), old, (hit - 1 : U32), init))
1798
1799def 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:
1800  (old, best) = r
1801  ar.replay(outs, (old, spare), init, pos, 0, cap, best)
1802
1803def ar.cached.fresh(skip: Bool, ar: Ar, outs: List<&2, Op>, +init: List<&2, Maybe<&2, U32>>, +pos: U32) -> Ar:
1804  match skip:
1805    case True{}:
1806      Ar{old, spare, size, +cap, best} = ar
1807      Ar{old, spare, 0, cap, None{}}
1808    case False{}:
1809      Ar{old, spare, size, +cap, best} = ar
1810      ar.replay.best((old, None{}), spare, outs, cap, init, pos)
1811
1812# A cached transition was learned in this run, so the buffers already fit its outputs.
1813def 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:
1814  match fresh:
1815    case True{}:
1816      ar.cached.fresh(seed.skip(Nil{}, None{}, start, next), ar, outs, init, pos)
1817    case False{}:
1818      Ar{old, spare, size, +cap, best} = ar
1819      ar.replay.best(ar.best.none(U32.is_eq(hit, 0), old, hit, init, best), spare, outs, cap, init, pos)
1820
1821type Qst is Type:
1822  QDone{best: List<&2, Maybe<&2, U32>>}
1823  QIdle{ar: Ar}
1824  QLive{ar: Ar}
1825  QPlain{st: Vm}
1826
1827def qa.status.if(zero: Bool, old: Array<Th>, spare: Array<Th>, +count: U32, +cap: U32, best: Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Qst:
1828  match zero:
1829    case False{}:
1830      QLive{Ar{old, spare, count, cap, best}}
1831    case True{}:
1832      match best:
1833        case Some{caps}:
1834          QDone{caps}
1835        case None{}:
1836          QIdle{Ar{old, spare, count, cap, None{}}}
1837
1838def qa.status(ar: Ar) -> Qst:
1839  Ar{old, spare, +count, +cap, best} = ar
1840  qa.status.if(U32.is_zero(count), old, spare, count, cap, best)
1841
1842type Qa is Type:
1843  Qa{a: Array<U32>, tab: Array<Tr>, keys: List<&2, Ix>, n: U32, id: U32, i: U32, d: Dc, ar: Qst, same: Bool}
1844
1845def qa.seed(r: Rq, +init: List<&2, Maybe<&2, U32>>) -> Qa:
1846  Rq{a, tab, keys, n, id, i, d, st, same} = r
1847  Qa{a, tab, keys, n, id, i, d, qa.status(ar.new(st, init)), same}
1848
1849def qa.from.state(cached: Bool, st: Vm, ar: Ar, +init: List<&2, Maybe<&2, U32>>) -> Qst:
1850  match cached:
1851    case True{}:
1852      qa.status(ar.reset(st, ar, init))
1853    case False{}:
1854      QPlain{st}
1855
1856def qa.from(r: Rq, ar: Ar, +init: List<&2, Maybe<&2, U32>>, +cap: U32) -> Qa:
1857  Rq{a, tab, keys, n, +id, i, d, st, same} = r
1858  Qa{a, tab, keys, n, id, i, d, qa.from.state(U32.is_lt(id, cap), st, ar, init), same}
1859
1860def qa.learn.vm(r: Ar & Vm, a: Array<U32>, tab: Array<Tr>, +keys: 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:
1861  (ar, +st) = r
1862  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)
1863
1864def qa.real.vm(r: Ar & Vm, s: Array<U32> & Dc, +j: U32, tab: Array<Tr>, +keys: 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:
1865  (ar, st) = r
1866  (a, +d) = s
1867  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)
1868
1869def qa.real(s: Array<U32> & Dc, +j: U32, tab: Array<Tr>, +keys: 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:
1870  qa.real.vm(ar.vm(ar), s, j, tab, keys, n, c, prog, cfuel, init, start, any, cap)
1871
1872def qa.cached(r: Array<Tr> & Tr, a: Array<U32>, +keys: 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:
1873  (tab, tr) = r
1874  match tr:
1875    case TrNo{}:
1876      qa.learn.vm(ar.vm(ar), a, tab, keys, n, idx, j, d, c, prog, cfuel, init, start, any, slots, cap)
1877    case TrSame{}:
1878      Qa{a, tab, keys, n, (idx / 128 : U32), j, d, qa.status(ar), True{}}
1879    case Tr{+next, +hit, +outs, +fresh}:
1880      Qa{a, tab, keys, n, next, j, d, qa.status(ar.cached(fresh, hit, outs, ar, init, j, start, Dc.char(d))), False{}}
1881
1882def qa.pick(ok: Bool, a: Array<U32>, tab: Array<Tr>, +keys: 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:
1883  match ok:
1884    case True{}:
1885      +idx = ((id * 128) + c : U32)
1886      qa.cached(Array.get(Tr, tab, idx), a, keys, n, idx, j, d, ar, c, prog, cfuel, init, start, any, slots, cap)
1887    case False{}:
1888      qa.real((a, d), j, tab, keys, n, ar, c, prog, cfuel, init, start, any, cap)
1889
1890def qa.step(s: Array<U32> & Dc, +j: U32, tab: Array<Tr>, +keys: 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:
1891  (a, +d) = s
1892  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)
1893
1894def qa.spin.read(s: Array<U32> & Dc, tab: Array<Tr>, +keys: List<&2, Ix>, +n: U32, +id: U32, +i: U32, ar: Qst) -> Qa:
1895  (a, d) = s
1896  Qa{a, tab, keys, n, id, i, d, ar, False{}}
1897
1898def qa.spin.dec(moved: Bool, a: Array<U32>, tab: Array<Tr>, +len: U32, +keys: List<&2, Ix>, +n: U32, +id: U32, +i: U32, d: Dc, ar: Qst) -> Qa:
1899  match moved:
1900    case True{}:
1901      qa.spin.read(dec(a, len, i), tab, keys, n, id, i, ar)
1902    case False{}:
1903      Qa{a, tab, keys, n, id, i, d, ar, False{}}
1904
1905def qa.spin.at(s: Spin, +old: U32, +len: U32, +keys: List<&2, Ix>, +n: U32, +id: U32, d: Dc, ar: Qst) -> Qa:
1906  Spin{a, tab, +i} = s
1907  qa.spin.dec(U32.is_ne(i, old), a, tab, len, keys, n, id, i, d, ar)
1908
1909def qa.spin.if(same: Bool, a: Array<U32>, tab: Array<Tr>, +keys: List<&2, Ix>, +n: U32, +id: U32, +i: U32, d: Dc, ar: Qst, +fuel: Nat, +len: U32, +cap: U32) -> Qa:
1910  match same:
1911    case True{}:
1912      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)
1913    case False{}:
1914      Qa{a, tab, keys, n, id, i, d, ar, False{}}
1915
1916def qa.spin(r: Qa, +fuel: Nat, +len: U32, +cap: U32) -> Qa:
1917  Qa{a, tab, keys, n, +id, +i, d, ar, same} = r
1918  qa.spin.if(same, a, tab, keys, n, id, i, d, ar, fuel, len, cap)
1919
1920def qa.end.vm(st: Vm, a: Array<U32>, +prog: Trie<Inst>, +any: Bool) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1921  Vm{ths, best} = st
1922  (a, run.end(scan(ths, prog, None{}, any, Sc{Nil{}, best, False{}})))
1923
1924def qa.end(r: Ar & Vm, a: Array<U32>, +prog: Trie<Inst>, +any: Bool) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1925  (ar, st) = r
1926  qa.end.vm(st, a, prog, any)
1927
1928def qa.end.status(st: Qst, a: Array<U32>, +prog: Trie<Inst>, +any: Bool) -> Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1929  match st:
1930    case QDone{best}:
1931      (a, Some{best})
1932    case QIdle{ar}:
1933      qa.end(ar.vm(ar), a, prog, any)
1934    case QLive{ar}:
1935      qa.end(ar.vm(ar), a, prog, any)
1936    case QPlain{st}:
1937      qa.end.vm(st, a, prog, any)
1938
1939# Each step consumes a byte; after the cache fills, continue in the plain Pike VM.
1940def 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>>>:
1941  match fuel:
1942    case 0n:
1943      Qa{a, tab, keys, n, id, i, d, ar, same} = r
1944      (a, None{})
1945    case 1n+f:
1946      Qa{a, tab, +keys, +n, +id, +i, d, ar, same} = r
1947      match d:
1948        case DEnd{}:
1949          qa.end.status(ar, a, prog, any)
1950        case Dc{+c, +w}:
1951          match ar:
1952            case QDone{best}:
1953              (a, Some{best})
1954            case QIdle{ar}:
1955              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)
1956            case QLive{ar}:
1957              +j = (i + w : U32)
1958              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)
1959            case QPlain{st}:
1960              runb(Nat.add(f, 1n), Rb{a, i, Dc{c, w}, st}, len, prog, cfuel, init, start, asc, any)
1961
1962def exec.bytes.fin(+len: U32, r: Array<U32> & Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1963  (a, m) = r
1964  (Bytes.Bytes{len, a}, m)
1965
1966# Short texts get a small cache: 8 states, so learning costs little.
1967def exec.bytes.go(plain: Bool, +len: 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>>>:
1968  match plain:
1969    case True{}:
1970      +small = U32.is_lt(len, 4096)
1971      +cap = Bool.pick(U32, small, 8, 256)
1972      runqa(Nat.add(U32.to_nat(len), 2n), qa.seed(rq.of(rb.seed(dec(buf, len, 0), 0, prog, fuel, init, start), Array.new(Tr, Bool.pick(Nat, small, 10n, 15n), TrNo{}), Nil{}, 0, cap), init), len, prog, fuel, init, start, asc, any, slots, cap)
1973    case False{}:
1974      runb(Nat.add(U32.to_nat(len), 2n), rb.seed(dec(buf, len, 0), 0, prog, fuel, init, start), len, prog, fuel, init, start, asc, any)
1975
1976def exec.bytes(re: Regex, b: Bytes.Bytes, +any: Bool) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>:
1977  Regex{+prog, +fuel, +slots, +start, bits, +asc, plain} = re
1978  Bytes.Bytes{+len, buf} = b
1979  +sl = Bool.pick(Nat, any, 0n, slots)
1980  exec.bytes.fin(len, exec.bytes.go(plain, len, buf, prog, fuel, List.replicate(Maybe<&2, U32>, sl, None{}), start, asc, any, sl))
1981
1982def find.bytes.fin(r: Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, Span>>>:
1983  (b, m) = r
1984  (b, find.spans(m))
1985
1986# find over UTF-8 bytes: the buffer back, and spans as byte offsets.
1987def find.bytes(re: Regex, b: Bytes.Bytes) -> Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, Span>>>:
1988  find.bytes.fin(exec.bytes(re, b, False{}))
1989
1990def is_match.bytes.fin(r: Bytes.Bytes & Maybe<&2, List<&2, Maybe<&2, U32>>>) -> Bytes.Bytes & Bool:
1991  (b, m) = r
1992  (b, Maybe.is_some(&2, List<&2, Maybe<&2, U32>>, m))
1993
1994def is_match.bytes.vm(re: Regex, b: Bytes.Bytes) -> Bytes.Bytes & Bool:
1995  is_match.bytes.fin(exec.bytes(re, b, True{}))
1996
1997# The bit NFA over Bytes: the buffer, the offset i of the next char, that char, and the NFA state.
1998type Rt is Type:
1999  Rt{a: Array<U32>, i: U32, d: Dc, st: Bs}
2000
2001def rt.at(r: Array<U32> & Dc, +j: U32, st: Bs) -> Rt:
2002  (a, +d) = r
2003  Rt{a, j, d, st}
2004
2005def rt.skip(r: Array<U32> & U32, +len: U32, +atn: U32, +hit1: Bool) -> Rt:
2006  (a, +k) = r
2007  rt.at(dec(a, len, k), k, Bs{atn, False{}, hit1})
2008
2009# idle: only the sets live at a fresh start wait on c, and c starts none of them.
2010def 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:
2011  match idle:
2012    case True{}:
2013      match asc:
2014        case None{}:
2015          rt.at(dec(a, len, j), j, Bs{atn, False{}, hit1})
2016        case Some{+m}:
2017          rt.skip(skip.from(a, len, j, m), len, atn, hit1)
2018    case False{}:
2019      rt.at(dec(a, len, j), j, bits.step(sets, cur, c, Bs{atn, False{}, hit1}))
2020
2021def 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:
2022  match fuel:
2023    case 0n:
2024      Rt{a, i, d, st} = r
2025      (a, False{})
2026    case 1n+f:
2027      Rt{a, +i, d, st} = r
2028      match d:
2029        case DEnd{}:
2030          Bs{cur, done, ok} = st
2031          (a, done || ok)
2032        case Dc{+c, +w}:
2033          match st:
2034            case Bs{cur, True{}, ok}:
2035              (a, True{})
2036            case Bs{+cur, False{}, ok}:
2037              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)
2038
2039def bits.bytes.fin(+len: U32, r: Array<U32> & Bool) -> Bytes.Bytes & Maybe<&2, Bool>:
2040  (a, x) = r
2041  (Bytes.Bytes{len, a}, Some{x})
2042
2043def bits.bytes(b: Bits, start: Maybe<&2, List<&2, Inst>>, asc: Maybe<&2, Asc>, +len: U32, buf: Array<U32>) -> Bytes.Bytes & Maybe<&2, Bool>:
2044  Bits{sets, at0, hit0, hit01, atn, hit1} = b
2045  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))
2046
2047def 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>:
2048  match m:
2049    case None{}:
2050      (b, None{})
2051    case Some{x}:
2052      Bytes.Bytes{+len, buf} = b
2053      bits.bytes(x, start, asc, len, buf)
2054
2055# The bit NFA form of is_match over Bytes, or None when the program does not allow it.
2056def is_match.bytes.bits(re: Regex, b: Bytes.Bytes) -> Bytes.Bytes & Maybe<&2, Bool>:
2057  Regex{prog, fuel, slots, start, bt, asc, plain} = re
2058  bits.bytes.if(bt, start, asc, b)
2059
2060def is_match.bytes.pick(r: Bytes.Bytes & Maybe<&2, Bool>, re: Regex) -> Bytes.Bytes & Bool:
2061  (b, m) = r
2062  match m:
2063    case Some{x}:
2064      (b, x)
2065    case None{}:
2066      is_match.bytes.vm(re, b)
2067
2068# is_match over UTF-8 bytes: the buffer back, and whether it has a match.
2069def is_match.bytes(+re: Regex, b: Bytes.Bytes) -> Bytes.Bytes & Bool:
2070  is_match.bytes.pick(is_match.bytes.bits(re, b), re)