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).
28	import Base
29	import ./text.bend as X
30	
31	type AaGRange is Data:
32	  AaGRange{lo: U32, hi: U32}
33	
34	type AaGTok is Data:
35	  AaGChar{c: U32}
36	  AaGAny{}
37	  AaGClass{neg: Bool, ranges: List<&2, AaGRange>}
38	  AaGStar{}
39	  AaGStar2{}
40	
41	type AaGlob is Data:
42	  AaGlob{alts: List<&2, List<&2, AaGTok>>, literal: Bool}
43	
44	# Character classes
45	
46	def 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	
51	def 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	
58	def 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	
67	def 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	
109	def AaGNfa.hd(bs: List<&2, Bool>) -> Bool:
110	  match bs:
111	    case Nil{}:
112	      False{}
113	    case Con{b, t}:
114	      b
115	
116	def 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)
124	def 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
134	def 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
146	def 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
157	def 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
165	def 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
173	def 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.
183	def 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	
195	def 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
203	def 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
211	def 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 '/'
218	def 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
226	def 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	
233	def 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
241	def 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
255	def 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
263	def 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	
274	def 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
282	def 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
298	def 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	
313	def 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	
320	def 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	
327	def 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	
332	def 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)
340	def 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	
347	def 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	
352	def AaGlob.matches(g: AaGlob, +s: List<&2, U32>) -> Bool:
353	  match g:
354	    case AaGlob{alts, literal}:
355	      AaGlob.matches.go(alts, s)
356	
357	def 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	
364	def AaGlob.model(g: AaGlob, +s: List<&2, U32>) -> Bool:
365	  match g:
366	    case AaGlob{alts, literal}:
367	      AaGlob.model.go(alts, s)
368	
369	def 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	
378	def 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	
395	def AaGlob.rank.max(+a: U32, +b: U32) -> U32:
396	  Bool.pick(U32, U32.is_lt(a, b), b, a)
397	
398	def 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
406	def 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	
417	type AaGFlat is Data:
418	  AaGFTok{t: AaGTok}
419	  AaGFOpen{}
420	  AaGFSep{}
421	  AaGFClose{}
422	
423	type 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
433	type AaGLex is Data:
434	  AaGLex{mode: AaGMode, prev: U32, slash: Bool, start: Bool, depth: Nat, out: List<&2, AaGFlat>, ok: Bool}
435	
436	def 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	
441	def 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	
446	def 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	
457	def 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	
462	def AaGLex.depth(st: AaGLex) -> Nat:
463	  match st:
464	    case AaGLex{m, p, sl, st0, d, out, ok}:
465	      d
466	
467	def AaGLex.prev(st: AaGLex) -> U32:
468	  match st:
469	    case AaGLex{m, p, sl, st0, d, out, ok}:
470	      p
471	
472	def 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	
477	def 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	
482	def 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	
489	def 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	
494	def 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	
501	def 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)
506	def 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	
513	def AaGLex.star(+st: AaGLex, next: Bool) -> AaGLex:
514	  AaGLex.star.go(Bool.and(U32.is_eq(AaGLex.prev(st), 47), next), st, AaGStar{})
515	
516	def 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
520	type AaGCh is Data:
521	  AaGCLit{}
522	  AaGCEsc{}
523	  AaGCStar{}
524	  AaGCAny{}
525	  AaGCClass{}
526	  AaGCOpen{}
527	  AaGCComma{}
528	  AaGCClose{}
529	  AaGCBad{}
530	  AaGCSlash{}
531	
532	def 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	
535	def 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 [...]
559	type AaGK is Data:
560	  AaGKClose{}
561	  AaGKCaret{}
562	  AaGKDash{}
563	  AaGKBack{}
564	  AaGKOther{}
565	
566	def 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	
569	def 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
577	def 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	
584	def 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	
591	def 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	
598	def 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
606	def 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	
617	def 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	
632	def 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	
645	def 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)
653	def 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	
664	def 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	
669	def 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	
682	def 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	
691	type AaGFrame is Data:
692	  AaGFrame{outer: List<&2, List<&2, AaGTok>>, done: List<&2, List<&2, AaGTok>>, n: Nat}
693	
694	type AaGExp is Data:
695	  AaGExp{cur: List<&2, List<&2, AaGTok>>, frames: List<&2, AaGFrame>, ok: Bool}
696	
697	def 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	
704	def 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	
711	def 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	
718	def 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	
725	def 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)
733	def 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	
740	def 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	
747	def 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	
756	def 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	
763	def 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	
772	def 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	
785	def 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	
792	def 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	
799	def 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
813	def 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	
828	def 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	
835	def 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	
844	def 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	
847	def 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
861	def 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)
865	def 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	
872	def AaGlob.literal(xs: List<&2, U32>) -> AaGlob:
873	  AaGlob{[AaGSeq.literal(xs)], True{}}
874	
875	# the pattern that matches every string
876	def AaGlob.all() -> AaGlob:
877	  AaGlob{[[AaGStar2{}]], False{}}
878	
879	def 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
887	def AaGlob.match_text(p: List<&2, U32>, +s: List<&2, U32>) -> Bool:
888	  AaGlob.match_text.go(AaGlob.parse(p), s)