1	# bend-osdev-apparmor: loading policy text (apparmor.d(5), "FORMAT").
2	#
3	# 1. Each file's text is split into tokens (token.bend), and the tokens into
4	#    items: statements ending at a comma, variable assignments (which end at
5	#    the end of their line), includes, and block openings and closings.
6	# 2. Includes are replaced by the items of the included file, taken from the
7	#    file map: <name> and "name" both look up name. An include is expanded
8	#    at most once in each block (the file's top level, each profile, hat or
9	#    qualifier block), so including a file twice is including it once and
10	#    include cycles end (apparmor_parser 4.0.1 does the same; see the
11	#    README, "Experiments"). A missing file fails unless the include says
12	#    `if exists`.
13	# 3. The preamble (before the first profile) assigns variables, @{NAME} =
14	#    values or += values, and declares aliases, alias /from/ -> /to/,; abi
15	#    statements are accepted and ignored.
16	# 4. Profiles are built: headers, flags, rules (with variables expanded:
17	#    one value as itself, several as {v1,v2}; a value's trailing '/' is
18	#    dropped before a '/'; @{profile_name} is the profile's full name),
19	#    child profiles and hats, and qualifier blocks. An alias adds, for each
20	#    file rule whose pattern starts with its source, a copy starting with
21	#    its target. Two rules on the same literal path with different exec
22	#    modes fail.
23	import Base
24	import ./text.bend as X
25	import ./glob.bend as G
26	import ./perm.bend as P
27	import ./token.bend as T
28	import ./error.bend as E
29	import ./options.bend as O
30	import ./profile.bend as PR
31	import ./rule.bend as R
32	import ./rule_file.bend as F
33	import ./rule_capability.bend as RC
34	import ./rule_network.bend as RN
35	import ./rule_signal.bend as RS
36	import ./rule_ptrace.bend as RP
37	import ./rule_mount.bend as RM
38	import ./rule_dbus.bend as RD
39	import ./rule_change_profile.bend as RX
40	
41	# a file of the file map: its name (as includes name it) and its text
42	type AaSrcFile is Data:
43	  AaSrcFile{name: List<&2, U32>, text: List<&2, U32>}
44	
45	# Items
46	
47	type AaItem is Data:
48	  AaIStmt{toks: List<&2, T.AaTok>, src: E.AaSrc}
49	  AaIVar{toks: List<&2, T.AaTok>, src: E.AaSrc}
50	  AaIInclude{name: List<&2, U32>, optional: Bool, src: E.AaSrc}
51	  AaIOpen{toks: List<&2, T.AaTok>, src: E.AaSrc}
52	  AaIClose{src: E.AaSrc}
53	  AaIError{err: E.AaError}
54	
55	def AaItem.rev_onto(xs: List<&2, AaItem>, acc: List<&2, AaItem>) -> List<&2, AaItem>:
56	  match xs:
57	    case Nil{}:
58	      acc
59	    case Con{h, t}:
60	      AaItem.rev_onto(t, Con{h, acc})
61	
62	# The itemizer. Modes: normal; a candidate variable assignment (the word
63	# @{NAME} alone, waiting to see = or +=); a variable assignment on a line;
64	# an include waiting for its path (stage 0), after `if` (1), after `if exists` (2).
65	type AaItMode is Data:
66	  AaImNorm{}
67	  AaImVarCand{line: U32}
68	  AaImVar{line: U32}
69	  AaImInc{stage: Nat, line: U32}
70	
71	type AaItB is Data:
72	  AaItB{file: List<&2, U32>, mode: AaItMode, pend: List<&2, T.AaTok>, pdepth: Nat, out: List<&2, AaItem>}
73	
74	def AaItB.src(+file: List<&2, U32>, line: U32) -> E.AaSrc:
75	  E.AaSrc{file, line}
76	
77	def AaItB.emit(b: AaItB, it: AaItem) -> AaItB:
78	  match b:
79	    case AaItB{f, m, pe, pd, out}:
80	      AaItB{f, AaImNorm{}, Nil{}, pd, Con{it, out}}
81	
82	def AaItB.err(b: AaItB, e: E.AaError) -> AaItB:
83	  AaItB.emit(b, AaIError{e})
84	
85	def AaItB.push(b: AaItB, t: T.AaTok) -> AaItB:
86	  match b:
87	    case AaItB{f, m, pe, pd, out}:
88	      AaItB{f, m, Con{t, pe}, pd, out}
89	
90	def AaItB.mode(b: AaItB, m: AaItMode) -> AaItB:
91	  match b:
92	    case AaItB{f, m0, pe, pd, out}:
93	      AaItB{f, m, pe, pd, out}
94	
95	def AaItB.file(b: AaItB) -> List<&2, U32>:
96	  match b:
97	    case AaItB{f, m, pe, pd, out}:
98	      f
99	
100	def AaItB.pend_empty(b: AaItB) -> Bool:
101	  match b:
102	    case AaItB{f, m, pe, pd, out}:
103	      match pe:
104	        case Nil{}:
105	          True{}
106	        case Con{h, t}:
107	          False{}
108	
109	def AaItB.pdepth(b: AaItB) -> Nat:
110	  match b:
111	    case AaItB{f, m, pe, pd, out}:
112	      pd
113	
114	def AaItB.paren(b: AaItB, up: Bool, t: T.AaTok) -> AaItB:
115	  match b:
116	    case AaItB{f, m, pe, pd, out}:
117	      match up:
118	        case True{}:
119	          AaItB{f, m, Con{t, pe}, 1n+pd, out}
120	        case False{}:
121	          AaItB{f, m, Con{t, pe}, Nat.sub(pd, 1n), out}
122	
123	def AaItB.flush.item(kind: Nat, ts: List<&2, T.AaTok>, src: E.AaSrc) -> AaItem:
124	  match kind:
125	    case 0n:
126	      AaIStmt{ts, src}
127	    case 1n+k:
128	      match k:
129	        case 0n:
130	          AaIOpen{ts, src}
131	        case 1n+j:
132	          AaIVar{ts, src}
133	
134	# the pending tokens become an item: 0 a statement, 1 a block opening, 2 an assignment
135	def AaItB.flush(b: AaItB, kind: Nat, line: U32) -> AaItB:
136	  match b:
137	    case AaItB{+f, m, pe, pd, out}:
138	      AaItB{f, AaImNorm{}, Nil{}, pd, Con{AaItB.flush.item(kind, T.AaTok.rev_onto(pe, Nil{}), E.AaSrc{f, line}), out}}
139	
140	# a word starting @{: 0 not a variable word, 1 exactly @{NAME}, 2 @{NAME}= or @{NAME}+= with more
141	def AaIt.var_kind.rest(+r: List<&2, U32>) -> Nat:
142	  match r:
143	    case Nil{}:
144	      1n
145	    case Con{h, t}:
146	      Bool.pick(Nat, Bool.or(X.AaText.starts(r, "="), X.AaText.starts(r, "+=")), 2n, 0n)
147	
148	def AaIt.after_close(xs: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
149	  match xs:
150	    case Nil{}:
151	      None{}
152	    case Con{+h, +t}:
153	      Bool.pick(Maybe<&2, List<&2, U32>>, U32.is_eq(h, 125), Some{t}, AaIt.after_close(t))
154	
155	def AaIt.var_kind.go(m: Maybe<&2, List<&2, U32>>) -> Nat:
156	  match m:
157	    case None{}:
158	      0n
159	    case Some{r}:
160	      AaIt.var_kind.rest(r)
161	
162	def AaIt.var_kind(+w: List<&2, U32>) -> Nat:
163	  Bool.pick(Nat, X.AaText.starts(w, "@{"), AaIt.var_kind.go(AaIt.after_close(w)), 0n)
164	
165	def AaIt.is_include(t: T.AaTok) -> Bool:
166	  match t:
167	    case T.AaTWord{+w, l}:
168	      Bool.or(X.AaText.is(w, "#include"), X.AaText.is(w, "include"))
169	    case _:
170	      False{}
171	
172	# a token in normal mode
173	def AaItB.norm.word(k: Nat, +b: AaItB, t: T.AaTok, +line: U32) -> AaItB:
174	  match k:
175	    case 0n:
176	      AaItB.push(b, t)
177	    case 1n+k1:
178	      match k1:
179	        case 0n:
180	          AaItB.mode(AaItB.push(b, t), AaImVarCand{line})
181	        case 1n+k2:
182	          AaItB.mode(AaItB.push(b, t), AaImVar{line})
183	
184	def AaItB.norm.first(t: T.AaTok, +b: AaItB) -> AaItB:
185	  match t:
186	    case T.AaTWord{+w, +l}:
187	      Bool.pick(AaItB, AaIt.is_include(T.AaTWord{w, l}), AaItB.mode(b, AaImInc{0n, l}), AaItB.norm.word(AaIt.var_kind(w), b, T.AaTWord{w, l}, l))
188	    case _:
189	      AaItB.push(b, t)
190	
191	def AaItB.norm.open(depth0: Bool, +b: AaItB, t: T.AaTok, +l: U32) -> AaItB:
192	  match depth0:
193	    case True{}:
194	      AaItB.flush(b, 1n, l)
195	    case False{}:
196	      AaItB.push(b, t)
197	
198	def AaItB.norm.close(depth0: Bool, empty: Bool, +b: AaItB, t: T.AaTok, +l: U32) -> AaItB:
199	  match depth0:
200	    case True{}:
201	      match empty:
202	        case True{}:
203	          AaItB.emit(b, AaIClose{E.AaSrc{AaItB.file(b), l}})
204	        case False{}:
205	          AaItB.err(b, E.AaErrSyntax{AaItB.file(b), l})
206	    case False{}:
207	      AaItB.push(b, t)
208	
209	def AaItB.norm.comma(depth0: Bool, empty: Bool, +b: AaItB, t: T.AaTok, +l: U32) -> AaItB:
210	  match depth0:
211	    case True{}:
212	      match empty:
213	        case True{}:
214	          AaItB.err(b, E.AaErrSyntax{AaItB.file(b), l})
215	        case False{}:
216	          AaItB.flush(b, 0n, l)
217	    case False{}:
218	      AaItB.push(b, t)
219	
220	def AaItB.norm.go(t: T.AaTok, +d0: Bool, +empty: Bool, +b: AaItB) -> AaItB:
221	  match t:
222	    case T.AaTOpen{+l}:
223	      AaItB.norm.open(d0, b, T.AaTOpen{l}, l)
224	    case T.AaTClose{+l}:
225	      AaItB.norm.close(d0, empty, b, T.AaTClose{l}, l)
226	    case T.AaTComma{+l}:
227	      AaItB.norm.comma(d0, empty, b, T.AaTComma{l}, l)
228	    case T.AaTLParen{l}:
229	      AaItB.paren(b, True{}, T.AaTLParen{l})
230	    case T.AaTRParen{l}:
231	      AaItB.paren(b, False{}, T.AaTRParen{l})
232	    case T.AaTWord{+w, +l}:
233	      Bool.pick(AaItB, Bool.and(d0, empty), AaItB.norm.first(T.AaTWord{w, l}, b), AaItB.push(b, T.AaTWord{w, l}))
234	    case T.AaTQuoted{q, l}:
235	      AaItB.push(b, T.AaTQuoted{q, l})
236	
237	def AaItB.norm(+b: AaItB, t: T.AaTok) -> AaItB:
238	  AaItB.norm.go(t, Nat.is_eq(AaItB.pdepth(b), 0n), AaItB.pend_empty(b), b)
239	
240	# after @{NAME}: = or += makes it an assignment; anything else a rule
241	def AaItB.varcand(+b: AaItB, t: T.AaTok, +line: U32) -> AaItB:
242	  match t:
243	    case T.AaTWord{+w, +l}:
244	      Bool.pick(AaItB, Bool.or(X.AaText.starts(w, "="), X.AaText.starts(w, "+=")), AaItB.mode(AaItB.push(b, T.AaTWord{w, l}), AaImVar{line}), AaItB.norm(AaItB.mode(b, AaImNorm{}), T.AaTWord{w, l}))
245	    case _:
246	      AaItB.norm(AaItB.mode(b, AaImNorm{}), t)
247	
248	# an assignment takes the tokens of its line; a comma there is an error
249	def AaItB.var.same(same: Bool, +b: AaItB, t: T.AaTok, +line: U32) -> AaItB:
250	  match same:
251	    case True{}:
252	      match t:
253	        case T.AaTWord{w, l}:
254	          AaItB.push(b, T.AaTWord{w, l})
255	        case T.AaTQuoted{q, l}:
256	          AaItB.push(b, T.AaTQuoted{q, l})
257	        case _:
258	          AaItB.err(b, E.AaErrSyntax{AaItB.file(b), line})
259	    case False{}:
260	      AaItB.norm(AaItB.flush(b, 2n, line), t)
261	
262	def AaItB.var(+b: AaItB, +t: T.AaTok, +line: U32) -> AaItB:
263	  AaItB.var.same(U32.is_eq(T.AaTok.line(t), line), b, t, line)
264	
265	# the name inside <...>
266	def AaIt.magic(+w: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
267	  Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(U32.is_eq(X.AaText.head(w), 60), U32.is_eq(X.AaText.last(w, 0), 62)), Some{X.AaText.init(X.AaText.tail(w))}, None{})
268	
269	def AaItB.inc.magic(m: Maybe<&2, List<&2, U32>>, +b: AaItB, opt: Bool, +line: U32) -> AaItB:
270	  match m:
271	    case None{}:
272	      AaItB.err(b, E.AaErrSyntax{AaItB.file(b), line})
273	    case Some{n}:
274	      AaItB.emit(b, AaIInclude{n, opt, E.AaSrc{AaItB.file(b), line}})
275	
276	def AaItB.inc.path(+b: AaItB, t: T.AaTok, +opt: Bool, +line: U32) -> AaItB:
277	  match t:
278	    case T.AaTWord{w, l}:
279	      AaItB.inc.magic(AaIt.magic(w), b, opt, line)
280	    case T.AaTQuoted{q, l}:
281	      AaItB.emit(b, AaIInclude{q, opt, E.AaSrc{AaItB.file(b), line}})
282	    case _:
283	      AaItB.err(b, E.AaErrSyntax{AaItB.file(b), line})
284	
285	def AaItB.inc(stage: Nat, +b: AaItB, +t: T.AaTok, +line: U32) -> AaItB:
286	  match stage:
287	    case 0n:
288	      Bool.pick(AaItB, T.AaTok.is(t, "if"), AaItB.mode(b, AaImInc{1n, line}), AaItB.inc.path(b, t, False{}, line))
289	    case 1n+s:
290	      match s:
291	        case 0n:
292	          Bool.pick(AaItB, T.AaTok.is(t, "exists"), AaItB.mode(b, AaImInc{2n, line}), AaItB.err(b, E.AaErrSyntax{AaItB.file(b), line}))
293	        case 1n+r:
294	          AaItB.inc.path(b, t, True{}, line)
295	
296	def AaItB.step(b: AaItB, +t: T.AaTok) -> AaItB:
297	  match b:
298	    case AaItB{f, m, pe, pd, out}:
299	      match m:
300	        case AaImNorm{}:
301	          AaItB.norm(AaItB{f, AaImNorm{}, pe, pd, out}, t)
302	        case AaImVarCand{+l}:
303	          AaItB.varcand(AaItB{f, AaImVarCand{l}, pe, pd, out}, t, l)
304	        case AaImVar{+l}:
305	          AaItB.var(AaItB{f, AaImVar{l}, pe, pd, out}, t, l)
306	        case AaImInc{+s, +l}:
307	          AaItB.inc(s, AaItB{f, AaImInc{s, l}, pe, pd, out}, t, l)
308	
309	def AaItB.run(ts: List<&2, T.AaTok>, b: AaItB) -> AaItB:
310	  match ts:
311	    case Nil{}:
312	      b
313	    case Con{t, rest}:
314	      AaItB.run(rest, AaItB.step(b, t))
315	
316	def AaItB.finish(b: AaItB) -> List<&2, AaItem>:
317	  match b:
318	    case AaItB{+f, m, pe, pd, out}:
319	      match m:
320	        case AaImNorm{}:
321	          match pe:
322	            case Nil{}:
323	              AaItem.rev_onto(out, Nil{})
324	            case Con{h, t}:
325	              AaItem.rev_onto(Con{AaIError{E.AaErrSyntax{f, T.AaTok.line(h)}}, out}, Nil{})
326	        case AaImVarCand{+l}:
327	          AaItem.rev_onto(Con{AaIError{E.AaErrSyntax{f, l}}, out}, Nil{})
328	        case AaImVar{+l}:
329	          AaItem.rev_onto(Con{AaIVar{T.AaTok.rev_onto(pe, Nil{}), E.AaSrc{f, l}}, out}, Nil{})
330	        case AaImInc{+s, +l}:
331	          AaItem.rev_onto(Con{AaIError{E.AaErrSyntax{f, l}}, out}, Nil{})
332	
333	def AaIt.of_lex(r: Result<&2, &2, U32, List<&2, T.AaTok>>, +file: List<&2, U32>) -> List<&2, AaItem>:
334	  match r:
335	    case Fail{l}:
336	      [AaIError{E.AaErrLex{file, l}}]
337	    case Done{ts}:
338	      AaItB.finish(AaItB.run(ts, AaItB{file, AaImNorm{}, Nil{}, 0n, Nil{}}))
339	
340	# the items of a file's text; a fault becomes an error item
341	def AaParse.items(+file: List<&2, U32>, text: List<&2, U32>) -> List<&2, AaItem>:
342	  AaIt.of_lex(T.AaTok.lex(text), file)
343	
344	# Includes
345	
346	type AaExpOut is Data:
347	  AaExpOut{items: List<&2, AaItem>, scopes: List<&2, List<&2, List<&2, U32>>>}
348	
349	def AaExpOut.items(o: AaExpOut) -> List<&2, AaItem>:
350	  match o:
351	    case AaExpOut{i, s}:
352	      i
353	
354	def AaExpOut.scopes(o: AaExpOut) -> List<&2, List<&2, List<&2, U32>>>:
355	  match o:
356	    case AaExpOut{i, s}:
357	      s
358	
359	def AaParse.find_file(fs: List<&2, AaSrcFile>, +name: List<&2, U32>) -> Maybe<&2, AaSrcFile>:
360	  match fs:
361	    case Nil{}:
362	      None{}
363	    case Con{+f, t}:
364	      match f:
365	        case AaSrcFile{n, x}:
366	          Bool.pick(Maybe<&2, AaSrcFile>, X.AaText.eq(n, name), Some{f}, AaParse.find_file(t, name))
367	
368	# the file is already included in the innermost block
369	def AaParse.seen(scopes: List<&2, List<&2, List<&2, U32>>>, +name: List<&2, U32>) -> Bool:
370	  match scopes:
371	    case Nil{}:
372	      False{}
373	    case Con{s, t}:
374	      X.AaText.member(s, name)
375	
376	def AaParse.mark(scopes: List<&2, List<&2, List<&2, U32>>>, name: List<&2, U32>) -> List<&2, List<&2, List<&2, U32>>>:
377	  match scopes:
378	    case Nil{}:
379	      [[name]]
380	    case Con{s, t}:
381	      Con{Con{name, s}, t}
382	
383	def AaParse.pop(scopes: List<&2, List<&2, List<&2, U32>>>) -> List<&2, List<&2, List<&2, U32>>>:
384	  match scopes:
385	    case Nil{}:
386	      Nil{}
387	    case Con{s, t}:
388	      t
389	
390	# the items an include brings in
391	def AaParse.inc_items(m: Maybe<&2, AaSrcFile>, opt: Bool, src: E.AaSrc) -> List<&2, AaItem>:
392	  match m:
393	    case None{}:
394	      match opt:
395	        case True{}:
396	          Nil{}
397	        case False{}:
398	          [AaIError{E.AaSrc.include(src)}]
399	    case Some{f}:
400	      match f:
401	        case AaSrcFile{+n, x}:
402	          AaParse.items(n, x)
403	
404	# includes nested too deep
405	def AaParse.expand0(items: List<&2, AaItem>, +scopes: List<&2, List<&2, List<&2, U32>>>, +acc: List<&2, AaItem>) -> AaExpOut:
406	  match items:
407	    case Nil{}:
408	      AaExpOut{AaItem.rev_onto(acc, Nil{}), scopes}
409	    case Con{it, rest}:
410	      match it:
411	        case AaIOpen{ts, src}:
412	          AaParse.expand0(rest, Con{Nil{}, scopes}, Con{AaIOpen{ts, src}, acc})
413	        case AaIClose{src}:
414	          AaParse.expand0(rest, AaParse.pop(scopes), Con{AaIClose{src}, acc})
415	        case AaIInclude{+name, opt, src}:
416	          AaParse.expand0(rest, scopes, Bool.pick(List<&2, AaItem>, AaParse.seen(scopes, name), acc, Con{AaIError{E.AaSrc.include_depth(src)}, acc}))
417	        case AaIStmt{ts, src}:
418	          AaParse.expand0(rest, scopes, Con{AaIStmt{ts, src}, acc})
419	        case AaIVar{ts, src}:
420	          AaParse.expand0(rest, scopes, Con{AaIVar{ts, src}, acc})
421	        case AaIError{e}:
422	          AaParse.expand0(rest, scopes, Con{AaIError{e}, acc})
423	
424	# the items with every include replaced by the included file's items;
425	# scopes: the files included so far in each open block, innermost first
426	def AaParse.expand(+fuel: Nat, items: List<&2, AaItem>, +files: List<&2, AaSrcFile>, +scopes: List<&2, List<&2, List<&2, U32>>>, +acc: List<&2, AaItem>) -> AaExpOut:
427	  match fuel:
428	    case 0n:
429	      AaParse.expand0(items, scopes, acc)
430	    case 1n+f:
431	      match items:
432	        case Nil{}:
433	          AaExpOut{AaItem.rev_onto(acc, Nil{}), scopes}
434	        case Con{it, +rest}:
435	          match it:
436	            case AaIOpen{ts, src}:
437	              AaParse.expand(fuel, rest, files, Con{Nil{}, scopes}, Con{AaIOpen{ts, src}, acc})
438	            case AaIClose{src}:
439	              AaParse.expand(fuel, rest, files, AaParse.pop(scopes), Con{AaIClose{src}, acc})
440	            case AaIInclude{+name, opt, +src}:
441	              # Bend evaluates both arms of a Bool.pick, so the recursion is
442	              # one call whose arguments depend on whether the file is seen
443	              +seen = AaParse.seen(scopes, name)
444	              +sub = AaParse.expand(f, AaParse.inc_items(Bool.pick(Maybe<&2, AaSrcFile>, seen, None{}, AaParse.find_file(files, name)), Bool.or(seen, opt), src), files, AaParse.mark(scopes, name), Nil{})
445	              AaParse.expand(fuel, rest, files, Bool.pick(List<&2, List<&2, List<&2, U32>>>, seen, scopes, AaExpOut.scopes(sub)), Bool.pick(List<&2, AaItem>, seen, acc, AaItem.rev_onto(AaExpOut.items(sub), acc)))
446	            case AaIStmt{ts, src}:
447	              AaParse.expand(fuel, rest, files, scopes, Con{AaIStmt{ts, src}, acc})
448	            case AaIVar{ts, src}:
449	              AaParse.expand(fuel, rest, files, scopes, Con{AaIVar{ts, src}, acc})
450	            case AaIError{e}:
451	              AaParse.expand(fuel, rest, files, scopes, Con{AaIError{e}, acc})
452	
453	def AaParse.first_error(items: List<&2, AaItem>) -> Maybe<&2, E.AaError>:
454	  match items:
455	    case Nil{}:
456	      None{}
457	    case Con{it, rest}:
458	      match it:
459	        case AaIError{e}:
460	          Some{e}
461	        case _:
462	          AaParse.first_error(rest)
463	
464	# Variables
465	
466	def AaVars.find(env: List<&2, O.AaVar>, +name: List<&2, U32>) -> Maybe<&2, List<&2, List<&2, U32>>>:
467	  match env:
468	    case Nil{}:
469	      None{}
470	    case Con{v, t}:
471	      match v:
472	        case O.AaVar{n, +vals}:
473	          Bool.pick(Maybe<&2, List<&2, List<&2, U32>>>, X.AaText.eq(n, name), Some{vals}, AaVars.find(t, name))
474	
475	def AaVars.is_some(m: Maybe<&2, List<&2, List<&2, U32>>>) -> Bool:
476	  match m:
477	    case None{}:
478	      False{}
479	    case Some{x}:
480	      True{}
481	
482	# values added to a variable's
483	def AaVars.extend(env: List<&2, O.AaVar>, +name: List<&2, U32>, +more: List<&2, List<&2, U32>>) -> List<&2, O.AaVar>:
484	  match env:
485	    case Nil{}:
486	      Nil{}
487	    case Con{v, t}:
488	      match v:
489	        case O.AaVar{+n, +vals}:
490	          Con{Bool.pick(O.AaVar, X.AaText.eq(n, name), O.AaVar{n, X.AaText.lappend(vals, more)}, O.AaVar{n, vals}), AaVars.extend(t, name, more)}
491	
492	# a variable name: a letter, then letters, digits and '_'
493	def AaVars.name_ok.go(xs: List<&2, U32>) -> Bool:
494	  match xs:
495	    case Nil{}:
496	      True{}
497	    case Con{+h, t}:
498	      Bool.and(Bool.or(T.AaTerm.letter(h), Bool.or(Bool.and(U32.is_ge(h, 48), U32.is_le(h, 57)), U32.is_eq(h, 95))), AaVars.name_ok.go(t))
499	
500	def AaVars.name_ok(xs: List<&2, U32>) -> Bool:
501	  match xs:
502	    case Nil{}:
503	      False{}
504	    case Con{+h, t}:
505	      Bool.and(T.AaTerm.letter(h), AaVars.name_ok.go(t))
506	
507	# @{NAME} at the start of a word: the name and what follows the '}'
508	type AaVRef is Data:
509	  AaVRef{name: List<&2, U32>, rest: List<&2, U32>}
510	
511	def AaVars.ref.go(xs: List<&2, U32>, +acc: List<&2, U32>) -> Maybe<&2, AaVRef>:
512	  match xs:
513	    case Nil{}:
514	      None{}
515	    case Con{+h, +t}:
516	      Bool.pick(Maybe<&2, AaVRef>, U32.is_eq(h, 125), Some{AaVRef{X.AaText.rev(acc), t}}, AaVars.ref.go(t, Con{h, acc}))
517	
518	def AaVars.ref(+w: List<&2, U32>) -> Maybe<&2, AaVRef>:
519	  Bool.pick(Maybe<&2, AaVRef>, X.AaText.starts(w, "@{"), AaVars.ref.go(X.AaText.drop(2n, w), Nil{}), None{})
520	
521	def AaVars.values.cons(x: List<&2, U32>, r: Result<&2, &2, E.AaError, List<&2, List<&2, U32>>>) -> Result<&2, &2, E.AaError, List<&2, List<&2, U32>>>:
522	  match r:
523	    case Fail{e}:
524	      Fail{e}
525	    case Done{xs}:
526	      Done{Con{x, xs}}
527	
528	# the text of each word or string
529	def AaVars.values(ts: List<&2, T.AaTok>, src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, List<&2, U32>>>:
530	  match ts:
531	    case Nil{}:
532	      Done{Nil{}}
533	    case Con{t, rest}:
534	      match t:
535	        case T.AaTWord{w, l}:
536	          AaVars.values.cons(w, AaVars.values(rest, src))
537	        case T.AaTQuoted{q, l}:
538	          AaVars.values.cons(q, AaVars.values(rest, src))
539	        case _:
540	          Fail{E.AaSrc.syntax(src)}
541	
542	# an assignment: name, whether it is +=, the values
543	type AaAssign is Data:
544	  AaAssign{name: List<&2, U32>, append: Bool, values: List<&2, List<&2, U32>>}
545	
546	# the operator at the start of x: += (True) or = (False), and what follows it
547	def AaVars.op(+x: List<&2, U32>) -> Maybe<&2, AaVRef>:
548	  Bool.pick(Maybe<&2, AaVRef>, X.AaText.starts(x, "+="), Some{AaVRef{[1], X.AaText.drop(2n, x)}}, Bool.pick(Maybe<&2, AaVRef>, X.AaText.starts(x, "="), Some{AaVRef{Nil{}, X.AaText.drop(1n, x)}}, None{}))
549	
550	def AaVars.first(rem: List<&2, U32>) -> List<&2, List<&2, U32>>:
551	  match rem:
552	    case Nil{}:
553	      Nil{}
554	    case Con{h, t}:
555	      [Con{h, t}]
556	
557	def AaVars.assign.op(m: Maybe<&2, AaVRef>, name: List<&2, U32>, rest: List<&2, T.AaTok>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaAssign>:
558	  match m:
559	    case None{}:
560	      Fail{E.AaSrc.syntax(src)}
561	    case Some{o}:
562	      match o:
563	        case AaVRef{tag, rem}:
564	          do Result<&2, &2, E.AaError, AaAssign>:
565	            vs : List<&2, List<&2, U32>> <- AaVars.values(rest, src)
566	            return AaAssign{name, Bool.not(X.AaText.is_nil(tag)), X.AaText.lappend(AaVars.first(rem), vs)}
567	
568	# @{NAME} then a separate = or += word
569	def AaVars.assign.next(ts: List<&2, T.AaTok>, name: List<&2, U32>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaAssign>:
570	  match ts:
571	    case Nil{}:
572	      Fail{E.AaSrc.syntax(src)}
573	    case Con{t, rest}:
574	      match t:
575	        case T.AaTWord{+w, l}:
576	          AaVars.assign.op(AaVars.op(w), name, rest, src)
577	        case _:
578	          Fail{E.AaSrc.syntax(src)}
579	
580	def AaVars.assign.ref(m: Maybe<&2, AaVRef>, +rest: List<&2, T.AaTok>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaAssign>:
581	  match m:
582	    case None{}:
583	      Fail{E.AaSrc.syntax(src)}
584	    case Some{r}:
585	      match r:
586	        case AaVRef{+name, +after}:
587	          Bool.pick(Result<&2, &2, E.AaError, AaAssign>, AaVars.name_ok(name), Bool.pick(Result<&2, &2, E.AaError, AaAssign>, X.AaText.is_nil(after), AaVars.assign.next(rest, name, src), AaVars.assign.op(AaVars.op(after), name, rest, src)), Fail{E.AaSrc.syntax(src)})
588	
589	def AaVars.assign.parse(ts: List<&2, T.AaTok>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaAssign>:
590	  match ts:
591	    case Nil{}:
592	      Fail{E.AaSrc.syntax(src)}
593	    case Con{t, rest}:
594	      match t:
595	        case T.AaTWord{+w, l}:
596	          AaVars.assign.ref(AaVars.ref(w), rest, src)
597	        case _:
598	          Fail{E.AaSrc.syntax(src)}
599	
600	# the environment after an assignment
601	def AaVars.apply.go(ap: Bool, known: Bool, env: List<&2, O.AaVar>, name: List<&2, U32>, vs: List<&2, List<&2, U32>>, src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, O.AaVar>>:
602	  match ap:
603	    case True{}:
604	      match known:
605	        case True{}:
606	          Done{AaVars.extend(env, name, vs)}
607	        case False{}:
608	          Fail{E.AaSrc.var_redefined(src)}
609	    case False{}:
610	      match known:
611	        case True{}:
612	          Fail{E.AaSrc.var_redefined(src)}
613	        case False{}:
614	          Done{Con{O.AaVar{name, vs}, env}}
615	
616	def AaVars.apply(a: AaAssign, +env: List<&2, O.AaVar>, src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, O.AaVar>>:
617	  match a:
618	    case AaAssign{+name, ap, vs}:
619	      AaVars.apply.go(ap, AaVars.is_some(AaVars.find(env, name)), env, name, vs, src)
620	
621	# Expanding variables in a text
622	
623	def AaVars.unslash(+v: List<&2, U32>) -> List<&2, U32>:
624	  Bool.pick(List<&2, U32>, U32.is_eq(X.AaText.last(v, 0), 47), X.AaText.init(v), v)
625	
626	def AaVars.value(strip: Bool, +v: List<&2, U32>) -> List<&2, U32>:
627	  match strip:
628	    case True{}:
629	      AaVars.unslash(v)
630	    case False{}:
631	      v
632	
633	# the values, separated by commas, last character first, onto acc
634	def AaVars.join(vs: List<&2, List<&2, U32>>, +strip: Bool, +first: Bool, +acc: List<&2, U32>) -> List<&2, U32>:
635	  match vs:
636	    case Nil{}:
637	      acc
638	    case Con{v, t}:
639	      AaVars.join(t, strip, False{}, X.AaText.rev_onto(AaVars.value(strip, v), Bool.pick(List<&2, U32>, first, acc, Con{44, acc})))
640	
641	# the expansion of one reference (last character first, onto out)
642	def AaVars.emit(m: Maybe<&2, List<&2, List<&2, U32>>>, +strip: Bool, out: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
643	  match m:
644	    case None{}:
645	      None{}
646	    case Some{vs}:
647	      match vs:
648	        case Nil{}:
649	          None{}
650	        case Con{v, rest}:
651	          match rest:
652	            case Nil{}:
653	              Some{X.AaText.rev_onto(AaVars.value(strip, v), out)}
654	            case Con{w, more}:
655	              Some{Con{125, AaVars.join(Con{v, Con{w, more}}, strip, True{}, Con{123, out})}}
656	
657	def AaVars.lookup(+env: List<&2, O.AaVar>, pname: Maybe<&2, List<&2, U32>>, +name: List<&2, U32>) -> Maybe<&2, List<&2, List<&2, U32>>>:
658	  match pname:
659	    case None{}:
660	      AaVars.find(env, name)
661	    case Some{p}:
662	      Bool.pick(Maybe<&2, List<&2, List<&2, U32>>>, X.AaText.is(name, "profile_name"), Some{[p]}, AaVars.find(env, name))
663	
664	# the substitution: mode (0 text, 1 after an at sign, 2 inside a reference),
665	# the name read so far, the output (both last character first), still well formed
666	type AaSb is Data:
667	  AaSb{mode: Nat, name: List<&2, U32>, out: List<&2, U32>, ok: Bool}
668	
669	def AaSb.close(r: Maybe<&2, List<&2, U32>>, ok: Bool) -> AaSb:
670	  match r:
671	    case None{}:
672	      AaSb{0n, Nil{}, Nil{}, False{}}
673	    case Some{out}:
674	      AaSb{0n, Nil{}, out, ok}
675	
676	def AaSb.text(+h: U32, +out: List<&2, U32>, +ok: Bool) -> AaSb:
677	  Bool.pick(AaSb, U32.is_eq(h, 64), AaSb{1n, Nil{}, out, ok}, AaSb{0n, Nil{}, Con{h, out}, ok})
678	
679	def AaSb.step(st: AaSb, +h: U32, +next: U32, +env: List<&2, O.AaVar>, +pname: Maybe<&2, List<&2, U32>>) -> AaSb:
680	  match st:
681	    case AaSb{m, +nm, +out, +ok}:
682	      match m:
683	        case 0n:
684	          AaSb.text(h, out, ok)
685	        case 1n+m1:
686	          match m1:
687	            case 0n:
688	              Bool.pick(AaSb, U32.is_eq(h, 123), AaSb{2n, Nil{}, out, ok}, AaSb.text(h, Con{64, out}, ok))
689	            case 1n+m2:
690	              Bool.pick(AaSb, U32.is_eq(h, 125), AaSb.close(AaVars.emit(AaVars.lookup(env, pname, X.AaText.rev(nm)), U32.is_eq(next, 47), out), ok), AaSb{2n, Con{h, nm}, out, ok})
691	
692	def AaSb.run(xs: List<&2, U32>, st: AaSb, +env: List<&2, O.AaVar>, +pname: Maybe<&2, List<&2, U32>>) -> AaSb:
693	  match xs:
694	    case Nil{}:
695	      st
696	    case Con{+h, +t}:
697	      AaSb.run(t, AaSb.step(st, h, X.AaText.head(t), env, pname), env, pname)
698	
699	def AaSb.result(st: AaSb) -> Maybe<&2, List<&2, U32>>:
700	  match st:
701	    case AaSb{m, nm, out, ok}:
702	      match m:
703	        case 0n:
704	          match ok:
705	            case False{}:
706	              None{}
707	            case True{}:
708	              Some{X.AaText.rev(out)}
709	        case 1n+m1:
710	          match m1:
711	            case 0n:
712	              match ok:
713	                case False{}:
714	                  None{}
715	                case True{}:
716	                  Some{X.AaText.rev(Con{64, out})}
717	            case 1n+m2:
718	              None{}
719	
720	# one round: every reference replaced by its values
721	def AaVars.subst(xs: List<&2, U32>, +env: List<&2, O.AaVar>, +pname: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
722	  AaSb.result(AaSb.run(xs, AaSb{0n, Nil{}, Nil{}, True{}}, env, pname))
723	
724	# a reference remains: an at sign before an opening brace
725	def AaVars.has_ref(xs: List<&2, U32>) -> Bool:
726	  match xs:
727	    case Nil{}:
728	      False{}
729	    case Con{+h, +t}:
730	      Bool.or(Bool.and(U32.is_eq(h, 64), U32.is_eq(X.AaText.head(t), 123)), AaVars.has_ref(t))
731	
732	# whether a text still holds a reference; None stays None
733	def AaVars.more(m: Maybe<&2, List<&2, U32>>) -> Bool:
734	  match m:
735	    case None{}:
736	      False{}
737	    case Some{t}:
738	      AaVars.has_ref(t)
739	
740	# more: m still holds a reference (computed by the caller, so that a text
741	# without one is not substituted again)
742	def AaVars.expand.go(fuel: Nat, +more: Bool, m: Maybe<&2, List<&2, U32>>, +env: List<&2, O.AaVar>, +pname: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
743	  match fuel:
744	    case 0n:
745	      match more:
746	        case True{}:
747	          None{}
748	        case False{}:
749	          m
750	    case 1n+f:
751	      match more:
752	        case False{}:
753	          m
754	        case True{}:
755	          match m:
756	            case None{}:
757	              None{}
758	            case Some{t}:
759	              +n = AaVars.subst(t, env, pname)
760	              AaVars.expand.go(f, AaVars.more(n), n, env, pname)
761	
762	# xs with its variables expanded (values may refer to variables, to a depth
763	# of eight); None if a variable is not assigned
764	def AaVars.expand(+xs: List<&2, U32>, +env: List<&2, O.AaVar>, +pname: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
765	  AaVars.expand.go(8n, AaVars.has_ref(xs), Some{xs}, env, pname)
766	
767	def AaVars.tok.go(m: Maybe<&2, List<&2, U32>>, quoted: Bool, l: U32, src: E.AaSrc) -> Result<&2, &2, E.AaError, T.AaTok>:
768	  match m:
769	    case None{}:
770	      Fail{E.AaSrc.var_undefined(src)}
771	    case Some{x}:
772	      match quoted:
773	        case True{}:
774	          Done{T.AaTQuoted{x, l}}
775	        case False{}:
776	          Done{T.AaTWord{x, l}}
777	
778	def AaVars.tok(t: T.AaTok, +env: List<&2, O.AaVar>, +pname: Maybe<&2, List<&2, U32>>, src: E.AaSrc) -> Result<&2, &2, E.AaError, T.AaTok>:
779	  match t:
780	    case T.AaTWord{w, l}:
781	      AaVars.tok.go(AaVars.expand(w, env, pname), False{}, l, src)
782	    case T.AaTQuoted{q, l}:
783	      AaVars.tok.go(AaVars.expand(q, env, pname), True{}, l, src)
784	    case T.AaTOpen{l}:
785	      Done{T.AaTOpen{l}}
786	    case T.AaTClose{l}:
787	      Done{T.AaTClose{l}}
788	    case T.AaTLParen{l}:
789	      Done{T.AaTLParen{l}}
790	    case T.AaTRParen{l}:
791	      Done{T.AaTRParen{l}}
792	    case T.AaTComma{l}:
793	      Done{T.AaTComma{l}}
794	
795	# a statement's tokens with variables expanded
796	def AaVars.toks(ts: List<&2, T.AaTok>, +env: List<&2, O.AaVar>, +pname: Maybe<&2, List<&2, U32>>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, T.AaTok>>:
797	  match ts:
798	    case Nil{}:
799	      Done{Nil{}}
800	    case Con{t, rest}:
801	      do Result<&2, &2, E.AaError, List<&2, T.AaTok>>:
802	        x : T.AaTok <- AaVars.tok(t, env, pname, src)
803	        xs : List<&2, T.AaTok> <- AaVars.toks(rest, env, pname, src)
804	        return Con{x, xs}
805	
806	# The preamble: variables and aliases
807	
808	type AaAlias is Data:
809	  AaAlias{from: List<&2, U32>, to: List<&2, U32>}
810	
811	type AaPre is Data:
812	  AaPre{env: List<&2, O.AaVar>, aliases: List<&2, AaAlias>, depth: Nat, started: Bool, err: Maybe<&2, E.AaError>}
813	
814	def AaPre.fail(p: AaPre, e: E.AaError) -> AaPre:
815	  match p:
816	    case AaPre{v, a, d, s, err}:
817	      match err:
818	        case None{}:
819	          AaPre{v, a, d, s, Some{e}}
820	        case Some{e0}:
821	          AaPre{v, a, d, s, Some{e0}}
822	
823	def AaPre.env(r: Result<&2, &2, E.AaError, List<&2, O.AaVar>>, p: AaPre) -> AaPre:
824	  match r:
825	    case Fail{e}:
826	      AaPre.fail(p, e)
827	    case Done{v}:
828	      match p:
829	        case AaPre{v0, a, d, s, err}:
830	          AaPre{v, a, d, s, err}
831	
832	def AaPre.assign(r: Result<&2, &2, E.AaError, AaAssign>, +p: AaPre, src: E.AaSrc) -> AaPre:
833	  match r:
834	    case Fail{e}:
835	      AaPre.fail(p, e)
836	    case Done{a}:
837	      match p:
838	        case AaPre{+v, al, d, s, err}:
839	          AaPre.env(AaVars.apply(a, v, src), AaPre{v, al, d, s, err})
840	
841	def AaPre.text(t: T.AaTok) -> Maybe<&2, List<&2, U32>>:
842	  match t:
843	    case T.AaTWord{w, l}:
844	      Some{w}
845	    case T.AaTQuoted{q, l}:
846	      Some{q}
847	    case _:
848	      None{}
849	
850	# alias FROM -> TO
851	def AaPre.alias.go(a: Maybe<&2, List<&2, U32>>, b: Maybe<&2, List<&2, U32>>, p: AaPre, src: E.AaSrc) -> AaPre:
852	  match a:
853	    case None{}:
854	      AaPre.fail(p, E.AaSrc.syntax(src))
855	    case Some{x}:
856	      match b:
857	        case None{}:
858	          AaPre.fail(p, E.AaSrc.syntax(src))
859	        case Some{y}:
860	          match p:
861	            case AaPre{v, al, d, s, err}:
862	              AaPre{v, Con{AaAlias{x, y}, al}, d, s, err}
863	
864	def AaPre.alias(ts: List<&2, T.AaTok>, +p: AaPre, +src: E.AaSrc) -> AaPre:
865	  match ts:
866	    case Con{a, r1}:
867	      match r1:
868	        case Con{arrow, r2}:
869	          match r2:
870	            case Con{b, r3}:
871	              match r3:
872	                case Nil{}:
873	                  Bool.pick(AaPre, T.AaTok.is(arrow, "->"), AaPre.alias.go(AaPre.text(a), AaPre.text(b), p, src), AaPre.fail(p, E.AaSrc.syntax(src)))
874	                case Con{x, r4}:
875	                  AaPre.fail(p, E.AaSrc.syntax(src))
876	            case Nil{}:
877	              AaPre.fail(p, E.AaSrc.syntax(src))
878	        case Nil{}:
879	          AaPre.fail(p, E.AaSrc.syntax(src))
880	    case Nil{}:
881	      AaPre.fail(p, E.AaSrc.syntax(src))
882	
883	def AaPre.depth(p: AaPre) -> Nat:
884	  match p:
885	    case AaPre{v, a, d, s, err}:
886	      d
887	
888	def AaPre.started(p: AaPre) -> Bool:
889	  match p:
890	    case AaPre{v, a, d, s, err}:
891	      s
892	
893	# a statement at the top level: alias (before the first profile), abi, or an error
894	def AaPre.top(ts: List<&2, T.AaTok>, +p: AaPre, +src: E.AaSrc) -> AaPre:
895	  match ts:
896	    case Nil{}:
897	      AaPre.fail(p, E.AaSrc.syntax(src))
898	    case Con{+t, rest}:
899	      Bool.pick(AaPre, T.AaTok.is(t, "alias"), Bool.pick(AaPre, AaPre.started(p), AaPre.fail(p, E.AaSrc.preamble(src)), AaPre.alias(rest, p, src)), Bool.pick(AaPre, T.AaTok.is(t, "abi"), p, AaPre.fail(p, E.AaSrc.syntax(src))))
900	
901	def AaPre.stmt(d: Nat, ts: List<&2, T.AaTok>, +p: AaPre, +src: E.AaSrc) -> AaPre:
902	  match d:
903	    case 0n:
904	      AaPre.top(ts, p, src)
905	    case 1n+e:
906	      p
907	
908	def AaPre.var(ok: Bool, ts: List<&2, T.AaTok>, +p: AaPre, +src: E.AaSrc) -> AaPre:
909	  match ok:
910	    case True{}:
911	      AaPre.assign(AaVars.assign.parse(ts, src), p, src)
912	    case False{}:
913	      AaPre.fail(p, E.AaSrc.preamble(src))
914	
915	def AaPre.open(p: AaPre) -> AaPre:
916	  match p:
917	    case AaPre{v, a, d, s, err}:
918	      AaPre{v, a, 1n+d, True{}, err}
919	
920	def AaPre.close(p: AaPre, src: E.AaSrc) -> AaPre:
921	  match p:
922	    case AaPre{v, a, d, s, err}:
923	      match d:
924	        case 0n:
925	          AaPre.fail(AaPre{v, a, 0n, s, err}, E.AaSrc.syntax(src))
926	        case 1n+e:
927	          AaPre{v, a, e, s, err}
928	
929	def AaPre.step(+p: AaPre, it: AaItem) -> AaPre:
930	  match it:
931	    case AaIVar{ts, src}:
932	      AaPre.var(Bool.and(Nat.is_eq(AaPre.depth(p), 0n), Bool.not(AaPre.started(p))), ts, p, src)
933	    case AaIStmt{ts, src}:
934	      AaPre.stmt(AaPre.depth(p), ts, p, src)
935	    case AaIOpen{ts, src}:
936	      AaPre.open(p)
937	    case AaIClose{src}:
938	      AaPre.close(p, src)
939	    case AaIInclude{n, o, src}:
940	      p
941	    case AaIError{e}:
942	      AaPre.fail(p, e)
943	
944	def AaPre.run(items: List<&2, AaItem>, p: AaPre) -> AaPre:
945	  match items:
946	    case Nil{}:
947	      p
948	    case Con{it, rest}:
949	      AaPre.run(rest, AaPre.step(p, it))
950	
951	# Qualifiers: [audit] [allow | deny] [owner], in that order; a block's
952	# qualifiers apply to the rules inside it. access: 0 neither, 1 allow, 2 deny
953	
954	type AaBQ is Data:
955	  AaBQ{audit: Bool, access: Nat, owner: Bool}
956	
957	def AaBQ.none() -> AaBQ:
958	  AaBQ{False{}, 0n, False{}}
959	
960	# what a term is as a qualifier: 1 audit, 2 allow, 3 deny, 4 owner, 0 none
961	def AaQ.kind(+t: T.AaTerm) -> Nat:
962	  Bool.pick(Nat, T.AaTerm.is(t, "audit"), 1n, Bool.pick(Nat, T.AaTerm.is(t, "allow"), 2n, Bool.pick(Nat, T.AaTerm.is(t, "deny"), 3n, Bool.pick(Nat, T.AaTerm.is(t, "owner"), 4n, 0n))))
963	
964	# the qualifier k may come at stage s (0 start, 1 after audit, 2 after allow
965	# or deny, 3 after owner), and the stage after it
966	def AaQ.allowed(k: Nat, s: Nat) -> Bool:
967	  match k:
968	    case 0n:
969	      False{}
970	    case 1n+k1:
971	      match k1:
972	        case 0n:
973	          Nat.is_eq(s, 0n)
974	        case 1n+k2:
975	          match k2:
976	            case 0n:
977	              Nat.is_le(s, 1n)
978	            case 1n+k3:
979	              match k3:
980	                case 0n:
981	                  Nat.is_le(s, 1n)
982	                case 1n+k4:
983	                  Nat.is_le(s, 2n)
984	
985	def AaQ.stage(k: Nat) -> Nat:
986	  match k:
987	    case 0n:
988	      0n
989	    case 1n+k1:
990	      match k1:
991	        case 0n:
992	          1n
993	        case 1n+k2:
994	          match k2:
995	            case 0n:
996	              2n
997	            case 1n+k3:
998	              match k3:
999	                case 0n:
1000	                  2n
1001	                case 1n+k4:
1002	                  3n
1003	
1004	def AaQ.add(q: AaBQ, k: Nat) -> AaBQ:
1005	  match q:
1006	    case AaBQ{a, c, o}:
1007	      match k:
1008	        case 0n:
1009	          AaBQ{a, c, o}
1010	        case 1n+k1:
1011	          match k1:
1012	            case 0n:
1013	              AaBQ{True{}, c, o}
1014	            case 1n+k2:
1015	              match k2:
1016	                case 0n:
1017	                  AaBQ{a, 1n, o}
1018	                case 1n+k3:
1019	                  match k3:
1020	                    case 0n:
1021	                      AaBQ{a, 2n, o}
1022	                    case 1n+k4:
1023	                      AaBQ{a, c, True{}}
1024	
1025	type AaQP is Data:
1026	  AaQP{q: AaBQ, rest: List<&2, T.AaTerm>}
1027	
1028	def AaQ.parse.go(+k: Nat, +t: T.AaTerm, +rest: List<&2, T.AaTerm>, +stage: Nat, +q: AaBQ, more: AaQP) -> AaQP:
1029	  Bool.pick(AaQP, AaQ.allowed(k, stage), more, AaQP{q, Con{t, rest}})
1030	
1031	# the leading qualifiers of a rule's terms, and the terms after them
1032	def AaQ.parse(ts: List<&2, T.AaTerm>, +stage: Nat, +q: AaBQ) -> AaQP:
1033	  match ts:
1034	    case Nil{}:
1035	      AaQP{q, Nil{}}
1036	    case Con{+t, +rest}:
1037	      +k = AaQ.kind(t)
1038	      AaQ.parse.go(k, t, rest, stage, q, AaQ.parse(rest, AaQ.stage(k), AaQ.add(q, k)))
1039	
1040	# a block's qualifiers with a rule's (or an inner block's): allow and deny conflict
1041	def AaQ.combine(b: AaBQ, r: AaBQ, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaBQ>:
1042	  match b:
1043	    case AaBQ{a1, +c1, o1}:
1044	      match r:
1045	        case AaBQ{a2, +c2, o2}:
1046	          Bool.pick(Result<&2, &2, E.AaError, AaBQ>, Bool.and(Bool.and(Nat.is_gt(c1, 0n), Nat.is_gt(c2, 0n)), Bool.not(Nat.is_eq(c1, c2))), Fail{E.AaSrc.syntax(src)}, Done{AaBQ{Bool.or(a1, a2), Nat.max(c1, c2), Bool.or(o1, o2)}})
1047	
1048	def AaBQ.qual(q: AaBQ) -> P.AaQual:
1049	  match q:
1050	    case AaBQ{a, c, o}:
1051	      P.AaQual{a, Nat.is_eq(c, 2n), o}
1052	
1053	# Rules
1054	
1055	type AaCtx is Data:
1056	  AaCtx{env: List<&2, O.AaVar>, aliases: List<&2, AaAlias>}
1057	
1058	def AaCtx.env(c: AaCtx) -> List<&2, O.AaVar>:
1059	  match c:
1060	    case AaCtx{e, a}:
1061	      e
1062	
1063	def AaCtx.aliases(c: AaCtx) -> List<&2, AaAlias>:
1064	  match c:
1065	    case AaCtx{e, a}:
1066	      a
1067	
1068	def AaParse.unsupported() -> List<&2, String>:
1069	  ["link", "unix", "pivot_root", "set", "mqueue", "io_uring", "userns", "all", "rlimit"]
1070	
1071	# the keyword of a rule: 1 capability, 2 network, 3 signal, 4 ptrace, 5
1072	# mount, 6 remount, 7 umount, 8 dbus, 9 change_profile, 10 file, 11 a rule
1073	# kind outside the model, 12 a statement that belongs in the preamble, 0 none
1074	# (a file rule without the keyword)
1075	def AaParse.keyword(+t: T.AaTerm) -> Nat:
1076	  Bool.pick(Nat, T.AaTerm.is(t, "capability"), 1n, Bool.pick(Nat, T.AaTerm.is(t, "network"), 2n, Bool.pick(Nat, T.AaTerm.is(t, "signal"), 3n, Bool.pick(Nat, T.AaTerm.is(t, "ptrace"), 4n, Bool.pick(Nat, T.AaTerm.is(t, "mount"), 5n, Bool.pick(Nat, T.AaTerm.is(t, "remount"), 6n, Bool.pick(Nat, T.AaTerm.is(t, "umount"), 7n, Bool.pick(Nat, T.AaTerm.is(t, "dbus"), 8n, Bool.pick(Nat, T.AaTerm.is(t, "change_profile"), 9n, Bool.pick(Nat, T.AaTerm.is(t, "file"), 10n, Bool.pick(Nat, T.AaTerm.is_one_of(t, AaParse.unsupported()), 11n, Bool.pick(Nat, Bool.or(T.AaTerm.is(t, "alias"), T.AaTerm.is(t, "abi")), 12n, 0n))))))))))))
1077	
1078	def AaParse.wrap.cap(r: Result<&2, &2, E.AaError, RC.AaCapRule>) -> Result<&2, &2, E.AaError, PR.AaRules>:
1079	  match r:
1080	    case Fail{e}:
1081	      Fail{e}
1082	    case Done{x}:
1083	      Done{PR.AaRules.cap(x)}
1084	
1085	def AaParse.wrap.net(r: Result<&2, &2, E.AaError, RN.AaNetRule>) -> Result<&2, &2, E.AaError, PR.AaRules>:
1086	  match r:
1087	    case Fail{e}:
1088	      Fail{e}
1089	    case Done{x}:
1090	      Done{PR.AaRules.net(x)}
1091	
1092	def AaParse.wrap.signal(r: Result<&2, &2, E.AaError, RS.AaSignalRule>) -> Result<&2, &2, E.AaError, PR.AaRules>:
1093	  match r:
1094	    case Fail{e}:
1095	      Fail{e}
1096	    case Done{x}:
1097	      Done{PR.AaRules.signal(x)}
1098	
1099	def AaParse.wrap.ptrace(r: Result<&2, &2, E.AaError, RP.AaPtraceRule>) -> Result<&2, &2, E.AaError, PR.AaRules>:
1100	  match r:
1101	    case Fail{e}:
1102	      Fail{e}
1103	    case Done{x}:
1104	      Done{PR.AaRules.ptrace(x)}
1105	
1106	def AaParse.wrap.mount(r: Result<&2, &2, E.AaError, RM.AaMountRule>) -> Result<&2, &2, E.AaError, PR.AaRules>:
1107	  match r:
1108	    case Fail{e}:
1109	      Fail{e}
1110	    case Done{x}:
1111	      Done{PR.AaRules.mount(x)}
1112	
1113	def AaParse.wrap.dbus(r: Result<&2, &2, E.AaError, RD.AaDbusRule>) -> Result<&2, &2, E.AaError, PR.AaRules>:
1114	  match r:
1115	    case Fail{e}:
1116	      Fail{e}
1117	    case Done{x}:
1118	      Done{PR.AaRules.dbus_rule(x)}
1119	
1120	def AaParse.wrap.change(r: Result<&2, &2, E.AaError, RX.AaChangeRule>) -> Result<&2, &2, E.AaError, PR.AaRules>:
1121	  match r:
1122	    case Fail{e}:
1123	      Fail{e}
1124	    case Done{x}:
1125	      Done{PR.AaRules.change(x)}
1126	
1127	def AaParse.alias.glob(m: Maybe<&2, G.AaGlob>, r: F.AaFileRule) -> List<&2, F.AaFileRule>:
1128	  match m:
1129	    case None{}:
1130	      Nil{}
1131	    case Some{g}:
1132	      match r:
1133	        case F.AaFileRule{q, text, g0, p, e, tg}:
1134	          [F.AaFileRule{q, text, g, p, e, tg}]
1135	
1136	# a file rule copied under an alias whose source starts its pattern
1137	def AaParse.alias.one(a: AaAlias, r: F.AaFileRule) -> List<&2, F.AaFileRule>:
1138	  match a:
1139	    case AaAlias{+from, +to}:
1140	      match r:
1141	        case F.AaFileRule{q, +text, g, p, e, tg}:
1142	          Bool.pick(List<&2, F.AaFileRule>, Bool.and(Bool.not(X.AaText.is_nil(text)), X.AaText.prefix(text, from)), AaParse.alias.glob(G.AaGlob.parse(X.AaText.append(to, X.AaText.drop(X.AaText.len(from), text))), F.AaFileRule{q, X.AaText.append(to, X.AaText.drop(X.AaText.len(from), text)), g, p, e, tg}), Nil{})
1143	
1144	def AaParse.alias.all(als: List<&2, AaAlias>, +r: F.AaFileRule) -> List<&2, F.AaFileRule>:
1145	  match als:
1146	    case Nil{}:
1147	      Nil{}
1148	    case Con{a, t}:
1149	      F.AaFileRule.append(AaParse.alias.one(a, r), AaParse.alias.all(t, r))
1150	
1151	def AaParse.wrap.file(r: Result<&2, &2, E.AaError, F.AaFileRule>, als: List<&2, AaAlias>) -> Result<&2, &2, E.AaError, PR.AaRules>:
1152	  match r:
1153	    case Fail{e}:
1154	      Fail{e}
1155	    case Done{+x}:
1156	      Done{PR.AaRules.with_files(PR.AaRules.empty(), Con{x, AaParse.alias.all(als, x)})}
1157	
1158	def AaParse.dispatch(k: Nat, +t: T.AaTerm, +rest: List<&2, T.AaTerm>, +q: P.AaQual, +als: List<&2, AaAlias>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaRules>:
1159	  match k:
1160	    case 0n:
1161	      AaParse.wrap.file(F.AaFile.parse(Con{t, rest}, q, src), als)
1162	    case 1n+k1:
1163	      match k1:
1164	        case 0n:
1165	          AaParse.wrap.cap(RC.AaCap.parse(rest, q, src))
1166	        case 1n+k2:
1167	          match k2:
1168	            case 0n:
1169	              AaParse.wrap.net(RN.AaNet.parse(rest, q, src))
1170	            case 1n+k3:
1171	              match k3:
1172	                case 0n:
1173	                  AaParse.wrap.signal(RS.AaSignal.parse(rest, q, src))
1174	                case 1n+k4:
1175	                  match k4:
1176	                    case 0n:
1177	                      AaParse.wrap.ptrace(RP.AaPtrace.parse(rest, q, src))
1178	                    case 1n+k5:
1179	                      match k5:
1180	                        case 0n:
1181	                          AaParse.wrap.mount(RM.AaMount.parse(RM.AaMountOpMount{}, rest, q, src))
1182	                        case 1n+k6:
1183	                          match k6:
1184	                            case 0n:
1185	                              AaParse.wrap.mount(RM.AaMount.parse(RM.AaMountOpRemount{}, rest, q, src))
1186	                            case 1n+k7:
1187	                              match k7:
1188	                                case 0n:
1189	                                  AaParse.wrap.mount(RM.AaMount.parse(RM.AaMountOpUmount{}, rest, q, src))
1190	                                case 1n+k8:
1191	                                  match k8:
1192	                                    case 0n:
1193	                                      AaParse.wrap.dbus(RD.AaDbus.parse(rest, q, src))
1194	                                    case 1n+k9:
1195	                                      match k9:
1196	                                        case 0n:
1197	                                          AaParse.wrap.change(RX.AaChange.parse(rest, q, src))
1198	                                        case 1n+k10:
1199	                                          match k10:
1200	                                            case 0n:
1201	                                              AaParse.wrap.file(F.AaFile.parse(rest, q, src), als)
1202	                                            case 1n+k11:
1203	                                              match k11:
1204	                                                case 0n:
1205	                                                  Fail{E.AaSrc.unsupported(src)}
1206	                                                case 1n+k12:
1207	                                                  Fail{E.AaSrc.preamble(src)}
1208	
1209	# a rule's terms (after the qualifiers), with the qualifiers in force
1210	def AaParse.rule(ts: List<&2, T.AaTerm>, +q: P.AaQual, +als: List<&2, AaAlias>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaRules>:
1211	  match ts:
1212	    case Nil{}:
1213	      Fail{E.AaSrc.syntax(src)}
1214	    case Con{+t, rest}:
1215	      AaParse.dispatch(AaParse.keyword(t), t, rest, q, als, src)
1216	
1217	def AaParse.terms(m: Maybe<&2, List<&2, T.AaTerm>>, src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, T.AaTerm>>:
1218	  match m:
1219	    case None{}:
1220	      Fail{E.AaSrc.syntax(src)}
1221	    case Some{ts}:
1222	      Done{ts}
1223	
1224	def AaParse.rule.qual(qp: AaQP, +block: AaBQ, +als: List<&2, AaAlias>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaRules>:
1225	  match qp:
1226	    case AaQP{q, rest}:
1227	      do Result<&2, &2, E.AaError, PR.AaRules>:
1228	        c : AaBQ <- AaQ.combine(block, q, src)
1229	        AaParse.rule(rest, AaBQ.qual(c), als, src)
1230	
1231	# a statement inside a profile: its rules
1232	def AaParse.stmt(ts: List<&2, T.AaTok>, +block: AaBQ, +pname: List<&2, U32>, +ctx: AaCtx, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaRules>:
1233	  do Result<&2, &2, E.AaError, PR.AaRules>:
1234	    xs : List<&2, T.AaTok> <- AaVars.toks(ts, AaCtx.env(ctx), Some{pname}, src)
1235	    terms : List<&2, T.AaTerm> <- AaParse.terms(T.AaTerm.of_toks(xs), src)
1236	    AaParse.rule.qual(AaQ.parse(terms, 0n, AaBQ.none()), block, AaCtx.aliases(ctx), src)
1237	
1238	# Profile heads: profile NAME [ATTACHMENT] [FLAGS], PATH [FLAGS], ^HAT
1239	# [FLAGS], hat NAME [FLAGS], or the qualifiers of a qualifier block.
1240	# kind: 0 a profile, 1 a hat, 2 a qualifier block
1241	
1242	type AaHead is Data:
1243	  AaHead{kind: Nat, name: List<&2, U32>, attach: Maybe<&2, G.AaGlob>, flags: PR.AaFlags, q: AaBQ}
1244	
1245	# Flags: the mode seen (if any) and the audit flag
1246	type AaFlB is Data:
1247	  AaFlB{mode: Maybe<&2, PR.AaMode>, audit: Bool}
1248	
1249	def AaFl.mode_of(+w: List<&2, U32>) -> Maybe<&2, PR.AaMode>:
1250	  Bool.pick(Maybe<&2, PR.AaMode>, X.AaText.is(w, "enforce"), Some{PR.AaModeEnforce{}}, Bool.pick(Maybe<&2, PR.AaMode>, X.AaText.is(w, "complain"), Some{PR.AaModeComplain{}}, Bool.pick(Maybe<&2, PR.AaMode>, X.AaText.is(w, "kill"), Some{PR.AaModeKill{}}, Bool.pick(Maybe<&2, PR.AaMode>, X.AaText.is(w, "unconfined"), Some{PR.AaModeUnconfined{}}, Bool.pick(Maybe<&2, PR.AaMode>, X.AaText.is(w, "default_allow"), Some{PR.AaModeDefaultAllow{}}, Bool.pick(Maybe<&2, PR.AaMode>, X.AaText.is(w, "prompt"), Some{PR.AaModePrompt{}}, None{}))))))
1251	
1252	def AaFl.misc() -> List<&2, String>:
1253	  ["mediate_deleted", "attach_disconnected", "chroot_relative", "debug", "interruptible"]
1254	
1255	def AaFl.mode_eq(a: PR.AaMode, b: PR.AaMode) -> Bool:
1256	  X.AaText.eq(X.AaText.of_string(PR.AaMode.show(a)), X.AaText.of_string(PR.AaMode.show(b)))
1257	
1258	def AaFl.set_mode(b: AaFlB, m: PR.AaMode, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaFlB>:
1259	  match b:
1260	    case AaFlB{old, a}:
1261	      match old:
1262	        case None{}:
1263	          Done{AaFlB{Some{m}, a}}
1264	        case Some{+o}:
1265	          Bool.pick(Result<&2, &2, E.AaError, AaFlB>, AaFl.mode_eq(o, m), Done{AaFlB{Some{o}, a}}, Fail{E.AaSrc.flag(src)})
1266	
1267	def AaFl.word.mode(m: Maybe<&2, PR.AaMode>, +w: List<&2, U32>, +b: AaFlB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaFlB>:
1268	  match m:
1269	    case Some{x}:
1270	      AaFl.set_mode(b, x, src)
1271	    case None{}:
1272	      match b:
1273	        case AaFlB{+mo, +a}:
1274	          Bool.pick(Result<&2, &2, E.AaError, AaFlB>, X.AaText.is(w, "audit"), Done{AaFlB{mo, True{}}}, Bool.pick(Result<&2, &2, E.AaError, AaFlB>, X.AaText.one_of(AaFl.misc(), w), Done{AaFlB{mo, a}}, Fail{E.AaSrc.flag(src)}))
1275	
1276	# kill.signal=SIGNAL and attach_disconnected.path=PATH are accepted and not modelled
1277	def AaFl.step(t: T.AaTerm, +b: AaFlB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaFlB>:
1278	  match t:
1279	    case T.AaTmWord{+w}:
1280	      AaFl.word.mode(AaFl.mode_of(w), w, b, src)
1281	    case T.AaTmCond{+k, v}:
1282	      Bool.pick(Result<&2, &2, E.AaError, AaFlB>, Bool.or(X.AaText.is(k, "kill.signal"), X.AaText.is(k, "attach_disconnected.path")), Done{b}, Fail{E.AaSrc.flag(src)})
1283	    case _:
1284	      Fail{E.AaSrc.flag(src)}
1285	
1286	def AaFl.run(ts: List<&2, T.AaTerm>, b: AaFlB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaFlB>:
1287	  match ts:
1288	    case Nil{}:
1289	      Done{b}
1290	    case Con{t, rest}:
1291	      do Result<&2, &2, E.AaError, AaFlB>:
1292	        b2 : AaFlB <- AaFl.step(t, b, src)
1293	        AaFl.run(rest, b2, src)
1294	
1295	def AaFl.finish(b: AaFlB) -> PR.AaFlags:
1296	  match b:
1297	    case AaFlB{m, a}:
1298	      PR.AaFlags{Maybe.default(&2, PR.AaMode, m, PR.AaModeEnforce{}), a}
1299	
1300	def AaFl.list(xs: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaFlags>:
1301	  do Result<&2, &2, E.AaError, PR.AaFlags>:
1302	    b : AaFlB <- AaFl.run(xs, AaFlB{None{}, False{}}, src)
1303	    return AaFl.finish(b)
1304	
1305	# the flags term: flags=(...) or (...)
1306	def AaFl.term(t: T.AaTerm, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaFlags>:
1307	  match t:
1308	    case T.AaTmList{xs}:
1309	      AaFl.list(xs, src)
1310	    case T.AaTmCond{+k, v}:
1311	      match v:
1312	        case T.AaTmList{xs}:
1313	          Bool.pick(Result<&2, &2, E.AaError, PR.AaFlags>, X.AaText.is(k, "flags"), AaFl.list(xs, src), Fail{E.AaSrc.syntax(src)})
1314	        case _:
1315	          Fail{E.AaSrc.syntax(src)}
1316	    case _:
1317	      Fail{E.AaSrc.syntax(src)}
1318	
1319	# optional flags, and nothing after them
1320	def AaFl.opt(ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaFlags>:
1321	  match ts:
1322	    case Nil{}:
1323	      Done{PR.AaFlags.default()}
1324	    case Con{t, rest}:
1325	      match rest:
1326	        case Nil{}:
1327	          AaFl.term(t, src)
1328	        case Con{x, more}:
1329	          Fail{E.AaSrc.syntax(src)}
1330	
1331	def AaParse.alnum(+c: U32) -> Bool:
1332	  Bool.or(T.AaTerm.letter(c), Bool.and(U32.is_ge(c, 48), U32.is_le(c, 57)))
1333	
1334	# a profile name: a quoted string, or a word starting with a letter, a digit or '/'
1335	def AaParse.name(t: T.AaTerm, +src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, U32>>:
1336	  match t:
1337	    case T.AaTmWord{+w}:
1338	      Bool.pick(Result<&2, &2, E.AaError, List<&2, U32>>, Bool.or(AaParse.alnum(X.AaText.head(w)), U32.is_eq(X.AaText.head(w), 47)), Done{w}, Fail{E.AaSrc.syntax(src)})
1339	    case T.AaTmQuoted{+q}:
1340	      Bool.pick(Result<&2, &2, E.AaError, List<&2, U32>>, X.AaText.is_nil(q), Fail{E.AaSrc.syntax(src)}, Done{q})
1341	    case _:
1342	      Fail{E.AaSrc.syntax(src)}
1343	
1344	def AaParse.attach.glob(r: Result<&2, &2, E.AaError, G.AaGlob>, src: E.AaSrc) -> Result<&2, &2, E.AaError, Maybe<&2, G.AaGlob>>:
1345	  match r:
1346	    case Fail{e}:
1347	      Fail{e}
1348	    case Done{+g}:
1349	      Bool.pick(Result<&2, &2, E.AaError, Maybe<&2, G.AaGlob>>, F.AaFile.rooted(g), Done{Some{g}}, Fail{E.AaSrc.syntax(src)})
1350	
1351	# a name that is an absolute path is also the attachment
1352	def AaParse.self_attach(+name: List<&2, U32>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, Maybe<&2, G.AaGlob>>:
1353	  Bool.pick(Result<&2, &2, E.AaError, Maybe<&2, G.AaGlob>>, U32.is_eq(X.AaText.head(name), 47), AaParse.attach.glob(R.AaRule.glob_text(name, src), src), Done{None{}})
1354	
1355	def AaParse.head.make(kind: Nat, name: List<&2, U32>, attach: Maybe<&2, G.AaGlob>, r: Result<&2, &2, E.AaError, PR.AaFlags>) -> Result<&2, &2, E.AaError, AaHead>:
1356	  match r:
1357	    case Fail{e}:
1358	      Fail{e}
1359	    case Done{f}:
1360	      Done{AaHead{kind, name, attach, f, AaBQ.none()}}
1361	
1362	def AaParse.head.flags_only(ts: List<&2, T.AaTerm>, +name: List<&2, U32>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1363	  do Result<&2, &2, E.AaError, AaHead>:
1364	    a : Maybe<&2, G.AaGlob> <- AaParse.self_attach(name, src)
1365	    AaParse.head.make(0n, name, a, AaFl.opt(ts, src))
1366	
1367	def AaParse.head.attached(t: T.AaTerm, rest: List<&2, T.AaTerm>, name: List<&2, U32>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1368	  do Result<&2, &2, E.AaError, AaHead>:
1369	    g : G.AaGlob <- R.AaRule.glob(t, src)
1370	    a : Maybe<&2, G.AaGlob> <- AaParse.attach.glob(Done{g}, src)
1371	    AaParse.head.make(0n, name, a, AaFl.opt(rest, src))
1372	
1373	# after `profile NAME`: an attachment, then flags
1374	def AaParse.head.profile.rest(ts: List<&2, T.AaTerm>, +name: List<&2, U32>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1375	  match ts:
1376	    case Nil{}:
1377	      do Result<&2, &2, E.AaError, AaHead>:
1378	        a : Maybe<&2, G.AaGlob> <- AaParse.self_attach(name, src)
1379	        return AaHead{0n, name, a, PR.AaFlags.default(), AaBQ.none()}
1380	    case Con{+t, +rest}:
1381	      Bool.pick(Result<&2, &2, E.AaError, AaHead>, F.AaFile.is_path(t), AaParse.head.attached(t, rest, name, src), AaParse.head.flags_only(Con{t, rest}, name, src))
1382	
1383	def AaParse.head.profile(ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1384	  match ts:
1385	    case Nil{}:
1386	      Fail{E.AaSrc.syntax(src)}
1387	    case Con{t, rest}:
1388	      do Result<&2, &2, E.AaError, AaHead>:
1389	        n : List<&2, U32> <- AaParse.name(t, src)
1390	        AaParse.head.profile.rest(rest, n, src)
1391	
1392	def AaParse.head.hat.name(+n: List<&2, U32>, rest: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1393	  Bool.pick(Result<&2, &2, E.AaError, AaHead>, AaParse.alnum(X.AaText.head(n)), AaParse.head.make(1n, n, None{}, AaFl.opt(rest, src)), Fail{E.AaSrc.syntax(src)})
1394	
1395	# hat NAME [FLAGS]
1396	def AaParse.head.hat(ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1397	  match ts:
1398	    case Nil{}:
1399	      Fail{E.AaSrc.syntax(src)}
1400	    case Con{t, rest}:
1401	      match t:
1402	        case T.AaTmWord{w}:
1403	          AaParse.head.hat.name(w, rest, src)
1404	        case _:
1405	          Fail{E.AaSrc.syntax(src)}
1406	
1407	def AaParse.head.qual(qp: AaQP, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1408	  match qp:
1409	    case AaQP{q, rest}:
1410	      match rest:
1411	        case Nil{}:
1412	          Done{AaHead{2n, Nil{}, None{}, PR.AaFlags.default(), q}}
1413	        case Con{x, more}:
1414	          Fail{E.AaSrc.syntax(src)}
1415	
1416	# a path as the head: its name and its attachment
1417	def AaParse.head.path(t: T.AaTerm, rest: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1418	  do Result<&2, &2, E.AaError, AaHead>:
1419	    n : List<&2, U32> <- AaParse.name(t, src)
1420	    AaParse.head.flags_only(rest, n, src)
1421	
1422	def AaParse.head.word(+w: List<&2, U32>, +t: T.AaTerm, +rest: List<&2, T.AaTerm>, +top: Bool, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1423	  Bool.pick(Result<&2, &2, E.AaError, AaHead>, X.AaText.is(w, "profile"), AaParse.head.profile(rest, src), Bool.pick(Result<&2, &2, E.AaError, AaHead>, Bool.and(Bool.not(top), X.AaText.is(w, "hat")), AaParse.head.hat(rest, src), Bool.pick(Result<&2, &2, E.AaError, AaHead>, Bool.and(Bool.not(top), U32.is_eq(X.AaText.head(w), 94)), AaParse.head.hat.name(X.AaText.tail(w), rest, src), Bool.pick(Result<&2, &2, E.AaError, AaHead>, Bool.and(top, F.AaFile.is_path(t)), AaParse.head.path(t, rest, src), Bool.pick(Result<&2, &2, E.AaError, AaHead>, Bool.not(top), AaParse.head.qual(AaQ.parse(Con{t, rest}, 0n, AaBQ.none()), src), Fail{E.AaSrc.syntax(src)})))))
1424	
1425	# the head of a block, at the top level or inside a profile
1426	def AaParse.head(ts: List<&2, T.AaTerm>, +top: Bool, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1427	  match ts:
1428	    case Nil{}:
1429	      Fail{E.AaSrc.syntax(src)}
1430	    case Con{t, rest}:
1431	      match t:
1432	        case T.AaTmWord{+w}:
1433	          AaParse.head.word(w, T.AaTmWord{w}, rest, top, src)
1434	        case T.AaTmQuoted{+q}:
1435	          Bool.pick(Result<&2, &2, E.AaError, AaHead>, top, AaParse.head.path(T.AaTmQuoted{q}, rest, src), Fail{E.AaSrc.syntax(src)})
1436	        case _:
1437	          Fail{E.AaSrc.syntax(src)}
1438	
1439	# Exec conflicts: two rules on the same literal path with different exec modes
1440	
1441	def AaParse.target_eq(a: Maybe<&2, List<&2, U32>>, b: Maybe<&2, List<&2, U32>>) -> Bool:
1442	  match a b:
1443	    case None{} None{}:
1444	      True{}
1445	    case Some{x} Some{y}:
1446	      X.AaText.eq(x, y)
1447	    case _ _:
1448	      False{}
1449	
1450	def AaParse.xconf(a: F.AaFileRule, b: F.AaFileRule) -> Bool:
1451	  match a:
1452	    case F.AaFileRule{q1, t1, g1, p1, e1, tg1}:
1453	      match e1:
1454	        case None{}:
1455	          False{}
1456	        case Some{m1}:
1457	          match b:
1458	            case F.AaFileRule{q2, t2, g2, p2, e2, tg2}:
1459	              match e2:
1460	                case None{}:
1461	                  False{}
1462	                case Some{m2}:
1463	                  Bool.and(Bool.and(G.AaGlob.is_literal(g1), G.AaGlob.is_literal(g2)), Bool.and(X.AaText.eq(t1, t2), Bool.not(Bool.and(F.AaXMode.eq(m1, m2), AaParse.target_eq(tg1, tg2)))))
1464	
1465	def AaParse.xconf.any(+r: F.AaFileRule, rs: List<&2, F.AaFileRule>) -> Bool:
1466	  match rs:
1467	    case Nil{}:
1468	      False{}
1469	    case Con{s, t}:
1470	      Bool.or(AaParse.xconf(r, s), AaParse.xconf.any(r, t))
1471	
1472	def AaParse.conflicts.go(rs: List<&2, F.AaFileRule>) -> Bool:
1473	  match rs:
1474	    case Nil{}:
1475	      False{}
1476	    case Con{+r, +t}:
1477	      Bool.or(AaParse.xconf.any(r, t), AaParse.conflicts.go(t))
1478	
1479	# the allow rules with an exec mode on a literal pattern: the only ones that can conflict
1480	def AaParse.exec_literal(r: F.AaFileRule) -> Bool:
1481	  match r:
1482	    case F.AaFileRule{q, t, g, p, e, tg}:
1483	      match e:
1484	        case None{}:
1485	          False{}
1486	        case Some{m}:
1487	          Bool.and(G.AaGlob.is_literal(g), Bool.not(P.AaQual.deny(q)))
1488	
1489	def AaParse.exec_rules(rs: List<&2, F.AaFileRule>) -> List<&2, F.AaFileRule>:
1490	  match rs:
1491	    case Nil{}:
1492	      Nil{}
1493	    case Con{+r, t}:
1494	      F.AaFileRule.matching.go(AaParse.exec_literal(r), r, AaParse.exec_rules(t))
1495	
1496	def AaParse.conflicts(rs: List<&2, F.AaFileRule>) -> Bool:
1497	  AaParse.conflicts.go(AaParse.exec_rules(rs))
1498	
1499	# change_profile rules with exec conditions must agree on safe and unsafe
1500	# (apparmor_parser 4.0.1 refuses overlapping ones that differ; the package,
1501	# which does not intersect patterns, refuses any allow rules that differ)
1502	def AaParse.cp_applies(r: RX.AaChangeRule) -> Bool:
1503	  match r:
1504	    case RX.AaChangeRule{q, e, s, tg}:
1505	      match e:
1506	        case None{}:
1507	          False{}
1508	        case Some{g}:
1509	          Bool.not(P.AaQual.deny(q))
1510	
1511	def AaParse.cp_safe(r: RX.AaChangeRule) -> Bool:
1512	  match r:
1513	    case RX.AaChangeRule{q, e, s, tg}:
1514	      s
1515	
1516	def AaParse.cp_clash(applies: Bool, +s: Bool, seen: Maybe<&2, Bool>) -> Bool:
1517	  match applies:
1518	    case False{}:
1519	      False{}
1520	    case True{}:
1521	      match seen:
1522	        case None{}:
1523	          False{}
1524	        case Some{x}:
1525	          Bool.xor(x, s)
1526	
1527	def AaParse.cp_next(applies: Bool, s: Bool, +seen: Maybe<&2, Bool>) -> Maybe<&2, Bool>:
1528	  match applies:
1529	    case False{}:
1530	      seen
1531	    case True{}:
1532	      match seen:
1533	        case None{}:
1534	          Some{s}
1535	        case Some{x}:
1536	          Some{x}
1537	
1538	def AaParse.safe_clash(rs: List<&2, RX.AaChangeRule>, +seen: Maybe<&2, Bool>) -> Bool:
1539	  match rs:
1540	    case Nil{}:
1541	      False{}
1542	    case Con{+r, t}:
1543	      Bool.or(AaParse.cp_clash(AaParse.cp_applies(r), AaParse.cp_safe(r), seen), AaParse.safe_clash(t, AaParse.cp_next(AaParse.cp_applies(r), AaParse.cp_safe(r), seen)))
1544	
1545	# Building: a stack of open blocks, innermost first. A profile frame holds
1546	# the profile being built, whether it is a hat, its full name; every frame
1547	# holds the qualifiers in force.
1548	
1549	type AaFrame is Data:
1550	  AaFrame{prof: Maybe<&2, PR.AaProfile>, hat: Bool, full: List<&2, U32>, qual: AaBQ, src: E.AaSrc}
1551	
1552	type AaBuild is Data:
1553	  AaBuild{frames: List<&2, AaFrame>, top: List<&2, PR.AaProfile>, err: Maybe<&2, E.AaError>}
1554	
1555	def AaBuild.fail(b: AaBuild, e: E.AaError) -> AaBuild:
1556	  match b:
1557	    case AaBuild{fs, top, err}:
1558	      match err:
1559	        case None{}:
1560	          AaBuild{fs, top, Some{e}}
1561	        case Some{e0}:
1562	          AaBuild{fs, top, Some{e0}}
1563	
1564	# the innermost profile frame's full name
1565	def AaFrames.full(fs: List<&2, AaFrame>) -> List<&2, U32>:
1566	  match fs:
1567	    case Nil{}:
1568	      Nil{}
1569	    case Con{f, t}:
1570	      match f:
1571	        case AaFrame{p, h, full, q, s}:
1572	          match p:
1573	            case None{}:
1574	              AaFrames.full(t)
1575	            case Some{x}:
1576	              full
1577	
1578	def AaFrames.qual(fs: List<&2, AaFrame>) -> AaBQ:
1579	  match fs:
1580	    case Nil{}:
1581	      AaBQ.none()
1582	    case Con{f, t}:
1583	      match f:
1584	        case AaFrame{p, h, full, q, s}:
1585	          q
1586	
1587	# the rules added to the innermost profile
1588	def AaFrames.add_rules(fs: List<&2, AaFrame>, rs: PR.AaRules) -> List<&2, AaFrame>:
1589	  match fs:
1590	    case Nil{}:
1591	      Nil{}
1592	    case Con{f, t}:
1593	      match f:
1594	        case AaFrame{p, h, full, q, s}:
1595	          match p:
1596	            case None{}:
1597	              Con{AaFrame{None{}, h, full, q, s}, AaFrames.add_rules(t, rs)}
1598	            case Some{x}:
1599	              Con{AaFrame{Some{PR.AaProfile.prepend(x, rs)}, h, full, q, s}, t}
1600	
1601	def AaFrames.names.go(ps: List<&2, PR.AaProfile>) -> List<&2, List<&2, U32>>:
1602	  match ps:
1603	    case Nil{}:
1604	      Nil{}
1605	    case Con{p, t}:
1606	      Con{PR.AaProfile.name(p), AaFrames.names.go(t)}
1607	
1608	def AaFrames.names(+p: PR.AaProfile) -> List<&2, List<&2, U32>>:
1609	  AaFrames.names.go(PR.AaProfile.list_append(PR.AaProfile.children(p), PR.AaProfile.hats(p)))
1610	
1611	def AaFrames.add_sub.go(dup: Bool, +x: PR.AaProfile, k: PR.AaProfile, hat: Bool) -> Maybe<&2, PR.AaProfile>:
1612	  match dup:
1613	    case True{}:
1614	      None{}
1615	    case False{}:
1616	      match hat:
1617	        case True{}:
1618	          Some{PR.AaProfile.add_hat(x, k)}
1619	        case False{}:
1620	          Some{PR.AaProfile.add_child(x, k)}
1621	
1622	def AaFrames.add_sub.put(m: Maybe<&2, PR.AaProfile>, h: Bool, full: List<&2, U32>, q: AaBQ, s: E.AaSrc, t: List<&2, AaFrame>) -> Maybe<&2, List<&2, AaFrame>>:
1623	  match m:
1624	    case None{}:
1625	      None{}
1626	    case Some{y}:
1627	      Some{Con{AaFrame{Some{y}, h, full, q, s}, t}}
1628	
1629	def AaFrames.add_sub.cons(f: AaFrame, m: Maybe<&2, List<&2, AaFrame>>) -> Maybe<&2, List<&2, AaFrame>>:
1630	  match m:
1631	    case None{}:
1632	      None{}
1633	    case Some{t}:
1634	      Some{Con{f, t}}
1635	
1636	# a finished child or hat added to the innermost profile; None if the name is taken
1637	def AaFrames.add_sub(fs: List<&2, AaFrame>, +k: PR.AaProfile, +hat: Bool) -> Maybe<&2, List<&2, AaFrame>>:
1638	  match fs:
1639	    case Nil{}:
1640	      None{}
1641	    case Con{f, t}:
1642	      match f:
1643	        case AaFrame{p, h, full, q, s}:
1644	          match p:
1645	            case None{}:
1646	              AaFrames.add_sub.cons(AaFrame{None{}, h, full, q, s}, AaFrames.add_sub(t, k, hat))
1647	            case Some{+x}:
1648	              AaFrames.add_sub.put(AaFrames.add_sub.go(X.AaText.member(AaFrames.names(x), PR.AaProfile.name(k)), x, k, hat), h, full, q, s, t)
1649	
1650	def AaFrames.has_profile(fs: List<&2, AaFrame>) -> Bool:
1651	  match fs:
1652	    case Nil{}:
1653	      False{}
1654	    case Con{f, t}:
1655	      match f:
1656	        case AaFrame{p, h, full, q, s}:
1657	          match p:
1658	            case None{}:
1659	              AaFrames.has_profile(t)
1660	            case Some{x}:
1661	              True{}
1662	
1663	def AaBuild.top_names(ps: List<&2, PR.AaProfile>) -> List<&2, List<&2, U32>>:
1664	  AaFrames.names.go(ps)
1665	
1666	# a finished profile: checked, and added to its parent or to the top level
1667	def AaBuild.finish.sub(m: Maybe<&2, List<&2, AaFrame>>, top: List<&2, PR.AaProfile>, err: Maybe<&2, E.AaError>, src: E.AaSrc) -> AaBuild:
1668	  match m:
1669	    case None{}:
1670	      AaBuild.fail(AaBuild{Nil{}, top, err}, E.AaSrc.duplicate(src))
1671	    case Some{fs}:
1672	      AaBuild{fs, top, err}
1673	
1674	def AaBuild.finish.top(+p: PR.AaProfile, +top: List<&2, PR.AaProfile>, +err: Maybe<&2, E.AaError>, +src: E.AaSrc) -> AaBuild:
1675	  Bool.pick(AaBuild, X.AaText.member(AaBuild.top_names(top), PR.AaProfile.name(p)), AaBuild.fail(AaBuild{Nil{}, top, err}, E.AaSrc.duplicate(src)), AaBuild{Nil{}, PR.AaProfile.list_append(top, [p]), err})
1676	
1677	def AaBuild.finish.place(nested: Bool, +p: PR.AaProfile, hat: Bool, +fs: List<&2, AaFrame>, +top: List<&2, PR.AaProfile>, +err: Maybe<&2, E.AaError>, +src: E.AaSrc) -> AaBuild:
1678	  match nested:
1679	    case True{}:
1680	      AaBuild.finish.sub(AaFrames.add_sub(fs, p, hat), top, err, src)
1681	    case False{}:
1682	      AaBuild.finish.top(p, top, err, src)
1683	
1684	def AaBuild.finish(+p: PR.AaProfile, +hat: Bool, +fs: List<&2, AaFrame>, +top: List<&2, PR.AaProfile>, +err: Maybe<&2, E.AaError>, +src: E.AaSrc) -> AaBuild:
1685	  Bool.pick(AaBuild, Bool.or(AaParse.conflicts(PR.AaRules.files(PR.AaProfile.rules(p))), AaParse.safe_clash(PR.AaRules.changes(PR.AaProfile.rules(p)), None{})), AaBuild.fail(AaBuild{fs, top, err}, E.AaSrc.exec_conflict(src)), AaBuild.finish.place(AaFrames.has_profile(fs), p, hat, fs, top, err, src))
1686	
1687	def AaBuild.close(b: AaBuild, src: E.AaSrc) -> AaBuild:
1688	  match b:
1689	    case AaBuild{fs, top, err}:
1690	      match fs:
1691	        case Nil{}:
1692	          AaBuild.fail(AaBuild{Nil{}, top, err}, E.AaSrc.syntax(src))
1693	        case Con{f, rest}:
1694	          match f:
1695	            case AaFrame{p, h, full, q, s}:
1696	              match p:
1697	                case None{}:
1698	                  AaBuild{rest, top, err}
1699	                case Some{x}:
1700	                  AaBuild.finish(x, h, rest, top, err, s)
1701	
1702	def AaBuild.push.qual(r: Result<&2, &2, E.AaError, AaBQ>, fs: List<&2, AaFrame>, top: List<&2, PR.AaProfile>, err: Maybe<&2, E.AaError>, src: E.AaSrc) -> AaBuild:
1703	  match r:
1704	    case Fail{e}:
1705	      AaBuild.fail(AaBuild{fs, top, err}, e)
1706	    case Done{q}:
1707	      AaBuild{Con{AaFrame{None{}, False{}, Nil{}, q, src}, fs}, top, err}
1708	
1709	def AaBuild.push.kind(kind: Nat, +fs: List<&2, AaFrame>, top: List<&2, PR.AaProfile>, err: Maybe<&2, E.AaError>, name: List<&2, U32>, attach: Maybe<&2, G.AaGlob>, flags: PR.AaFlags, q: AaBQ, full: List<&2, U32>, +src: E.AaSrc) -> AaBuild:
1710	  match kind:
1711	    case 0n:
1712	      AaBuild{Con{AaFrame{Some{PR.AaProfile.new(name, attach, flags)}, False{}, full, AaBQ.none(), src}, fs}, top, err}
1713	    case 1n+k:
1714	      match k:
1715	        case 0n:
1716	          AaBuild{Con{AaFrame{Some{PR.AaProfile.new(name, attach, flags)}, True{}, full, AaBQ.none(), src}, fs}, top, err}
1717	        case 1n+j:
1718	          AaBuild.push.qual(AaQ.combine(AaFrames.qual(fs), q, src), fs, top, err, src)
1719	
1720	# a block opens
1721	def AaBuild.push(r: Result<&2, &2, E.AaError, AaHead>, b: AaBuild, +src: E.AaSrc) -> AaBuild:
1722	  match r:
1723	    case Fail{e}:
1724	      AaBuild.fail(b, e)
1725	    case Done{hd}:
1726	      match hd:
1727	        case AaHead{kind, +name, attach, flags, q}:
1728	          match b:
1729	            case AaBuild{+fs, top, err}:
1730	              +outer = AaFrames.full(fs)
1731	              +full = Bool.pick(List<&2, U32>, X.AaText.is_nil(outer), name, X.AaText.append(outer, X.AaText.append(X.AaText.of_string("//"), name)))
1732	              AaBuild.push.kind(kind, fs, top, err, name, attach, flags, q, full, src)
1733	
1734	def AaBuild.frames(b: AaBuild) -> List<&2, AaFrame>:
1735	  match b:
1736	    case AaBuild{fs, top, err}:
1737	      fs
1738	
1739	def AaParse.head.of(ts: List<&2, T.AaTok>, +top: Bool, +pname: Maybe<&2, List<&2, U32>>, +ctx: AaCtx, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaHead>:
1740	  do Result<&2, &2, E.AaError, AaHead>:
1741	    xs : List<&2, T.AaTok> <- AaVars.toks(ts, AaCtx.env(ctx), pname, src)
1742	    terms : List<&2, T.AaTerm> <- AaParse.terms(T.AaTerm.of_toks(xs), src)
1743	    AaParse.head(terms, top, src)
1744	
1745	def AaBuild.open(+b: AaBuild, ts: List<&2, T.AaTok>, +ctx: AaCtx, +src: E.AaSrc) -> AaBuild:
1746	  +inside = AaFrames.has_profile(AaBuild.frames(b))
1747	  +pname = Bool.pick(Maybe<&2, List<&2, U32>>, inside, Some{AaFrames.full(AaBuild.frames(b))}, None{})
1748	  AaBuild.push(AaParse.head.of(ts, Bool.not(inside), pname, ctx, src), b, src)
1749	
1750	def AaBuild.rules(r: Result<&2, &2, E.AaError, PR.AaRules>, b: AaBuild) -> AaBuild:
1751	  match r:
1752	    case Fail{e}:
1753	      AaBuild.fail(b, e)
1754	    case Done{rs}:
1755	      match b:
1756	        case AaBuild{fs, top, err}:
1757	          AaBuild{AaFrames.add_rules(fs, rs), top, err}
1758	
1759	# a statement: a rule inside a profile; at the top level the preamble pass has checked it
1760	def AaBuild.stmt(+b: AaBuild, ts: List<&2, T.AaTok>, +ctx: AaCtx, +src: E.AaSrc) -> AaBuild:
1761	  +fs = AaBuild.frames(b)
1762	  Bool.pick(AaBuild, AaFrames.has_profile(fs), AaBuild.rules(AaParse.stmt(ts, AaFrames.qual(fs), AaFrames.full(fs), ctx, src), b), b)
1763	
1764	def AaBuild.ok(b: AaBuild) -> Bool:
1765	  match b:
1766	    case AaBuild{fs, top, err}:
1767	      match err:
1768	        case None{}:
1769	          True{}
1770	        case Some{e}:
1771	          False{}
1772	
1773	def AaBuild.step(+b: AaBuild, it: AaItem, +ctx: AaCtx) -> AaBuild:
1774	  match it:
1775	    case AaIOpen{ts, src}:
1776	      Bool.pick(AaBuild, AaBuild.ok(b), AaBuild.open(b, ts, ctx, src), b)
1777	    case AaIClose{src}:
1778	      Bool.pick(AaBuild, AaBuild.ok(b), AaBuild.close(b, src), b)
1779	    case AaIStmt{ts, src}:
1780	      Bool.pick(AaBuild, AaBuild.ok(b), AaBuild.stmt(b, ts, ctx, src), b)
1781	    case AaIVar{ts, src}:
1782	      b
1783	    case AaIInclude{n, o, src}:
1784	      b
1785	    case AaIError{e}:
1786	      AaBuild.fail(b, e)
1787	
1788	def AaBuild.run(items: List<&2, AaItem>, b: AaBuild, +ctx: AaCtx) -> AaBuild:
1789	  match items:
1790	    case Nil{}:
1791	      b
1792	    case Con{it, rest}:
1793	      AaBuild.run(rest, AaBuild.step(b, it, ctx), ctx)
1794	
1795	def AaBuild.result(b: AaBuild, src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaPolicy>:
1796	  match b:
1797	    case AaBuild{fs, top, err}:
1798	      match fs:
1799	        case Nil{}:
1800	          match err:
1801	            case Some{e}:
1802	              Fail{e}
1803	            case None{}:
1804	              Done{PR.AaPolicy{top}}
1805	        case Con{f, rest}:
1806	          match err:
1807	            case Some{e}:
1808	              Fail{e}
1809	            case None{}:
1810	              Fail{E.AaSrc.syntax(src)}
1811	
1812	# Loading
1813	
1814	def AaParse.pre.result(p: AaPre, items: List<&2, AaItem>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaPolicy>:
1815	  match p:
1816	    case AaPre{env, als, d, s, err}:
1817	      match d:
1818	        case 0n:
1819	          match err:
1820	            case Some{e}:
1821	              Fail{e}
1822	            case None{}:
1823	              AaBuild.result(AaBuild.run(items, AaBuild{Nil{}, Nil{}, None{}}, AaCtx{env, als}), src)
1824	        case 1n+x:
1825	          match err:
1826	            case Some{e}:
1827	              Fail{e}
1828	            case None{}:
1829	              Fail{E.AaSrc.syntax(src)}
1830	
1831	def AaParse.load.items(m: Maybe<&2, E.AaError>, +items: List<&2, AaItem>, +opts: O.AaOptions, +src: E.AaSrc) -> Result<&2, &2, E.AaError, PR.AaPolicy>:
1832	  match m:
1833	    case Some{e}:
1834	      Fail{e}
1835	    case None{}:
1836	      AaParse.pre.result(AaPre.run(items, AaPre{O.AaOptions.vars(opts), Nil{}, 0n, False{}, None{}}), items, src)
1837	
1838	def AaParse.load.file(m: Maybe<&2, AaSrcFile>, +opts: O.AaOptions, +files: List<&2, AaSrcFile>, +main: List<&2, U32>) -> Result<&2, &2, E.AaError, PR.AaPolicy>:
1839	  match m:
1840	    case None{}:
1841	      Fail{E.AaErrInclude{main, 0}}
1842	    case Some{f}:
1843	      match f:
1844	        case AaSrcFile{n, text}:
1845	          +items = AaExpOut.items(AaParse.expand(O.AaOptions.depth(opts), AaParse.items(main, text), files, [[main]], Nil{}))
1846	          AaParse.load.items(AaParse.first_error(items), items, opts, E.AaSrc{main, 0})
1847	
1848	# the policy the file named main defines, reading includes from the file map
1849	def AaParse.load(+opts: O.AaOptions, +files: List<&2, AaSrcFile>, +main: List<&2, U32>) -> Result<&2, &2, E.AaError, PR.AaPolicy>:
1850	  AaParse.load.file(AaParse.find_file(files, main), opts, files, main)