text.bend

bend-osdev-apparmor@0.1.0.0 · 203 lines · 25 definitions

1# bend-osdev-apparmor: byte-string helpers on List<&2, U32>, the form the
2# package works on inside (profile text, names, paths). Public interfaces take
3# Octets (bend-osdev-bytes) and convert once.
4import Base
5
6def AaText.is_nil(xs: List<&2, U32>) -> Bool:
7  match xs:
8    case Nil{}:
9      True{}
10    case Con{h, t}:
11      False{}
12
13def AaText.append(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
14  match xs:
15    case Nil{}:
16      ys
17    case Con{h, t}:
18      Con{h, AaText.append(t, ys)}
19
20def AaText.rev_onto(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
21  match xs:
22    case Nil{}:
23      acc
24    case Con{h, t}:
25      AaText.rev_onto(t, Con{h, acc})
26
27def AaText.rev(xs: List<&2, U32>) -> List<&2, U32>:
28  AaText.rev_onto(xs, Nil{})
29
30def AaText.len(xs: List<&2, U32>) -> Nat:
31  match xs:
32    case Nil{}:
33      0n
34    case Con{h, t}:
35      1n+AaText.len(t)
36
37def AaText.eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
38  match xs ys:
39    case Nil{} Nil{}:
40      True{}
41    case Nil{} Con{h, t}:
42      False{}
43    case Con{h, t} Nil{}:
44      False{}
45    case Con{a, as} Con{b, bs}:
46      Bool.and(U32.is_eq(a, b), AaText.eq(as, bs))
47
48# the codes of a string's characters
49def AaText.of_string(s: String) -> List<&2, U32>:
50  match s:
51    case SNil{}:
52      Nil{}
53    case SCon{c, t}:
54      Con{Char.to_u32(c), AaText.of_string(t)}
55
56def AaText.to_string(xs: List<&2, U32>) -> String:
57  match xs:
58    case Nil{}:
59      SNil{}
60    case Con{h, t}:
61      SCon{Char.from_u32(h), AaText.to_string(t)}
62
63# xs is exactly the string s
64def AaText.is(xs: List<&2, U32>, s: String) -> Bool:
65  match xs s:
66    case Nil{} SNil{}:
67      True{}
68    case Nil{} SCon{c, t}:
69      False{}
70    case Con{h, t} SNil{}:
71      False{}
72    case Con{h, t} SCon{c, u}:
73      Bool.and(U32.is_eq(h, Char.to_u32(c)), AaText.is(t, u))
74
75# xs begins with the string s
76def AaText.starts(xs: List<&2, U32>, s: String) -> Bool:
77  match xs s:
78    case Nil{} SNil{}:
79      True{}
80    case Nil{} SCon{c, t}:
81      False{}
82    case Con{h, t} SNil{}:
83      True{}
84    case Con{h, t} SCon{c, u}:
85      Bool.and(U32.is_eq(h, Char.to_u32(c)), AaText.starts(t, u))
86
87# xs begins with ys
88def AaText.prefix(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
89  match xs ys:
90    case Nil{} Nil{}:
91      True{}
92    case Nil{} Con{c, t}:
93      False{}
94    case Con{h, t} Nil{}:
95      True{}
96    case Con{h, t} Con{c, u}:
97      Bool.and(U32.is_eq(h, c), AaText.prefix(t, u))
98
99def AaText.drop(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
100  match n:
101    case 0n:
102      xs
103    case 1n+p:
104      match xs:
105        case Nil{}:
106          Nil{}
107        case Con{h, t}:
108          AaText.drop(p, t)
109
110def AaText.has(xs: List<&2, U32>, +c: U32) -> Bool:
111  match xs:
112    case Nil{}:
113      False{}
114    case Con{h, t}:
115      Bool.or(U32.is_eq(h, c), AaText.has(t, c))
116
117def AaText.head(xs: List<&2, U32>) -> U32:
118  match xs:
119    case Nil{}:
120      0
121    case Con{h, t}:
122      h
123
124def AaText.last(xs: List<&2, U32>, l: U32) -> U32:
125  match xs:
126    case Nil{}:
127      l
128    case Con{h, t}:
129      AaText.last(t, h)
130
131# the list without its last element
132def AaText.init(xs: List<&2, U32>) -> List<&2, U32>:
133  match xs:
134    case Nil{}:
135      Nil{}
136    case Con{h, t}:
137      match t:
138        case Nil{}:
139          Nil{}
140        case Con{a, b}:
141          Con{h, AaText.init(Con{a, b})}
142
143# x is one of the names xs
144def AaText.member(xs: List<&2, List<&2, U32>>, +x: List<&2, U32>) -> Bool:
145  match xs:
146    case Nil{}:
147      False{}
148    case Con{h, t}:
149      Bool.or(AaText.eq(h, x), AaText.member(t, x))
150
151# s is one of the strings ns
152def AaText.one_of(ns: List<&2, String>, +s: List<&2, U32>) -> Bool:
153  match ns:
154    case Nil{}:
155      False{}
156    case Con{h, t}:
157      Bool.or(AaText.is(s, h), AaText.one_of(t, s))
158
159# every name of xs is one of ys
160def AaText.subset(xs: List<&2, List<&2, U32>>, +ys: List<&2, List<&2, U32>>) -> Bool:
161  match xs:
162    case Nil{}:
163      True{}
164    case Con{h, t}:
165      Bool.and(AaText.member(ys, h), AaText.subset(t, ys))
166
167# split at the first "//": the text before it, and the rest after it
168def AaText.tail(xs: List<&2, U32>) -> List<&2, U32>:
169  match xs:
170    case Nil{}:
171      Nil{}
172    case Con{h, t}:
173      t
174
175# a name cut at its first "//": the part before it, and the rest after it
176type AaSplit is Data:
177  AaSplit{first: List<&2, U32>, rest: Maybe<&2, List<&2, U32>>}
178
179def AaText.split2.go(xs: List<&2, U32>, +prev: Bool, +acc: List<&2, U32>) -> AaSplit:
180  match xs:
181    case Nil{}:
182      AaSplit{AaText.rev(acc), None{}}
183    case Con{+h, +t}:
184      +slash = U32.is_eq(h, 47)
185      Bool.pick(AaSplit, Bool.and(prev, slash), AaSplit{AaText.rev(AaText.tail(acc)), Some{t}}, AaText.split2.go(t, slash, Con{h, acc}))
186
187def AaText.split2(xs: List<&2, U32>) -> AaSplit:
188  AaText.split2.go(xs, False{}, Nil{})
189
190# the split of a rest, if there is one
191def AaText.split2.opt(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, AaSplit>:
192  match m:
193    case None{}:
194      None{}
195    case Some{xs}:
196      Some{AaText.split2(xs)}
197
198def AaText.lappend(xs: List<&2, List<&2, U32>>, ys: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
199  match xs:
200    case Nil{}:
201      ys
202    case Con{h, t}:
203      Con{h, AaText.lappend(t, ys)}