1	import Base
2	import ./bytes.bend as B
3	
4	type Utf8.Error is Data:
5	  Truncated{index: Nat}
6	  InvalidByte{index: Nat, value: U32}
7	  Overlong{index: Nat}
8	  Surrogate{index: Nat}
9	  OutOfRange{index: Nat, value: U32}
10	
11	type Utf8.Acc is Data:
12	  AccOk{xs: List<&2, U32>}
13	  AccErr{e: Utf8.Error}
14	
15	type Utf8.DS is Data:
16	  DLead{}
17	  D2{b0: U32}
18	  D3{b0: U32}
19	  D3b{b0: U32, b1: U32}
20	  D4{b0: U32}
21	  D4b{b0: U32, b1: U32}
22	  D4c{b0: U32, b1: U32, b2: U32}
23	  DErr{e: Utf8.Error}
24	
25	def Utf8.is_cont(+b: U32) -> Bool:
26	  Bool.and(U32.is_ge(b, 128), U32.is_le(b, 191))
27	
28	def Utf8.is_sur(+cp: U32) -> Bool:
29	  Bool.and(U32.is_ge(cp, 55296), U32.is_le(cp, 57343))
30	
31	def Utf8.low6(b: U32) -> U32:
32	  U32.and(b, 63)
33	
34	def Utf8.cp2(+b0: U32, +b1: U32) -> U32:
35	  U32.add(U32.shln(U32.and(b0, 31), 6n), Utf8.low6(b1))
36	
37	def Utf8.cp3(+b0: U32, +b1: U32, +b2: U32) -> U32:
38	  U32.add(
39	    U32.shln(U32.and(b0, 15), 12n),
40	    U32.add(U32.shln(Utf8.low6(b1), 6n), Utf8.low6(b2))
41	  )
42	
43	def Utf8.cp4(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> U32:
44	  U32.add(
45	    U32.shln(U32.and(b0, 7), 18n),
46	    U32.add(
47	      U32.shln(Utf8.low6(b1), 12n),
48	      U32.add(U32.shln(Utf8.low6(b2), 6n), Utf8.low6(b3))
49	    )
50	  )
51	
52	def Utf8.bad_cp.sur(sur: Bool) -> Maybe<&2, Utf8.Error>:
53	  match sur:
54	    case True{}:
55	      Some{Surrogate{0n}}
56	    case False{}:
57	      None{}
58	
59	def Utf8.bad_cp.over(over: Bool, sur: Bool) -> Maybe<&2, Utf8.Error>:
60	  match over:
61	    case True{}:
62	      Some{Overlong{0n}}
63	    case False{}:
64	      Utf8.bad_cp.sur(sur)
65	
66	def Utf8.bad_cp.big(
67	  +cp: U32, big: Bool, over: Bool, sur: Bool
68	) -> Maybe<&2, Utf8.Error>:
69	  match big:
70	    case True{}:
71	      Some{OutOfRange{0n, cp}}
72	    case False{}:
73	      Utf8.bad_cp.over(over, sur)
74	
75	def Utf8.bad_cp(+cp: U32, min: U32) -> Maybe<&2, Utf8.Error>:
76	  Utf8.bad_cp.big(
77	    cp, U32.is_gt(cp, 1114111), U32.is_lt(cp, min), Utf8.is_sur(cp)
78	  )
79	
80	def Utf8.fix_idx(e: Utf8.Error, i: Nat) -> Utf8.Error:
81	  match e:
82	    case Truncated{_}:
83	      Truncated{i}
84	    case InvalidByte{_, v}:
85	      InvalidByte{i, v}
86	    case Overlong{_}:
87	      Overlong{i}
88	    case Surrogate{_}:
89	      Surrogate{i}
90	    case OutOfRange{_, v}:
91	      OutOfRange{i, v}
92	
93	def Utf8.st_cp.e(
94	  +cp: U32, i: Nat, e: Maybe<&2, Utf8.Error>
95	) -> Utf8.DS:
96	  match e:
97	    case None{}:
98	      DLead{}
99	    case Some{err}:
100	      DErr{Utf8.fix_idx(err, i)}
101	
102	def Utf8.st_cp(+cp: U32, i: Nat, min: U32) -> Utf8.DS:
103	  Utf8.st_cp.e(cp, i, Utf8.bad_cp(cp, min))
104	
105	def Utf8.push_cp.e(
106	  +cp: U32, acc: String, e: Maybe<&2, Utf8.Error>
107	) -> String:
108	  match e:
109	    case None{}:
110	      SCon{Char.from_u32(cp), acc}
111	    case Some{_}:
112	      acc
113	
114	def Utf8.push_cp(+cp: U32, acc: String, min: U32) -> String:
115	  Utf8.push_cp.e(cp, acc, Utf8.bad_cp(cp, min))
116	
117	def Utf8.st_cont.ok(
118	  +b: U32, i: Nat, next: Utf8.DS, ok: Bool
119	) -> Utf8.DS:
120	  match ok:
121	    case False{}:
122	      DErr{InvalidByte{i, b}}
123	    case True{}:
124	      next
125	
126	def Utf8.st_cont(+b: U32, i: Nat, next: Utf8.DS) -> Utf8.DS:
127	  Utf8.st_cont.ok(b, i, next, Utf8.is_cont(b))
128	
129	def Utf8.class_lead.e(+h: U32, i: Nat, four: Bool) -> Utf8.DS:
130	  match four:
131	    case True{}:
132	      D4{h}
133	    case False{}:
134	      DErr{InvalidByte{i, h}}
135	
136	def Utf8.class_lead.d(+h: U32, i: Nat, three: Bool) -> Utf8.DS:
137	  match three:
138	    case True{}:
139	      D3{h}
140	    case False{}:
141	      Utf8.class_lead.e(h, i, U32.is_le(h, 247))
142	
143	def Utf8.class_lead.c(
144	  +h: U32, i: Nat, two: Bool, three: Bool
145	) -> Utf8.DS:
146	  match two:
147	    case True{}:
148	      D2{h}
149	    case False{}:
150	      Utf8.class_lead.d(h, i, three)
151	
152	def Utf8.class_lead.b(+h: U32, i: Nat, cont: Bool) -> Utf8.DS:
153	  match cont:
154	    case True{}:
155	      DErr{InvalidByte{i, h}}
156	    case False{}:
157	      Utf8.class_lead.c(h, i, U32.is_le(h, 223), U32.is_le(h, 239))
158	
159	def Utf8.class_lead.a(+h: U32, i: Nat, ascii: Bool) -> Utf8.DS:
160	  match ascii:
161	    case True{}:
162	      DLead{}
163	    case False{}:
164	      Utf8.class_lead.b(h, i, U32.is_le(h, 191))
165	
166	def Utf8.class_lead(+h: U32, i: Nat) -> Utf8.DS:
167	  Utf8.class_lead.a(h, i, U32.is_le(h, 127))
168	
169	def Utf8.ascii_acc(+h: U32, acc: String, ascii: Bool) -> String:
170	  match ascii:
171	    case True{}:
172	      SCon{Char.from_u32(h), acc}
173	    case False{}:
174	      acc
175	
176	def Utf8.push2.c(+b0: U32, +b1: U32, acc: String, ok: Bool) -> String:
177	  match ok:
178	    case False{}:
179	      acc
180	    case True{}:
181	      Utf8.push_cp(Utf8.cp2(b0, b1), acc, 128)
182	
183	def Utf8.push2(+b0: U32, +b1: U32, acc: String) -> String:
184	  Utf8.push2.c(b0, b1, acc, Utf8.is_cont(b1))
185	
186	def Utf8.after2.c(+b0: U32, +b1: U32, i: Nat, ok: Bool) -> Utf8.DS:
187	  match ok:
188	    case False{}:
189	      DErr{InvalidByte{i, b1}}
190	    case True{}:
191	      Utf8.st_cp(Utf8.cp2(b0, b1), i, 128)
192	
193	def Utf8.after2(+b0: U32, +b1: U32, i: Nat) -> Utf8.DS:
194	  Utf8.after2.c(b0, b1, i, Utf8.is_cont(b1))
195	
196	def Utf8.push3.c(
197	  +b0: U32, +b1: U32, +b2: U32, acc: String, ok: Bool
198	) -> String:
199	  match ok:
200	    case False{}:
201	      acc
202	    case True{}:
203	      Utf8.push_cp(Utf8.cp3(b0, b1, b2), acc, 2048)
204	
205	def Utf8.push3(+b0: U32, +b1: U32, +b2: U32, acc: String) -> String:
206	  Utf8.push3.c(b0, b1, b2, acc, Utf8.is_cont(b2))
207	
208	def Utf8.after3.c(
209	  +b0: U32, +b1: U32, +b2: U32, i: Nat, ok: Bool
210	) -> Utf8.DS:
211	  match ok:
212	    case False{}:
213	      DErr{InvalidByte{i, b2}}
214	    case True{}:
215	      Utf8.st_cp(Utf8.cp3(b0, b1, b2), i, 2048)
216	
217	def Utf8.after3(+b0: U32, +b1: U32, +b2: U32, i: Nat) -> Utf8.DS:
218	  Utf8.after3.c(b0, b1, b2, i, Utf8.is_cont(b2))
219	
220	def Utf8.push4.c(
221	  +b0: U32, +b1: U32, +b2: U32, +b3: U32, acc: String, ok: Bool
222	) -> String:
223	  match ok:
224	    case False{}:
225	      acc
226	    case True{}:
227	      Utf8.push_cp(Utf8.cp4(b0, b1, b2, b3), acc, 65536)
228	
229	def Utf8.push4(
230	  +b0: U32, +b1: U32, +b2: U32, +b3: U32, acc: String
231	) -> String:
232	  Utf8.push4.c(b0, b1, b2, b3, acc, Utf8.is_cont(b3))
233	
234	def Utf8.after4.c(
235	  +b0: U32, +b1: U32, +b2: U32, +b3: U32, i: Nat, ok: Bool
236	) -> Utf8.DS:
237	  match ok:
238	    case False{}:
239	      DErr{InvalidByte{i, b3}}
240	    case True{}:
241	      Utf8.st_cp(Utf8.cp4(b0, b1, b2, b3), i, 65536)
242	
243	def Utf8.after4(
244	  +b0: U32, +b1: U32, +b2: U32, +b3: U32, i: Nat
245	) -> Utf8.DS:
246	  Utf8.after4.c(b0, b1, b2, b3, i, Utf8.is_cont(b3))
247	
248	def Utf8.dec.go(
249	  xs: List<&2, U32>, st: Utf8.DS, acc: String, +i: Nat
250	) -> Result<&2, &2, Utf8.Error, String>:
251	  match xs st:
252	    case _ DErr{e}:
253	      Fail{e}
254	    case Nil{} DLead{}:
255	      Done{String.reverse(acc)}
256	    case Con{+h, t} DLead{}:
257	      Utf8.dec.go(
258	        t,
259	        Utf8.class_lead(h, i),
260	        Utf8.ascii_acc(h, acc, U32.is_le(h, 127)),
261	        1n+i
262	      )
263	    case Nil{} D2{_}:
264	      Fail{Truncated{i}}
265	    case Con{+b1, t} D2{+b0}:
266	      Utf8.dec.go(t, Utf8.after2(b0, b1, i), Utf8.push2(b0, b1, acc), 1n+i)
267	    case Nil{} D3{_}:
268	      Fail{Truncated{i}}
269	    case Con{+b1, t} D3{+b0}:
270	      Utf8.dec.go(
271	        t, Utf8.st_cont(b1, i, D3b{b0, b1}), acc, 1n+i
272	      )
273	    case Nil{} D3b{_, _}:
274	      Fail{Truncated{i}}
275	    case Con{+b2, t} D3b{+b0, +b1}:
276	      Utf8.dec.go(
277	        t, Utf8.after3(b0, b1, b2, i), Utf8.push3(b0, b1, b2, acc), 1n+i
278	      )
279	    case Nil{} D4{_}:
280	      Fail{Truncated{i}}
281	    case Con{+b1, t} D4{+b0}:
282	      Utf8.dec.go(
283	        t, Utf8.st_cont(b1, i, D4b{b0, b1}), acc, 1n+i
284	      )
285	    case Nil{} D4b{_, _}:
286	      Fail{Truncated{i}}
287	    case Con{+b2, t} D4b{+b0, +b1}:
288	      Utf8.dec.go(
289	        t, Utf8.st_cont(b2, i, D4c{b0, b1, b2}), acc, 1n+i
290	      )
291	    case Nil{} D4c{_, _, _}:
292	      Fail{Truncated{i}}
293	    case Con{+b3, t} D4c{+b0, +b1, +b2}:
294	      Utf8.dec.go(
295	        t,
296	        Utf8.after4(b0, b1, b2, b3, i),
297	        Utf8.push4(b0, b1, b2, b3, acc),
298	        1n+i
299	      )
300	
301	def Utf8.decode(bytes: B.Bytes) -> Result<&2, &2, Utf8.Error, String>:
302	  match bytes:
303	    case B.Bytes{data}:
304	      Utf8.dec.go(data, DLead{}, SNil{}, 0n)
305	
306	def Utf8.emit2(+cp: U32, acc: List<&2, U32>) -> List<&2, U32>:
307	  Con{
308	    U32.or(128, U32.and(cp, 63)),
309	    Con{U32.or(192, U32.shrn(cp, 6n)), acc}
310	  }
311	
312	def Utf8.emit3(+cp: U32, acc: List<&2, U32>) -> List<&2, U32>:
313	  Con{
314	    U32.or(128, U32.and(cp, 63)),
315	    Con{
316	      U32.or(128, U32.and(U32.shrn(cp, 6n), 63)),
317	      Con{U32.or(224, U32.shrn(cp, 12n)), acc}
318	    }
319	  }
320	
321	def Utf8.emit4(+cp: U32, acc: List<&2, U32>) -> List<&2, U32>:
322	  Con{
323	    U32.or(128, U32.and(cp, 63)),
324	    Con{
325	      U32.or(128, U32.and(U32.shrn(cp, 6n), 63)),
326	      Con{
327	        U32.or(128, U32.and(U32.shrn(cp, 12n), 63)),
328	        Con{U32.or(240, U32.shrn(cp, 18n)), acc}
329	      }
330	    }
331	  }
332	
333	def Utf8.emit.e(+cp: U32, acc: List<&2, U32>, b4: Bool) -> Utf8.Acc:
334	  match b4:
335	    case True{}:
336	      AccOk{Utf8.emit4(cp, acc)}
337	    case False{}:
338	      AccErr{OutOfRange{0n, cp}}
339	
340	def Utf8.emit.d(+cp: U32, acc: List<&2, U32>, b3: Bool) -> Utf8.Acc:
341	  match b3:
342	    case True{}:
343	      AccOk{Utf8.emit3(cp, acc)}
344	    case False{}:
345	      Utf8.emit.e(cp, acc, U32.is_le(cp, 1114111))
346	
347	def Utf8.emit.c(
348	  +cp: U32, acc: List<&2, U32>, sur: Bool, b3: Bool
349	) -> Utf8.Acc:
350	  match sur:
351	    case True{}:
352	      AccErr{Surrogate{0n}}
353	    case False{}:
354	      Utf8.emit.d(cp, acc, b3)
355	
356	def Utf8.emit.b(+cp: U32, acc: List<&2, U32>, b2: Bool) -> Utf8.Acc:
357	  match b2:
358	    case True{}:
359	      AccOk{Utf8.emit2(cp, acc)}
360	    case False{}:
361	      Utf8.emit.c(cp, acc, Utf8.is_sur(cp), U32.is_le(cp, 65535))
362	
363	def Utf8.emit.a(
364	  +cp: U32, acc: List<&2, U32>, b1: Bool, b2: Bool
365	) -> Utf8.Acc:
366	  match b1:
367	    case True{}:
368	      AccOk{Con{cp, acc}}
369	    case False{}:
370	      Utf8.emit.b(cp, acc, b2)
371	
372	def Utf8.emit(+cp: U32, acc: List<&2, U32>) -> Utf8.Acc:
373	  Utf8.emit.a(cp, acc, U32.is_le(cp, 127), U32.is_le(cp, 2047))
374	
375	def Utf8.emit_at.fix(a: Utf8.Acc, i: Nat) -> Utf8.Acc:
376	  match a:
377	    case AccOk{xs}:
378	      AccOk{xs}
379	    case AccErr{e}:
380	      AccErr{Utf8.fix_idx(e, i)}
381	
382	def Utf8.emit_at(cp: U32, acc: List<&2, U32>, i: Nat) -> Utf8.Acc:
383	  Utf8.emit_at.fix(Utf8.emit(cp, acc), i)
384	
385	def Utf8.enc.go(
386	  s: String, acc: Utf8.Acc, +i: Nat
387	) -> Result<&2, &2, Utf8.Error, B.Bytes>:
388	  match s acc:
389	    case _ AccErr{e}:
390	      Fail{e}
391	    case SNil{} AccOk{xs}:
392	      Done{B.Bytes{List.reverse(&2, U32, xs)}}
393	    case SCon{h, t} AccOk{xs}:
394	      Utf8.enc.go(t, Utf8.emit_at(Char.to_u32(h), xs, i), 1n+i)
395	
396	def Utf8.encode(text: String) -> Result<&2, &2, Utf8.Error, B.Bytes>:
397	  Utf8.enc.go(text, AccOk{Nil{}}, 0n)