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.
4	import Base
5	
6	def AaText.is_nil(xs: List<&2, U32>) -> Bool:
7	  match xs:
8	    case Nil{}:
9	      True{}
10	    case Con{h, t}:
11	      False{}
12	
13	def 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	
20	def 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	
27	def AaText.rev(xs: List<&2, U32>) -> List<&2, U32>:
28	  AaText.rev_onto(xs, Nil{})
29	
30	def 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	
37	def 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
49	def 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	
56	def 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
64	def 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
76	def 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
88	def 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	
99	def 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	
110	def 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	
117	def AaText.head(xs: List<&2, U32>) -> U32:
118	  match xs:
119	    case Nil{}:
120	      0
121	    case Con{h, t}:
122	      h
123	
124	def 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
132	def 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
144	def 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
152	def 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
160	def 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
168	def 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
176	type AaSplit is Data:
177	  AaSplit{first: List<&2, U32>, rest: Maybe<&2, List<&2, U32>>}
178	
179	def 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	
187	def 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
191	def 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	
198	def 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)}