token.bend

bend-osdev-apparmor@0.1.0.0 · 646 lines · 75 definitions

1# bend-osdev-apparmor: the profile language's tokens (apparmor.d(5),
2# "FORMAT"), and the terms a rule is written in.
3#
4# Tokens: words, quoted strings, { } ( ) and the comma that ends a rule. '#'
5# at the start of a token begins a comment to the end of the line, except
6# "#include". Inside a word a '{' ... '}' group is part of the word (a glob),
7# so are ',' inside it and a ',' followed by a word character; a word ends
8# at white space, a '"', a ',' before white space, the end, '}', ')', '#' or
9# ',', a '(' after '=', a ')' inside parentheses, and a '}' outside a group.
10#
11# Terms: a rule's tokens read as words, quoted strings, parenthesised lists,
12# conditions key=value and the arrow ->.
13import Base
14import bend-osdev-apparmor@0.1.0.0/text.bend as X
15
16type AaTok is Data:
17  AaTWord{text: List<&2, U32>, line: U32}
18  AaTQuoted{text: List<&2, U32>, line: U32}
19  AaTOpen{line: U32}
20  AaTClose{line: U32}
21  AaTLParen{line: U32}
22  AaTRParen{line: U32}
23  AaTComma{line: U32}
24
25def AaTok.line(t: AaTok) -> U32:
26  match t:
27    case AaTWord{x, l}:
28      l
29    case AaTQuoted{x, l}:
30      l
31    case AaTOpen{l}:
32      l
33    case AaTClose{l}:
34      l
35    case AaTLParen{l}:
36      l
37    case AaTRParen{l}:
38      l
39    case AaTComma{l}:
40      l
41
42# the token is the word s
43def AaTok.is(t: AaTok, s: String) -> Bool:
44  match t:
45    case AaTWord{x, l}:
46      X.AaText.is(x, s)
47    case AaTQuoted{x, l}:
48      False{}
49    case AaTOpen{l}:
50      False{}
51    case AaTClose{l}:
52      False{}
53    case AaTLParen{l}:
54      False{}
55    case AaTRParen{l}:
56      False{}
57    case AaTComma{l}:
58      False{}
59
60# The lexer
61
62type AaLxMode is Data:
63  AaLxSpace{}
64  AaLxWord{acc: List<&2, U32>, depth: Nat}
65  AaLxQuote{acc: List<&2, U32>, esc: Bool}
66  AaLxHash{n: Nat}
67  AaLxComment{}
68
69# mode, current line, parenthesis depth, tokens (last first), still well
70# formed, and the line of the first fault
71type AaLex is Data:
72  AaLex{mode: AaLxMode, line: U32, pdepth: Nat, out: List<&2, AaTok>, ok: Bool, bad: U32}
73
74type AaLxCh is Data:
75  AaLxCWs{}
76  AaLxCNl{}
77  AaLxCHash{}
78  AaLxCOpen{}
79  AaLxCClose{}
80  AaLxCLP{}
81  AaLxCRP{}
82  AaLxCComma{}
83  AaLxCQuote{}
84  AaLxCOther{}
85
86def AaLxCh.ws(+h: U32) -> Bool:
87  Bool.or(U32.is_eq(h, 32), Bool.or(U32.is_eq(h, 9), Bool.or(U32.is_eq(h, 13), Bool.or(U32.is_eq(h, 11), U32.is_eq(h, 12)))))
88
89def AaLxCh.of(+h: U32) -> AaLxCh:
90  Bool.pick(AaLxCh, AaLxCh.ws(h), AaLxCWs{}, Bool.pick(AaLxCh, U32.is_eq(h, 10), AaLxCNl{}, Bool.pick(AaLxCh, U32.is_eq(h, 35), AaLxCHash{}, Bool.pick(AaLxCh, U32.is_eq(h, 123), AaLxCOpen{}, Bool.pick(AaLxCh, U32.is_eq(h, 125), AaLxCClose{}, Bool.pick(AaLxCh, U32.is_eq(h, 40), AaLxCLP{}, Bool.pick(AaLxCh, U32.is_eq(h, 41), AaLxCRP{}, Bool.pick(AaLxCh, U32.is_eq(h, 44), AaLxCComma{}, Bool.pick(AaLxCh, U32.is_eq(h, 34), AaLxCQuote{}, AaLxCOther{})))))))))
91
92# a character after which a ',' ends a word: white space, the end, '}', ')', '#', ','
93def AaLxCh.ends(+n: U32) -> Bool:
94  Bool.or(AaLxCh.ws(n), Bool.or(U32.is_eq(n, 10), Bool.or(U32.is_eq(n, 0), Bool.or(U32.is_eq(n, 125), Bool.or(U32.is_eq(n, 41), Bool.or(U32.is_eq(n, 35), U32.is_eq(n, 44)))))))
95
96def AaLex.fail(st: AaLex) -> AaLex:
97  match st:
98    case AaLex{m, +l, p, out, +ok, bad}:
99      AaLex{AaLxSpace{}, l, p, out, False{}, Bool.pick(U32, ok, l, bad)}
100
101def AaLex.mode(st: AaLex, m: AaLxMode) -> AaLex:
102  match st:
103    case AaLex{m0, l, p, out, ok, bad}:
104      AaLex{m, l, p, out, ok, bad}
105
106def AaLex.push(st: AaLex, t: AaTok) -> AaLex:
107  match st:
108    case AaLex{m, l, p, out, ok, bad}:
109      AaLex{AaLxSpace{}, l, p, Con{t, out}, ok, bad}
110
111def AaLex.line(st: AaLex) -> U32:
112  match st:
113    case AaLex{m, l, p, out, ok, bad}:
114      l
115
116def AaLex.pdepth(st: AaLex) -> Nat:
117  match st:
118    case AaLex{m, l, p, out, ok, bad}:
119      p
120
121# one more line, the mode unchanged
122def AaLex.bump(st: AaLex) -> AaLex:
123  match st:
124    case AaLex{m, l, p, out, ok, bad}:
125      AaLex{m, U32.add(l, 1), p, out, ok, bad}
126
127def AaLex.newline(st: AaLex) -> AaLex:
128  AaLex.mode(AaLex.bump(st), AaLxSpace{})
129
130def AaLex.open_paren(st: AaLex) -> AaLex:
131  match st:
132    case AaLex{m, +l, p, out, ok, bad}:
133      AaLex{AaLxSpace{}, l, 1n+p, Con{AaTLParen{l}, out}, ok, bad}
134
135def AaLex.close_paren.go(p: Nat, st: AaLex) -> AaLex:
136  match p:
137    case 0n:
138      AaLex.fail(st)
139    case 1n+q:
140      match st:
141        case AaLex{m, +l, p0, out, ok, bad}:
142          AaLex{AaLxSpace{}, l, q, Con{AaTRParen{l}, out}, ok, bad}
143
144def AaLex.close_paren(+st: AaLex) -> AaLex:
145  AaLex.close_paren.go(AaLex.pdepth(st), st)
146
147# the last token is the word "->": a '{' after it starts a pattern
148# (change_profile -> {a,b}), not a block
149def AaLex.after_arrow(st: AaLex) -> Bool:
150  match st:
151    case AaLex{m, l, p, out, ok, bad}:
152      match out:
153        case Nil{}:
154          False{}
155        case Con{t, rest}:
156          AaTok.is(t, "->")
157
158def AaLex.open(+st: AaLex) -> AaLex:
159  Bool.pick(AaLex, AaLex.after_arrow(st), AaLex.mode(st, AaLxWord{[123], 1n}), AaLex.push(st, AaTOpen{AaLex.line(st)}))
160
161# a character between tokens
162def AaLex.space.go(k: AaLxCh, +st: AaLex, h: U32) -> AaLex:
163  match k:
164    case AaLxCOther{}:
165      AaLex.mode(st, AaLxWord{[h], 0n})
166    case AaLxCWs{}:
167      st
168    case AaLxCNl{}:
169      AaLex.newline(st)
170    case AaLxCHash{}:
171      AaLex.mode(st, AaLxHash{0n})
172    case AaLxCOpen{}:
173      AaLex.open(st)
174    case AaLxCClose{}:
175      AaLex.push(st, AaTClose{AaLex.line(st)})
176    case AaLxCLP{}:
177      AaLex.open_paren(st)
178    case AaLxCRP{}:
179      AaLex.close_paren(st)
180    case AaLxCComma{}:
181      AaLex.push(st, AaTComma{AaLex.line(st)})
182    case AaLxCQuote{}:
183      AaLex.mode(st, AaLxQuote{Nil{}, False{}})
184
185def AaLex.space(st: AaLex, +h: U32) -> AaLex:
186  AaLex.space.go(AaLxCh.of(h), st, h)
187
188# the word in acc (last character first) ends
189def AaLex.word_end(+st: AaLex, acc: List<&2, U32>) -> AaLex:
190  AaLex.push(st, AaTWord{X.AaText.rev(acc), AaLex.line(st)})
191
192def AaLex.keep(st: AaLex, acc: List<&2, U32>, depth: Nat, h: U32) -> AaLex:
193  AaLex.mode(st, AaLxWord{Con{h, acc}, depth})
194
195def AaLex.word.comma(keep: Bool, +st: AaLex, acc: List<&2, U32>, depth: Nat, h: U32) -> AaLex:
196  match keep:
197    case True{}:
198      AaLex.keep(st, acc, depth, h)
199    case False{}:
200      +st2 = AaLex.word_end(st, acc)
201      AaLex.push(st2, AaTComma{AaLex.line(st2)})
202
203def AaLex.word.lp(split: Bool, st: AaLex, acc: List<&2, U32>, depth: Nat, h: U32) -> AaLex:
204  match split:
205    case True{}:
206      AaLex.open_paren(AaLex.word_end(st, acc))
207    case False{}:
208      AaLex.keep(st, acc, depth, h)
209
210def AaLex.word.rp(split: Bool, st: AaLex, acc: List<&2, U32>, depth: Nat, h: U32) -> AaLex:
211  match split:
212    case True{}:
213      AaLex.close_paren(AaLex.word_end(st, acc))
214    case False{}:
215      AaLex.keep(st, acc, depth, h)
216
217def AaLex.word.close(depth: Nat, st: AaLex, acc: List<&2, U32>, h: U32) -> AaLex:
218  match depth:
219    case 0n:
220      +st2 = AaLex.word_end(st, acc)
221      AaLex.push(st2, AaTClose{AaLex.line(st2)})
222    case 1n+d:
223      AaLex.keep(st, acc, d, h)
224
225def AaLex.word.go(k: AaLxCh, +st: AaLex, +acc: List<&2, U32>, +depth: Nat, +h: U32, +next: U32) -> AaLex:
226  match k:
227    case AaLxCWs{}:
228      AaLex.space(AaLex.word_end(st, acc), h)
229    case AaLxCNl{}:
230      AaLex.space(AaLex.word_end(st, acc), h)
231    case AaLxCComma{}:
232      AaLex.word.comma(Bool.or(Nat.is_gt(depth, 0n), Bool.not(Bool.or(Nat.is_gt(AaLex.pdepth(st), 0n), AaLxCh.ends(next)))), st, acc, depth, h)
233    case AaLxCLP{}:
234      AaLex.word.lp(Bool.and(Nat.is_eq(depth, 0n), U32.is_eq(X.AaText.head(acc), 61)), st, acc, depth, h)
235    case AaLxCRP{}:
236      AaLex.word.rp(Bool.and(Nat.is_eq(depth, 0n), Nat.is_gt(AaLex.pdepth(st), 0n)), st, acc, depth, h)
237    case AaLxCOpen{}:
238      AaLex.keep(st, acc, 1n+depth, h)
239    case AaLxCClose{}:
240      AaLex.word.close(depth, st, acc, h)
241    case AaLxCQuote{}:
242      AaLex.mode(AaLex.word_end(st, acc), AaLxQuote{Nil{}, False{}})
243    case AaLxCHash{}:
244      AaLex.keep(st, acc, depth, h)
245    case AaLxCOther{}:
246      AaLex.keep(st, acc, depth, h)
247
248def AaLex.quote.go(esc: Bool, +st: AaLex, +acc: List<&2, U32>, +h: U32) -> AaLex:
249  match esc:
250    case True{}:
251      AaLex.mode(st, AaLxQuote{Con{h, acc}, False{}})
252    case False{}:
253      Bool.pick(AaLex, U32.is_eq(h, 92), AaLex.mode(st, AaLxQuote{Con{h, acc}, True{}}), Bool.pick(AaLex, U32.is_eq(h, 34), AaLex.push(st, AaTQuoted{X.AaText.rev(acc), AaLex.line(st)}), Bool.pick(AaLex, U32.is_eq(h, 10), AaLex.mode(AaLex.bump(st), AaLxQuote{Con{h, acc}, False{}}), AaLex.mode(st, AaLxQuote{Con{h, acc}, False{}}))))
254
255# the letters of "include"
256def AaLex.inc(n: Nat) -> U32:
257  match n:
258    case 0n:
259      105
260    case 1n+a:
261      match a:
262        case 0n:
263          110
264        case 1n+b:
265          match b:
266            case 0n:
267              99
268            case 1n+c:
269              match c:
270                case 0n:
271                  108
272                case 1n+d:
273                  match d:
274                    case 0n:
275                      117
276                    case 1n+e:
277                      match e:
278                        case 0n:
279                          100
280                        case 1n+f:
281                          101
282
283def AaLex.comment(+st: AaLex, +h: U32) -> AaLex:
284  Bool.pick(AaLex, U32.is_eq(h, 10), AaLex.newline(st), AaLex.mode(st, AaLxComment{}))
285
286def AaLex.hash.go(more: Bool, +st: AaLex, +n: Nat, +h: U32) -> AaLex:
287  match more:
288    case True{}:
289      Bool.pick(AaLex, U32.is_eq(h, AaLex.inc(n)), AaLex.mode(st, AaLxHash{1n+n}), AaLex.comment(st, h))
290    case False{}:
291      Bool.pick(AaLex, Bool.or(AaLxCh.ws(h), Bool.or(U32.is_eq(h, 10), Bool.or(U32.is_eq(h, 60), U32.is_eq(h, 34)))), AaLex.space(AaLex.push(st, AaTWord{X.AaText.of_string("#include"), AaLex.line(st)}), h), AaLex.comment(st, h))
292
293def AaLex.step.mode(m: AaLxMode, +st: AaLex, +h: U32, +next: U32) -> AaLex:
294  match m:
295    case AaLxSpace{}:
296      AaLex.space(st, h)
297    case AaLxWord{acc, depth}:
298      AaLex.word.go(AaLxCh.of(h), st, acc, depth, h, next)
299    case AaLxQuote{acc, esc}:
300      AaLex.quote.go(esc, st, acc, h)
301    case AaLxHash{+n}:
302      AaLex.hash.go(Nat.is_lt(n, 7n), st, n, h)
303    case AaLxComment{}:
304      AaLex.comment(st, h)
305
306def AaLex.step(st: AaLex, +h: U32, +next: U32) -> AaLex:
307  match st:
308    case AaLex{m, l, p, out, ok, bad}:
309      AaLex.step.mode(m, AaLex{AaLxSpace{}, l, p, out, ok, bad}, h, next)
310
311def AaLex.finish.go(m: AaLxMode, +st: AaLex) -> AaLex:
312  match m:
313    case AaLxSpace{}:
314      st
315    case AaLxWord{acc, depth}:
316      AaLex.word_end(st, acc)
317    case AaLxQuote{acc, esc}:
318      AaLex.fail(st)
319    case AaLxHash{n}:
320      Bool.pick(AaLex, Nat.is_eq(n, 7n), AaLex.push(st, AaTWord{X.AaText.of_string("#include"), AaLex.line(st)}), st)
321    case AaLxComment{}:
322      st
323
324def AaLex.finish.paren(p: Nat, st: AaLex) -> AaLex:
325  match p:
326    case 0n:
327      st
328    case 1n+q:
329      AaLex.fail(st)
330
331def AaLex.finish(st: AaLex) -> AaLex:
332  match st:
333    case AaLex{m, l, p, out, ok, bad}:
334      +st2 = AaLex.finish.go(m, AaLex{AaLxSpace{}, l, p, out, ok, bad})
335      AaLex.finish.paren(AaLex.pdepth(st2), st2)
336
337def AaLex.run(xs: List<&2, U32>, st: AaLex) -> AaLex:
338  match xs:
339    case Nil{}:
340      AaLex.finish(st)
341    case Con{+h, +t}:
342      AaLex.run(t, AaLex.step(st, h, X.AaText.head(t)))
343
344def AaTok.rev_onto(xs: List<&2, AaTok>, acc: List<&2, AaTok>) -> List<&2, AaTok>:
345  match xs:
346    case Nil{}:
347      acc
348    case Con{h, t}:
349      AaTok.rev_onto(t, Con{h, acc})
350
351def AaLex.result(st: AaLex) -> Result<&2, &2, U32, List<&2, AaTok>>:
352  match st:
353    case AaLex{m, l, p, out, ok, bad}:
354      match ok:
355        case True{}:
356          Done{AaTok.rev_onto(out, Nil{})}
357        case False{}:
358          Fail{bad}
359
360# the tokens of a text, or the line of its first fault
361def AaTok.lex(xs: List<&2, U32>) -> Result<&2, &2, U32, List<&2, AaTok>>:
362  AaLex.result(AaLex.run(xs, AaLex{AaLxSpace{}, 1, 0n, Nil{}, True{}, 0}))
363
364# Terms
365
366type AaTerm is Data:
367  AaTmWord{text: List<&2, U32>}
368  AaTmQuoted{text: List<&2, U32>}
369  AaTmList{items: List<&2, AaTerm>}
370  AaTmCond{key: List<&2, U32>, value: AaTerm}
371  AaTmArrow{}
372
373# a character of a condition's key: a letter, a digit, '_' or '.'
374def AaTerm.key_char(+c: U32) -> Bool:
375  Bool.or(Bool.and(U32.is_ge(c, 97), U32.is_le(c, 122)), Bool.or(Bool.and(U32.is_ge(c, 65), U32.is_le(c, 90)), Bool.or(Bool.and(U32.is_ge(c, 48), U32.is_le(c, 57)), Bool.or(U32.is_eq(c, 95), U32.is_eq(c, 46)))))
376
377def AaTerm.letter(+c: U32) -> Bool:
378  Bool.or(Bool.and(U32.is_ge(c, 97), U32.is_le(c, 122)), Bool.and(U32.is_ge(c, 65), U32.is_le(c, 90)))
379
380# a condition's key and the text after its '='
381type AaKV is Data:
382  AaKV{key: List<&2, U32>, rest: List<&2, U32>}
383
384# key=rest: the key (last character first) read so far
385def AaTerm.split.go(xs: List<&2, U32>, +acc: List<&2, U32>) -> Maybe<&2, AaKV>:
386  match xs:
387    case Nil{}:
388      None{}
389    case Con{+h, +t}:
390      Bool.pick(Maybe<&2, AaKV>, U32.is_eq(h, 61), Some{AaKV{X.AaText.rev(acc), t}}, Bool.pick(Maybe<&2, AaKV>, AaTerm.key_char(h), AaTerm.split.go(t, Con{h, acc}), None{}))
391
392# a word key=rest, split, when the key is a letter then key characters
393def AaTerm.split(xs: List<&2, U32>) -> Maybe<&2, AaKV>:
394  match xs:
395    case Nil{}:
396      None{}
397    case Con{+h, t}:
398      Bool.pick(Maybe<&2, AaKV>, AaTerm.letter(h), AaTerm.split.go(Con{h, t}, Nil{}), None{})
399
400# the builder: a stack of open lists (innermost first), each its terms (last
401# first) and a key waiting for its value
402type AaTmFrame is Data:
403  AaTmFrame{acc: List<&2, AaTerm>, key: Maybe<&2, List<&2, U32>>}
404
405type AaTmB is Data:
406  AaTmB{frames: List<&2, AaTmFrame>, ok: Bool}
407
408def AaTmB.fail(b: AaTmB) -> AaTmB:
409  match b:
410    case AaTmB{fs, ok}:
411      AaTmB{fs, False{}}
412
413def AaTmFrame.add(f: AaTmFrame, t: AaTerm) -> AaTmFrame:
414  match f:
415    case AaTmFrame{acc, key}:
416      match key:
417        case None{}:
418          AaTmFrame{Con{t, acc}, None{}}
419        case Some{k}:
420          AaTmFrame{Con{AaTmCond{k, t}, acc}, None{}}
421
422def AaTmB.add(b: AaTmB, t: AaTerm) -> AaTmB:
423  match b:
424    case AaTmB{fs, ok}:
425      match fs:
426        case Nil{}:
427          AaTmB{Nil{}, False{}}
428        case Con{f, rest}:
429          AaTmB{Con{AaTmFrame.add(f, t), rest}, ok}
430
431def AaTmFrame.set_key(f: AaTmFrame, k: List<&2, U32>) -> Maybe<&2, AaTmFrame>:
432  match f:
433    case AaTmFrame{acc, key}:
434      match key:
435        case None{}:
436          Some{AaTmFrame{acc, Some{k}}}
437        case Some{k0}:
438          None{}
439
440def AaTmB.key.go(m: Maybe<&2, AaTmFrame>, rest: List<&2, AaTmFrame>, ok: Bool) -> AaTmB:
441  match m:
442    case None{}:
443      AaTmB{rest, False{}}
444    case Some{f}:
445      AaTmB{Con{f, rest}, ok}
446
447def AaTmB.key(b: AaTmB, k: List<&2, U32>) -> AaTmB:
448  match b:
449    case AaTmB{fs, ok}:
450      match fs:
451        case Nil{}:
452          AaTmB{Nil{}, False{}}
453        case Con{f, rest}:
454          AaTmB.key.go(AaTmFrame.set_key(f, k), rest, ok)
455
456def AaTmB.cond.go(r: List<&2, U32>, b: AaTmB, k: List<&2, U32>) -> AaTmB:
457  match r:
458    case Nil{}:
459      AaTmB.key(b, k)
460    case Con{h, t}:
461      AaTmB.add(b, AaTmCond{k, AaTmWord{Con{h, t}}})
462
463def AaTmB.cond(m: Maybe<&2, AaKV>, b: AaTmB, w: List<&2, U32>) -> AaTmB:
464  match m:
465    case None{}:
466      AaTmB.add(b, AaTmWord{w})
467    case Some{kr}:
468      match kr:
469        case AaKV{k, r}:
470          AaTmB.cond.go(r, b, k)
471
472def AaTmB.word(+b: AaTmB, +w: List<&2, U32>) -> AaTmB:
473  Bool.pick(AaTmB, X.AaText.is(w, "->"), AaTmB.add(b, AaTmArrow{}), AaTmB.cond(AaTerm.split(w), b, w))
474
475def AaTmB.open(b: AaTmB) -> AaTmB:
476  match b:
477    case AaTmB{fs, ok}:
478      AaTmB{Con{AaTmFrame{Nil{}, None{}}, fs}, ok}
479
480def AaTerm.rev_onto(xs: List<&2, AaTerm>, acc: List<&2, AaTerm>) -> List<&2, AaTerm>:
481  match xs:
482    case Nil{}:
483      acc
484    case Con{h, t}:
485      AaTerm.rev_onto(t, Con{h, acc})
486
487def AaTmB.close(b: AaTmB) -> AaTmB:
488  match b:
489    case AaTmB{fs, ok}:
490      match fs:
491        case Nil{}:
492          AaTmB{Nil{}, False{}}
493        case Con{f, rest}:
494          match f:
495            case AaTmFrame{acc, key}:
496              match key:
497                case None{}:
498                  AaTmB.add(AaTmB{rest, ok}, AaTmList{AaTerm.rev_onto(acc, Nil{})})
499                case Some{k}:
500                  AaTmB{rest, False{}}
501
502# inside parentheses a comma separates; elsewhere it is out of place
503def AaTmB.comma(b: AaTmB) -> AaTmB:
504  match b:
505    case AaTmB{fs, ok}:
506      match fs:
507        case Nil{}:
508          AaTmB{Nil{}, False{}}
509        case Con{f, rest}:
510          match rest:
511            case Nil{}:
512              AaTmB{Con{f, Nil{}}, False{}}
513            case Con{g, more}:
514              AaTmB{Con{f, Con{g, more}}, ok}
515
516def AaTmB.step(b: AaTmB, t: AaTok) -> AaTmB:
517  match t:
518    case AaTWord{w, l}:
519      AaTmB.word(b, w)
520    case AaTQuoted{q, l}:
521      AaTmB.add(b, AaTmQuoted{q})
522    case AaTOpen{l}:
523      AaTmB.fail(b)
524    case AaTClose{l}:
525      AaTmB.fail(b)
526    case AaTLParen{l}:
527      AaTmB.open(b)
528    case AaTRParen{l}:
529      AaTmB.close(b)
530    case AaTComma{l}:
531      AaTmB.comma(b)
532
533def AaTmB.run(ts: List<&2, AaTok>, b: AaTmB) -> AaTmB:
534  match ts:
535    case Nil{}:
536      b
537    case Con{t, rest}:
538      AaTmB.run(rest, AaTmB.step(b, t))
539
540def AaTmB.result(b: AaTmB) -> Maybe<&2, List<&2, AaTerm>>:
541  match b:
542    case AaTmB{fs, ok}:
543      match fs:
544        case Nil{}:
545          None{}
546        case Con{f, rest}:
547          match f:
548            case AaTmFrame{acc, key}:
549              match key:
550                case None{}:
551                  match rest:
552                    case Nil{}:
553                      match ok:
554                        case True{}:
555                          Some{AaTerm.rev_onto(acc, Nil{})}
556                        case False{}:
557                          None{}
558                    case Con{g, more}:
559                      None{}
560                case Some{k}:
561                  None{}
562
563# a statement's tokens as terms, or None if its parentheses or conditions are malformed
564def AaTerm.of_toks(ts: List<&2, AaTok>) -> Maybe<&2, List<&2, AaTerm>>:
565  AaTmB.result(AaTmB.run(ts, AaTmB{[AaTmFrame{Nil{}, None{}}], True{}}))
566
567# Reading terms
568
569def AaTerm.is(t: AaTerm, s: String) -> Bool:
570  match t:
571    case AaTmWord{w}:
572      X.AaText.is(w, s)
573    case AaTmQuoted{q}:
574      False{}
575    case AaTmList{xs}:
576      False{}
577    case AaTmCond{k, v}:
578      False{}
579    case AaTmArrow{}:
580      False{}
581
582def AaTerm.is_one_of(t: AaTerm, ns: List<&2, String>) -> Bool:
583  match t:
584    case AaTmWord{w}:
585      X.AaText.one_of(ns, w)
586    case AaTmQuoted{q}:
587      False{}
588    case AaTmList{xs}:
589      False{}
590    case AaTmCond{k, v}:
591      False{}
592    case AaTmArrow{}:
593      False{}
594
595# a word or quoted string's text
596def AaTerm.text(t: AaTerm) -> Maybe<&2, List<&2, U32>>:
597  match t:
598    case AaTmWord{w}:
599      Some{w}
600    case AaTmQuoted{q}:
601      Some{q}
602    case AaTmList{xs}:
603      None{}
604    case AaTmCond{k, v}:
605      None{}
606    case AaTmArrow{}:
607      None{}
608
609# the texts of a value: one word or string, or the words and strings of a list
610def AaTerm.texts.cons(a: Maybe<&2, List<&2, U32>>, b: Maybe<&2, List<&2, List<&2, U32>>>) -> Maybe<&2, List<&2, List<&2, U32>>>:
611  match a:
612    case None{}:
613      None{}
614    case Some{x}:
615      match b:
616        case None{}:
617          None{}
618        case Some{xs}:
619          Some{Con{x, xs}}
620
621def AaTerm.texts.go(xs: List<&2, AaTerm>) -> Maybe<&2, List<&2, List<&2, U32>>>:
622  match xs:
623    case Nil{}:
624      Some{Nil{}}
625    case Con{x, rest}:
626      AaTerm.texts.cons(AaTerm.text(x), AaTerm.texts.go(rest))
627
628def AaTerm.texts(t: AaTerm) -> Maybe<&2, List<&2, List<&2, U32>>>:
629  match t:
630    case AaTmWord{w}:
631      Some{[w]}
632    case AaTmQuoted{q}:
633      Some{[q]}
634    case AaTmList{xs}:
635      AaTerm.texts.go(xs)
636    case AaTmCond{k, v}:
637      None{}
638    case AaTmArrow{}:
639      None{}
640
641def AaTerm.is_arrow(t: AaTerm) -> Bool:
642  match t:
643    case AaTmArrow{}:
644      True{}
645    case _:
646      False{}