glob.bend

bend-osdev-apparmor@0.1.0.0 · 888 lines · 105 definitions

1# bend-osdev-apparmor: AppArmor globs (AARE), as an explicit matcher.
2#
3# apparmor.d(5), "Globbing (AARE)": * any run of characters except '/', **
4# any run including '/', ? one character except '/', [abc] [a-c] [^a-c] one
5# character in (or not in) a set, {ab,cd} alternatives. Where the page is
6# silent, the choices follow what apparmor_parser 4.0.1 compiles a pattern to
7# (its --dump=rule-exprs output; see the README, "Experiments"):
8#   * a * that is a whole path segment ('/' before it, '/' or the end after
9#     it) matches one or more characters, so /tmp/* does not match /tmp/;
10#     a ** after a '/' and before a '/', a '*' or the end matches one or
11#     more characters, the first not '/'. Both are a ? followed by the star;
12#   * a negated class may match '/';
13#   * runs of '/' collapse to one, except a leading "//";
14#   * \c is the character c; a class may not hold '\', start with ']' or
15#     end with '-'; a {...} group needs at least two alternatives.
16#
17# A pattern is brace-expanded when it is parsed: AaGlob holds its
18# alternatives, each a sequence of AaGTok. Three matchers, tied by laws for
19# every sequence and path:
20#   AaGSeq.model, the list model: every way to cut the path into one piece
21#     per token (AaGCuts.all), each piece checked against its token;
22#   AaGSeq.matches, the reference: a backtracking walk over the sequence and
23#     the path (exponential in the stars, since Bend evaluates every
24#     argument);
25#   AaGSeq.run, what AaGlob.matches uses: the set of active positions in the
26#     sequence moved along the path a byte at a time, stopping when none is
27#     left (linear in the path, times the sequence's length).
28import Base
29import bend-osdev-apparmor@0.1.0.0/text.bend as X
30
31type AaGRange is Data:
32  AaGRange{lo: U32, hi: U32}
33
34type AaGTok is Data:
35  AaGChar{c: U32}
36  AaGAny{}
37  AaGClass{neg: Bool, ranges: List<&2, AaGRange>}
38  AaGStar{}
39  AaGStar2{}
40
41type AaGlob is Data:
42  AaGlob{alts: List<&2, List<&2, AaGTok>>, literal: Bool}
43
44# Character classes
45
46def AaGRange.has(r: AaGRange, +c: U32) -> Bool:
47  match r:
48    case AaGRange{lo, hi}:
49      Bool.and(U32.is_le(lo, c), U32.is_le(c, hi))
50
51def AaGClass.any(rs: List<&2, AaGRange>, +c: U32) -> Bool:
52  match rs:
53    case Nil{}:
54      False{}
55    case Con{r, t}:
56      Bool.or(AaGRange.has(r, c), AaGClass.any(t, c))
57
58def AaGClass.has(neg: Bool, rs: List<&2, AaGRange>, +c: U32) -> Bool:
59  match neg:
60    case True{}:
61      Bool.not(AaGClass.any(rs, c))
62    case False{}:
63      AaGClass.any(rs, c)
64
65# The matcher
66
67def AaGSeq.matches(+seq: List<&2, AaGTok>, s: List<&2, U32>) -> Bool:
68  match seq:
69    case Nil{}:
70      X.AaText.is_nil(s)
71    case Con{AaGChar{c}, r}:
72      match s:
73        case Nil{}:
74          False{}
75        case Con{h, t}:
76          Bool.and(U32.is_eq(h, c), AaGSeq.matches(r, t))
77    case Con{AaGAny{}, r}:
78      match s:
79        case Nil{}:
80          False{}
81        case Con{h, t}:
82          Bool.and(U32.is_ne(h, 47), AaGSeq.matches(r, t))
83    case Con{AaGClass{neg, rs}, r}:
84      match s:
85        case Nil{}:
86          False{}
87        case Con{h, t}:
88          Bool.and(AaGClass.has(neg, rs, h), AaGSeq.matches(r, t))
89    case Con{AaGStar{}, r}:
90      match s:
91        case Nil{}:
92          AaGSeq.matches(r, Nil{})
93        case Con{+h, +t}:
94          Bool.or(AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), AaGSeq.matches(seq, t)))
95    case Con{AaGStar2{}, r}:
96      match s:
97        case Nil{}:
98          AaGSeq.matches(r, Nil{})
99        case Con{+h, +t}:
100          Bool.or(AaGSeq.matches(r, Con{h, t}), AaGSeq.matches(seq, t))
101
102# The fast matcher: the set of active positions in the sequence, one bit
103# per suffix (the sequence itself, its tail, ..., the empty suffix), moved
104# along the path a byte at a time. Bend evaluates every argument, so the
105# backtracking matcher above explores every branch; this one does a fixed
106# amount of work per byte and position. A law proves it equal to the
107# backtracking matcher for every sequence, path and set of positions.
108
109def AaGNfa.hd(bs: List<&2, Bool>) -> Bool:
110  match bs:
111    case Nil{}:
112      False{}
113    case Con{b, t}:
114      b
115
116def AaGNfa.tl(bs: List<&2, Bool>) -> List<&2, Bool>:
117  match bs:
118    case Nil{}:
119      Nil{}
120    case Con{b, t}:
121      t
122
123# a star stays on a byte (* on anything but '/', ** on anything)
124def AaGNfa.stay(tok: AaGTok, +h: U32) -> Bool:
125  match tok:
126    case AaGStar{}:
127      U32.is_ne(h, 47)
128    case AaGStar2{}:
129      True{}
130    case _:
131      False{}
132
133# a single-byte token moves past a byte it takes
134def AaGNfa.adv(tok: AaGTok, +h: U32) -> Bool:
135  match tok:
136    case AaGChar{c}:
137      U32.is_eq(h, c)
138    case AaGAny{}:
139      U32.is_ne(h, 47)
140    case AaGClass{n, rs}:
141      AaGClass.has(n, rs, h)
142    case _:
143      False{}
144
145# a star may match nothing: the position after it is active too
146def AaGNfa.isstar(tok: AaGTok) -> Bool:
147  match tok:
148    case AaGStar{}:
149      True{}
150    case AaGStar2{}:
151      True{}
152    case _:
153      False{}
154
155# the positions active after the byte h: cin, the position is reached
156# without a byte (after a star); ain, the previous position moved here
157def AaGNfa.next(+seq: List<&2, AaGTok>, +bs: List<&2, Bool>, +cin: Bool, +ain: Bool, +h: U32) -> List<&2, Bool>:
158  match seq:
159    case Nil{}:
160      [ain]
161    case Con{+tok, r}:
162      Con{Bool.or(Bool.and(Bool.or(AaGNfa.hd(bs), cin), AaGNfa.stay(tok, h)), ain), AaGNfa.next(r, AaGNfa.tl(bs), Bool.and(Bool.or(AaGNfa.hd(bs), cin), AaGNfa.isstar(tok)), Bool.and(Bool.or(AaGNfa.hd(bs), cin), AaGNfa.adv(tok, h)), h)}
163
164# what a set of positions accepts: some active position's suffix matches s
165def AaGNfa.sem(+seq: List<&2, AaGTok>, +bs: List<&2, Bool>, +s: List<&2, U32>) -> Bool:
166  match seq:
167    case Nil{}:
168      Bool.and(AaGNfa.hd(bs), X.AaText.is_nil(s))
169    case Con{tok, r}:
170      Bool.or(Bool.and(AaGNfa.hd(bs), AaGSeq.matches(Con{tok, r}, s)), AaGNfa.sem(r, AaGNfa.tl(bs), s))
171
172# some position is active
173def AaGNfa.alive(bs: List<&2, Bool>) -> Bool:
174  match bs:
175    case Nil{}:
176      False{}
177    case Con{b, t}:
178      Bool.or(b, AaGNfa.alive(t))
179
180# the positions moved along the path; at its end, the active positions
181# whose suffixes match the empty string accept. alive: some position is
182# active (computed by the caller); when none is, the path cannot match.
183def AaGNfa.run(s: List<&2, U32>, alive: Bool, +seq: List<&2, AaGTok>, bs: List<&2, Bool>) -> Bool:
184  match s:
185    case Nil{}:
186      AaGNfa.sem(seq, bs, Nil{})
187    case Con{h, t}:
188      match alive:
189        case False{}:
190          False{}
191        case True{}:
192          +n = AaGNfa.next(seq, bs, False{}, False{}, h)
193          AaGNfa.run(t, AaGNfa.alive(n), seq, n)
194
195def AaGNfa.falses(seq: List<&2, AaGTok>) -> List<&2, Bool>:
196  match seq:
197    case Nil{}:
198      [False{}]
199    case Con{t, r}:
200      Con{False{}, AaGNfa.falses(r)}
201
202# only the first position (the whole sequence) is active
203def AaGNfa.start(seq: List<&2, AaGTok>) -> List<&2, Bool>:
204  match seq:
205    case Nil{}:
206      [True{}]
207    case Con{t, r}:
208      Con{True{}, AaGNfa.falses(r)}
209
210# the matcher evaluation uses
211def AaGSeq.run(+seq: List<&2, AaGTok>, s: List<&2, U32>) -> Bool:
212  AaGNfa.run(s, True{}, seq, AaGNfa.start(seq))
213
214# The list model: a path matches a sequence of n tokens when it can be cut
215# into n pieces, in order, each matching its token
216
217# no byte of p is '/'
218def AaGPiece.no_slash(p: List<&2, U32>) -> Bool:
219  match p:
220    case Nil{}:
221      True{}
222    case Con{h, t}:
223      Bool.and(U32.is_ne(h, 47), AaGPiece.no_slash(t))
224
225# the piece p is one byte b for which ok holds
226def AaGPiece.one(ok: Bool, p: List<&2, U32>) -> Bool:
227  match p:
228    case Nil{}:
229      False{}
230    case Con{h, t}:
231      Bool.and(ok, X.AaText.is_nil(t))
232
233def AaGPiece.first(p: List<&2, U32>) -> U32:
234  match p:
235    case Nil{}:
236      0
237    case Con{h, t}:
238      h
239
240# the piece p matches the token
241def AaGTok.piece(tok: AaGTok, +p: List<&2, U32>) -> Bool:
242  match tok:
243    case AaGChar{c}:
244      AaGPiece.one(U32.is_eq(AaGPiece.first(p), c), p)
245    case AaGAny{}:
246      AaGPiece.one(U32.is_ne(AaGPiece.first(p), 47), p)
247    case AaGClass{neg, rs}:
248      AaGPiece.one(AaGClass.has(neg, rs, AaGPiece.first(p)), p)
249    case AaGStar{}:
250      AaGPiece.no_slash(p)
251    case AaGStar2{}:
252      True{}
253
254# the cuts with an empty first piece
255def AaGCuts.empty_first(ds: List<&2, List<&2, List<&2, U32>>>) -> List<&2, List<&2, List<&2, U32>>>:
256  match ds:
257    case Nil{}:
258      Nil{}
259    case Con{d, t}:
260      Con{Con{Nil{}, d}, AaGCuts.empty_first(t)}
261
262# the cuts with h put in front of the first piece
263def AaGCuts.grow(+h: U32, ds: List<&2, List<&2, List<&2, U32>>>) -> List<&2, List<&2, List<&2, U32>>>:
264  match ds:
265    case Nil{}:
266      Nil{}
267    case Con{d, t}:
268      match d:
269        case Nil{}:
270          AaGCuts.grow(h, t)
271        case Con{p, ps}:
272          Con{Con{Con{h, p}, ps}, AaGCuts.grow(h, t)}
273
274def AaGCuts.append(xs: List<&2, List<&2, List<&2, U32>>>, ys: List<&2, List<&2, List<&2, U32>>>) -> List<&2, List<&2, List<&2, U32>>>:
275  match xs:
276    case Nil{}:
277      ys
278    case Con{h, t}:
279      Con{h, AaGCuts.append(t, ys)}
280
281# every way to cut s into n pieces
282def AaGCuts.all(+n: Nat, s: List<&2, U32>) -> List<&2, List<&2, List<&2, U32>>>:
283  match n:
284    case 0n:
285      match s:
286        case Nil{}:
287          [Nil{}]
288        case Con{h, t}:
289          Nil{}
290    case 1n+p:
291      match s:
292        case Nil{}:
293          AaGCuts.empty_first(AaGCuts.all(p, Nil{}))
294        case Con{+h, +t}:
295          AaGCuts.append(AaGCuts.empty_first(AaGCuts.all(p, Con{h, t})), AaGCuts.grow(h, AaGCuts.all(n, t)))
296
297# the pieces d match the tokens one to one
298def AaGSeq.fits(+seq: List<&2, AaGTok>, d: List<&2, List<&2, U32>>) -> Bool:
299  match seq:
300    case Nil{}:
301      match d:
302        case Nil{}:
303          True{}
304        case Con{p, ps}:
305          False{}
306    case Con{tok, r}:
307      match d:
308        case Nil{}:
309          False{}
310        case Con{p, ps}:
311          Bool.and(AaGTok.piece(tok, p), AaGSeq.fits(r, ps))
312
313def AaGSeq.fits_any(+seq: List<&2, AaGTok>, ds: List<&2, List<&2, List<&2, U32>>>) -> Bool:
314  match ds:
315    case Nil{}:
316      False{}
317    case Con{d, t}:
318      Bool.or(AaGSeq.fits(seq, d), AaGSeq.fits_any(seq, t))
319
320def AaGSeq.len(seq: List<&2, AaGTok>) -> Nat:
321  match seq:
322    case Nil{}:
323      0n
324    case Con{t, r}:
325      1n+AaGSeq.len(r)
326
327def AaGSeq.model(+seq: List<&2, AaGTok>, s: List<&2, U32>) -> Bool:
328  AaGSeq.fits_any(seq, AaGCuts.all(AaGSeq.len(seq), s))
329
330# A whole pattern: some alternative matches
331
332def AaGlob.matches.go(alts: List<&2, List<&2, AaGTok>>, +s: List<&2, U32>) -> Bool:
333  match alts:
334    case Nil{}:
335      False{}
336    case Con{a, t}:
337      Bool.or(AaGSeq.run(a, s), AaGlob.matches.go(t, s))
338
339# the same with the backtracking matcher (the reference)
340def AaGlob.matches_ref.go(alts: List<&2, List<&2, AaGTok>>, +s: List<&2, U32>) -> Bool:
341  match alts:
342    case Nil{}:
343      False{}
344    case Con{a, t}:
345      Bool.or(AaGSeq.matches(a, s), AaGlob.matches_ref.go(t, s))
346
347def AaGlob.matches_ref(g: AaGlob, +s: List<&2, U32>) -> Bool:
348  match g:
349    case AaGlob{alts, literal}:
350      AaGlob.matches_ref.go(alts, s)
351
352def AaGlob.matches(g: AaGlob, +s: List<&2, U32>) -> Bool:
353  match g:
354    case AaGlob{alts, literal}:
355      AaGlob.matches.go(alts, s)
356
357def AaGlob.model.go(alts: List<&2, List<&2, AaGTok>>, +s: List<&2, U32>) -> Bool:
358  match alts:
359    case Nil{}:
360      False{}
361    case Con{a, t}:
362      Bool.or(AaGSeq.model(a, s), AaGlob.model.go(t, s))
363
364def AaGlob.model(g: AaGlob, +s: List<&2, U32>) -> Bool:
365  match g:
366    case AaGlob{alts, literal}:
367      AaGlob.model.go(alts, s)
368
369def AaGlob.is_literal(g: AaGlob) -> Bool:
370  match g:
371    case AaGlob{alts, literal}:
372      literal
373
374# How specific a match is, for choosing between attachments: a literal
375# pattern ranks above every other; otherwise the longest run of literal
376# bytes before the first wildcard, over the alternatives that match.
377
378def AaGSeq.prefix(seq: List<&2, AaGTok>) -> U32:
379  match seq:
380    case Nil{}:
381      0
382    case Con{t, r}:
383      match t:
384        case AaGChar{c}:
385          U32.add(1, AaGSeq.prefix(r))
386        case AaGAny{}:
387          0
388        case AaGClass{n, rs}:
389          0
390        case AaGStar{}:
391          0
392        case AaGStar2{}:
393          0
394
395def AaGlob.rank.max(+a: U32, +b: U32) -> U32:
396  Bool.pick(U32, U32.is_lt(a, b), b, a)
397
398def AaGlob.rank.go(alts: List<&2, List<&2, AaGTok>>, +s: List<&2, U32>, +best: U32) -> U32:
399  match alts:
400    case Nil{}:
401      best
402    case Con{+a, t}:
403      AaGlob.rank.go(t, s, Bool.pick(U32, AaGSeq.run(a, s), AaGlob.rank.max(best, U32.add(AaGSeq.prefix(a), 1)), best))
404
405# 0: no match; 1 + prefix length for a pattern; 1000000 for a literal match
406def AaGlob.rank(g: AaGlob, +s: List<&2, U32>) -> U32:
407  match g:
408    case AaGlob{alts, literal}:
409      match literal:
410        case True{}:
411          Bool.pick(U32, AaGlob.matches.go(alts, s), 1000000, 0)
412        case False{}:
413          AaGlob.rank.go(alts, s, 0)
414
415# Parsing a pattern's text (after variable expansion and unquoting)
416
417type AaGFlat is Data:
418  AaGFTok{t: AaGTok}
419  AaGFOpen{}
420  AaGFSep{}
421  AaGFClose{}
422
423type AaGMode is Data:
424  AaGMNorm{}
425  AaGMEsc{}
426  AaGMStar{}
427  AaGMClass{neg: Bool, first: Bool, rs: List<&2, AaGRange>, pend: Maybe<&2, U32>, dash: Bool}
428
429# the lexer's state: the mode, the character before the current one, whether
430# the last thing emitted is a '/' that a following '/' collapses into,
431# whether nothing has been emitted yet, the brace depth, the flat tokens
432# (last first), and whether the text is still well formed
433type AaGLex is Data:
434  AaGLex{mode: AaGMode, prev: U32, slash: Bool, start: Bool, depth: Nat, out: List<&2, AaGFlat>, ok: Bool}
435
436def AaGLex.fail(st: AaGLex) -> AaGLex:
437  match st:
438    case AaGLex{m, p, sl, st0, d, out, ok}:
439      AaGLex{AaGMNorm{}, p, sl, st0, d, out, False{}}
440
441def AaGLex.emit(st: AaGLex, f: AaGFlat, prev: U32) -> AaGLex:
442  match st:
443    case AaGLex{m, p, sl, st0, d, out, ok}:
444      AaGLex{AaGMNorm{}, prev, False{}, False{}, d, Con{f, out}, ok}
445
446def AaGLex.slash.go(sl: Bool, st: AaGLex) -> AaGLex:
447  match sl:
448    case True{}:
449      match st:
450        case AaGLex{m, p, sl2, st0, d, out, ok}:
451          AaGLex{AaGMNorm{}, 47, True{}, False{}, d, out, ok}
452    case False{}:
453      match st:
454        case AaGLex{m, p, sl2, +st0, d, out, ok}:
455          AaGLex{AaGMNorm{}, 47, Bool.not(st0), False{}, d, Con{AaGFTok{AaGChar{47}}, out}, ok}
456
457def AaGLex.slash(st: AaGLex) -> AaGLex:
458  match st:
459    case AaGLex{m, p, +sl, st0, d, out, ok}:
460      AaGLex.slash.go(sl, AaGLex{m, p, sl, st0, d, out, ok})
461
462def AaGLex.depth(st: AaGLex) -> Nat:
463  match st:
464    case AaGLex{m, p, sl, st0, d, out, ok}:
465      d
466
467def AaGLex.prev(st: AaGLex) -> U32:
468  match st:
469    case AaGLex{m, p, sl, st0, d, out, ok}:
470      p
471
472def AaGLex.set_mode(st: AaGLex, m: AaGMode) -> AaGLex:
473  match st:
474    case AaGLex{m0, p, sl, st0, d, out, ok}:
475      AaGLex{m, p, sl, st0, d, out, ok}
476
477def AaGLex.open(st: AaGLex) -> AaGLex:
478  match st:
479    case AaGLex{m, p, sl, st0, d, out, ok}:
480      AaGLex{AaGMNorm{}, 123, False{}, False{}, 1n+d, Con{AaGFOpen{}, out}, ok}
481
482def AaGLex.close.go(d: Nat, out: List<&2, AaGFlat>, ok: Bool, p: U32) -> AaGLex:
483  match d:
484    case 0n:
485      AaGLex{AaGMNorm{}, 125, False{}, False{}, 0n, out, False{}}
486    case 1n+e:
487      AaGLex{AaGMNorm{}, 125, False{}, False{}, e, Con{AaGFClose{}, out}, ok}
488
489def AaGLex.close(st: AaGLex) -> AaGLex:
490  match st:
491    case AaGLex{m, p, sl, st0, d, out, ok}:
492      AaGLex.close.go(d, out, ok, p)
493
494def AaGLex.comma.go(d: Nat, st: AaGLex) -> AaGLex:
495  match d:
496    case 0n:
497      AaGLex.emit(st, AaGFTok{AaGChar{44}}, 44)
498    case 1n+e:
499      AaGLex.emit(st, AaGFSep{}, 44)
500
501def AaGLex.comma(+st: AaGLex) -> AaGLex:
502  AaGLex.comma.go(AaGLex.depth(st), st)
503
504# a star or double star: after a '/', and before what `next` says, it stands
505# for one or more characters (a ? in front of it)
506def AaGLex.star.go(seg: Bool, st: AaGLex, t: AaGTok) -> AaGLex:
507  match seg:
508    case True{}:
509      AaGLex.emit(AaGLex.emit(st, AaGFTok{AaGAny{}}, 42), AaGFTok{t}, 42)
510    case False{}:
511      AaGLex.emit(st, AaGFTok{t}, 42)
512
513def AaGLex.star(+st: AaGLex, next: Bool) -> AaGLex:
514  AaGLex.star.go(Bool.and(U32.is_eq(AaGLex.prev(st), 47), next), st, AaGStar{})
515
516def AaGLex.star2(+st: AaGLex, next: Bool) -> AaGLex:
517  AaGLex.star.go(Bool.and(U32.is_eq(AaGLex.prev(st), 47), next), st, AaGStar2{})
518
519# what a character means in normal mode
520type AaGCh is Data:
521  AaGCLit{}
522  AaGCEsc{}
523  AaGCStar{}
524  AaGCAny{}
525  AaGCClass{}
526  AaGCOpen{}
527  AaGCComma{}
528  AaGCClose{}
529  AaGCBad{}
530  AaGCSlash{}
531
532def AaGCh.of(+h: U32) -> AaGCh:
533  Bool.pick(AaGCh, U32.is_eq(h, 92), AaGCEsc{}, Bool.pick(AaGCh, U32.is_eq(h, 42), AaGCStar{}, Bool.pick(AaGCh, U32.is_eq(h, 63), AaGCAny{}, Bool.pick(AaGCh, U32.is_eq(h, 91), AaGCClass{}, Bool.pick(AaGCh, U32.is_eq(h, 123), AaGCOpen{}, Bool.pick(AaGCh, U32.is_eq(h, 44), AaGCComma{}, Bool.pick(AaGCh, U32.is_eq(h, 125), AaGCClose{}, Bool.pick(AaGCh, U32.is_eq(h, 93), AaGCBad{}, Bool.pick(AaGCh, U32.is_eq(h, 47), AaGCSlash{}, AaGCLit{})))))))))
534
535def AaGLex.norm(k: AaGCh, +h: U32, st: AaGLex) -> AaGLex:
536  match k:
537    case AaGCLit{}:
538      AaGLex.emit(st, AaGFTok{AaGChar{h}}, h)
539    case AaGCEsc{}:
540      AaGLex.set_mode(st, AaGMEsc{})
541    case AaGCStar{}:
542      AaGLex.set_mode(st, AaGMStar{})
543    case AaGCAny{}:
544      AaGLex.emit(st, AaGFTok{AaGAny{}}, 63)
545    case AaGCClass{}:
546      AaGLex.set_mode(st, AaGMClass{False{}, True{}, Nil{}, None{}, False{}})
547    case AaGCOpen{}:
548      AaGLex.open(st)
549    case AaGCComma{}:
550      AaGLex.comma(st)
551    case AaGCClose{}:
552      AaGLex.close(st)
553    case AaGCBad{}:
554      AaGLex.fail(st)
555    case AaGCSlash{}:
556      AaGLex.slash(st)
557
558# Character classes: what a character means inside [...]
559type AaGK is Data:
560  AaGKClose{}
561  AaGKCaret{}
562  AaGKDash{}
563  AaGKBack{}
564  AaGKOther{}
565
566def AaGK.of(+h: U32) -> AaGK:
567  Bool.pick(AaGK, U32.is_eq(h, 93), AaGKClose{}, Bool.pick(AaGK, U32.is_eq(h, 94), AaGKCaret{}, Bool.pick(AaGK, U32.is_eq(h, 45), AaGKDash{}, Bool.pick(AaGK, U32.is_eq(h, 92), AaGKBack{}, AaGKOther{}))))
568
569def AaGClass.flush(rs: List<&2, AaGRange>, pend: Maybe<&2, U32>) -> List<&2, AaGRange>:
570  match pend:
571    case None{}:
572      rs
573    case Some{+c}:
574      Con{AaGRange{c, c}, rs}
575
576# a range lo-h, the dash seen: lo is pending
577def AaGClass.range(pend: Maybe<&2, U32>, h: U32, rs: List<&2, AaGRange>, st: AaGLex, neg: Bool) -> AaGLex:
578  match pend:
579    case None{}:
580      AaGLex.fail(st)
581    case Some{lo}:
582      AaGLex.set_mode(st, AaGMClass{neg, False{}, Con{AaGRange{lo, h}, rs}, None{}, False{}})
583
584def AaGClass.close.go(bad: Bool, st: AaGLex, neg: Bool, rs: List<&2, AaGRange>) -> AaGLex:
585  match bad:
586    case True{}:
587      AaGLex.fail(st)
588    case False{}:
589      AaGLex.emit(st, AaGFTok{AaGClass{neg, rs}}, 93)
590
591def AaGClass.other(dash: Bool, st: AaGLex, neg: Bool, rs: List<&2, AaGRange>, pend: Maybe<&2, U32>, h: U32) -> AaGLex:
592  match dash:
593    case True{}:
594      AaGClass.range(pend, h, rs, st, neg)
595    case False{}:
596      AaGLex.set_mode(st, AaGMClass{neg, False{}, AaGClass.flush(rs, pend), Some{h}, False{}})
597
598def AaGClass.caret.go(lit: Bool, st: AaGLex, neg: Bool, rs: List<&2, AaGRange>, pend: Maybe<&2, U32>, dash: Bool) -> AaGLex:
599  match lit:
600    case True{}:
601      AaGClass.other(dash, st, neg, rs, pend, 94)
602    case False{}:
603      AaGLex.set_mode(st, AaGMClass{True{}, True{}, rs, pend, dash})
604
605# k: 0 a literal '-' (first, or nothing pending), 1 the dash of a range, 2 a second dash
606def AaGClass.dash.go(k: Nat, st: AaGLex, neg: Bool, rs: List<&2, AaGRange>, pend: Maybe<&2, U32>) -> AaGLex:
607  match k:
608    case 0n:
609      AaGLex.set_mode(st, AaGMClass{neg, False{}, AaGClass.flush(rs, pend), Some{45}, False{}})
610    case 1n+j:
611      match j:
612        case 0n:
613          AaGLex.set_mode(st, AaGMClass{neg, False{}, rs, pend, True{}})
614        case 1n+i:
615          AaGLex.fail(st)
616
617def AaGClass.dash.kind(first: Bool, dash: Bool, pend: Maybe<&2, U32>) -> Nat:
618  match first:
619    case True{}:
620      0n
621    case False{}:
622      match dash:
623        case True{}:
624          2n
625        case False{}:
626          match pend:
627            case None{}:
628              0n
629            case Some{c}:
630              1n
631
632def AaGClass.step(k: AaGK, +h: U32, st: AaGLex, +neg: Bool, +first: Bool, +rs: List<&2, AaGRange>, +pend: Maybe<&2, U32>, +dash: Bool) -> AaGLex:
633  match k:
634    case AaGKClose{}:
635      AaGClass.close.go(Bool.or(first, dash), st, neg, AaGClass.flush(rs, pend))
636    case AaGKCaret{}:
637      AaGClass.caret.go(Bool.or(neg, Bool.not(first)), st, neg, rs, pend, dash)
638    case AaGKDash{}:
639      AaGClass.dash.go(AaGClass.dash.kind(first, dash, pend), st, neg, rs, pend)
640    case AaGKBack{}:
641      AaGLex.fail(st)
642    case AaGKOther{}:
643      AaGClass.other(dash, st, neg, rs, pend, h)
644
645def AaGLex.step.star(two: Bool, st: AaGLex, +h: U32, +next: U32) -> AaGLex:
646  match two:
647    case True{}:
648      AaGLex.star2(st, Bool.or(U32.is_eq(next, 47), Bool.or(U32.is_eq(next, 42), U32.is_eq(next, 0))))
649    case False{}:
650      AaGLex.norm(AaGCh.of(h), h, AaGLex.star(st, U32.is_eq(h, 47)))
651
652# one character, in the current mode; next is the character after it (0 at the end)
653def AaGLex.step.mode(m: AaGMode, st: AaGLex, +h: U32, +next: U32) -> AaGLex:
654  match m:
655    case AaGMNorm{}:
656      AaGLex.norm(AaGCh.of(h), h, st)
657    case AaGMEsc{}:
658      AaGLex.emit(st, AaGFTok{AaGChar{h}}, h)
659    case AaGMStar{}:
660      AaGLex.step.star(U32.is_eq(h, 42), st, h, next)
661    case AaGMClass{neg, first, rs, pend, dash}:
662      AaGClass.step(AaGK.of(h), h, st, neg, first, rs, pend, dash)
663
664def AaGLex.step(st: AaGLex, +h: U32, +next: U32) -> AaGLex:
665  match st:
666    case AaGLex{m, p, sl, st0, d, out, ok}:
667      AaGLex.step.mode(m, AaGLex{AaGMNorm{}, p, sl, st0, d, out, ok}, h, next)
668
669def AaGLex.finish(st: AaGLex) -> AaGLex:
670  match st:
671    case AaGLex{m, p, sl, st0, d, out, ok}:
672      match m:
673        case AaGMNorm{}:
674          AaGLex{AaGMNorm{}, p, sl, st0, d, out, ok}
675        case AaGMEsc{}:
676          AaGLex{AaGMNorm{}, p, sl, st0, d, out, False{}}
677        case AaGMStar{}:
678          AaGLex.star(AaGLex{AaGMNorm{}, p, sl, st0, d, out, ok}, True{})
679        case AaGMClass{n, f, rs, pe, da}:
680          AaGLex{AaGMNorm{}, p, sl, st0, d, out, False{}}
681
682def AaGLex.run(xs: List<&2, U32>, st: AaGLex) -> AaGLex:
683  match xs:
684    case Nil{}:
685      AaGLex.finish(st)
686    case Con{+h, +t}:
687      AaGLex.run(t, AaGLex.step(st, h, X.AaText.head(t)))
688
689# Brace expansion of the flat tokens. Sequences are built last token first.
690
691type AaGFrame is Data:
692  AaGFrame{outer: List<&2, List<&2, AaGTok>>, done: List<&2, List<&2, AaGTok>>, n: Nat}
693
694type AaGExp is Data:
695  AaGExp{cur: List<&2, List<&2, AaGTok>>, frames: List<&2, AaGFrame>, ok: Bool}
696
697def AaGSeqs.cons(+t: AaGTok, xs: List<&2, List<&2, AaGTok>>) -> List<&2, List<&2, AaGTok>>:
698  match xs:
699    case Nil{}:
700      Nil{}
701    case Con{h, r}:
702      Con{Con{t, h}, AaGSeqs.cons(t, r)}
703
704def AaGSeqs.append(xs: List<&2, List<&2, AaGTok>>, ys: List<&2, List<&2, AaGTok>>) -> List<&2, List<&2, AaGTok>>:
705  match xs:
706    case Nil{}:
707      ys
708    case Con{h, t}:
709      Con{h, AaGSeqs.append(t, ys)}
710
711def AaGSeq.append(xs: List<&2, AaGTok>, ys: List<&2, AaGTok>) -> List<&2, AaGTok>:
712  match xs:
713    case Nil{}:
714      ys
715    case Con{h, t}:
716      Con{h, AaGSeq.append(t, ys)}
717
718def AaGSeq.rev_onto(xs: List<&2, AaGTok>, acc: List<&2, AaGTok>) -> List<&2, AaGTok>:
719  match xs:
720    case Nil{}:
721      acc
722    case Con{h, t}:
723      AaGSeq.rev_onto(t, Con{h, acc})
724
725def AaGSeqs.rev(xs: List<&2, List<&2, AaGTok>>) -> List<&2, List<&2, AaGTok>>:
726  match xs:
727    case Nil{}:
728      Nil{}
729    case Con{h, t}:
730      Con{AaGSeq.rev_onto(h, Nil{}), AaGSeqs.rev(t)}
731
732# every a ++ o, a an alternative and o an outer prefix (both last token first)
733def AaGSeqs.after(+a: List<&2, AaGTok>, os: List<&2, List<&2, AaGTok>>) -> List<&2, List<&2, AaGTok>>:
734  match os:
735    case Nil{}:
736      Nil{}
737    case Con{o, t}:
738      Con{AaGSeq.append(a, o), AaGSeqs.after(a, t)}
739
740def AaGSeqs.product(alts: List<&2, List<&2, AaGTok>>, +os: List<&2, List<&2, AaGTok>>) -> List<&2, List<&2, AaGTok>>:
741  match alts:
742    case Nil{}:
743      Nil{}
744    case Con{a, t}:
745      AaGSeqs.append(AaGSeqs.after(a, os), AaGSeqs.product(t, os))
746
747def AaGExp.sep(fs: List<&2, AaGFrame>, cur: List<&2, List<&2, AaGTok>>, ok: Bool) -> AaGExp:
748  match fs:
749    case Nil{}:
750      AaGExp{cur, Nil{}, False{}}
751    case Con{f, rest}:
752      match f:
753        case AaGFrame{o, d, n}:
754          AaGExp{[Nil{}], Con{AaGFrame{o, AaGSeqs.append(d, cur), 1n+n}, rest}, ok}
755
756def AaGExp.close.go(n: Nat, o: List<&2, List<&2, AaGTok>>, alts: List<&2, List<&2, AaGTok>>, rest: List<&2, AaGFrame>, ok: Bool) -> AaGExp:
757  match n:
758    case 0n:
759      AaGExp{o, rest, False{}}
760    case 1n+m:
761      AaGExp{AaGSeqs.product(alts, o), rest, ok}
762
763def AaGExp.close(fs: List<&2, AaGFrame>, cur: List<&2, List<&2, AaGTok>>, ok: Bool) -> AaGExp:
764  match fs:
765    case Nil{}:
766      AaGExp{cur, Nil{}, False{}}
767    case Con{f, rest}:
768      match f:
769        case AaGFrame{o, d, n}:
770          AaGExp.close.go(n, o, AaGSeqs.append(d, cur), rest, ok)
771
772def AaGExp.step(e: AaGExp, f: AaGFlat) -> AaGExp:
773  match e:
774    case AaGExp{cur, fs, ok}:
775      match f:
776        case AaGFTok{t}:
777          AaGExp{AaGSeqs.cons(t, cur), fs, ok}
778        case AaGFOpen{}:
779          AaGExp{[Nil{}], Con{AaGFrame{cur, Nil{}, 0n}, fs}, ok}
780        case AaGFSep{}:
781          AaGExp.sep(fs, cur, ok)
782        case AaGFClose{}:
783          AaGExp.close(fs, cur, ok)
784
785def AaGExp.run(xs: List<&2, AaGFlat>, e: AaGExp) -> AaGExp:
786  match xs:
787    case Nil{}:
788      e
789    case Con{f, t}:
790      AaGExp.run(t, AaGExp.step(e, f))
791
792def AaGFlat.rev_onto(xs: List<&2, AaGFlat>, acc: List<&2, AaGFlat>) -> List<&2, AaGFlat>:
793  match xs:
794    case Nil{}:
795      acc
796    case Con{h, t}:
797      AaGFlat.rev_onto(t, Con{h, acc})
798
799def AaGTok.is_char(t: AaGTok) -> Bool:
800  match t:
801    case AaGChar{c}:
802      True{}
803    case AaGAny{}:
804      False{}
805    case AaGClass{n, rs}:
806      False{}
807    case AaGStar{}:
808      False{}
809    case AaGStar2{}:
810      False{}
811
812# every flat token is a literal character
813def AaGFlat.literal(xs: List<&2, AaGFlat>) -> Bool:
814  match xs:
815    case Nil{}:
816      True{}
817    case Con{f, t}:
818      match f:
819        case AaGFTok{tok}:
820          Bool.and(AaGTok.is_char(tok), AaGFlat.literal(t))
821        case AaGFOpen{}:
822          False{}
823        case AaGFSep{}:
824          False{}
825        case AaGFClose{}:
826          False{}
827
828def AaGlob.of_exp.go(ok: Bool, cur: List<&2, List<&2, AaGTok>>, lit: Bool) -> Maybe<&2, AaGlob>:
829  match ok:
830    case True{}:
831      Some{AaGlob{AaGSeqs.rev(cur), lit}}
832    case False{}:
833      None{}
834
835def AaGlob.of_exp(e: AaGExp, lit: Bool) -> Maybe<&2, AaGlob>:
836  match e:
837    case AaGExp{cur, fs, ok}:
838      match fs:
839        case Nil{}:
840          AaGlob.of_exp.go(ok, cur, lit)
841        case Con{f, r}:
842          None{}
843
844def AaGlob.of_flat(+flat: List<&2, AaGFlat>) -> Maybe<&2, AaGlob>:
845  AaGlob.of_exp(AaGExp.run(flat, AaGExp{[Nil{}], Nil{}, True{}}), AaGFlat.literal(flat))
846
847def AaGlob.of_lex(st: AaGLex) -> Maybe<&2, AaGlob>:
848  match st:
849    case AaGLex{m, p, sl, st0, d, out, ok}:
850      match d:
851        case 0n:
852          match ok:
853            case True{}:
854              AaGlob.of_flat(AaGFlat.rev_onto(out, Nil{}))
855            case False{}:
856              None{}
857        case 1n+e:
858          None{}
859
860# the pattern written as the text xs, or None if it is malformed
861def AaGlob.parse(xs: List<&2, U32>) -> Maybe<&2, AaGlob>:
862  AaGlob.of_lex(AaGLex.run(xs, AaGLex{AaGMNorm{}, 0, False{}, True{}, 0n, Nil{}, True{}}))
863
864# a pattern matching exactly the bytes xs (no wildcards)
865def AaGSeq.literal(xs: List<&2, U32>) -> List<&2, AaGTok>:
866  match xs:
867    case Nil{}:
868      Nil{}
869    case Con{h, t}:
870      Con{AaGChar{h}, AaGSeq.literal(t)}
871
872def AaGlob.literal(xs: List<&2, U32>) -> AaGlob:
873  AaGlob{[AaGSeq.literal(xs)], True{}}
874
875# the pattern that matches every string
876def AaGlob.all() -> AaGlob:
877  AaGlob{[[AaGStar2{}]], False{}}
878
879def AaGlob.match_text.go(m: Maybe<&2, AaGlob>, +s: List<&2, U32>) -> Bool:
880  match m:
881    case None{}:
882      False{}
883    case Some{g}:
884      AaGlob.matches(g, s)
885
886# the pattern written as p (False if it is malformed) matches s
887def AaGlob.match_text(p: List<&2, U32>, +s: List<&2, U32>) -> Bool:
888  AaGlob.match_text.go(AaGlob.parse(p), s)