1	# ezsys/src/str: text helpers that Python's str gives a service for free:
2	# strip with Python's whitespace, replace, split and find on a text
3	# separator, lower and upper case for ASCII, Latin-1, Latin Extended-A,
4	# Greek and Cyrillic, padding and truncation by code point, and the numeric
5	# order of digit strings. Pure; every function walks its text once, left to
6	# right, one code point a step.
7	import Base
8	
9	# --- whitespace ---
10	
11	# Python's whitespace (str.isspace, str.strip with no argument): the code
12	# points 9 to 13, 28 to 32, 133, 160, 5760, 8192 to 8202, 8232, 8233, 8239,
13	# 8287 and 12288
14	def text.spaces() -> List<&2, U32>:
15	  [9, 10, 11, 12, 13, 28, 29, 30, 31, 32, 133, 160, 5760, 8192, 8193, 8194,
16	    8195, 8196, 8197, 8198, 8199, 8200, 8201, 8202, 8232, 8233, 8239, 8287,
17	    12288]
18	
19	# whether a character is Python whitespace
20	def text.space(chr: Char) -> Bool:
21	  match chr:
22	    case Chr{+x}:
23	      List.contains(~U32, ~U32.is_eq, text.spaces(), x)
24	
25	# a character at the start: dropped when it is whitespace, and the rest
26	# stripped too; else the text is kept from it
27	def text.lstrip.if(
28	  sp: Bool,
29	  hd: Char,
30	  tl: String,
31	  more: Unit -> String
32	) -> String:
33	  match sp:
34	    case True{}:
35	      more(Unit{})
36	    case False{}:
37	      SCon{hd, tl}
38	
39	# the text with its leading whitespace removed
40	def text.lstrip(txt: String) -> String:
41	  match txt:
42	    case SNil{}:
43	      SNil{}
44	    case SCon{+h, +t}:
45	      text.lstrip.if(text.space(h), h, t, _u => text.lstrip(t))
46	
47	# a lone last character: gone when it is whitespace
48	def text.rstrip.lone(sp: Bool, hd: Char) -> String:
49	  match sp:
50	    case True{}:
51	      SNil{}
52	    case False{}:
53	      SCon{hd, SNil{}}
54	
55	# a character before the stripped rest: when nothing is left after it, it
56	# goes too if it is whitespace
57	def text.rstrip.put(+hd: Char, rule: String) -> String:
58	  match rule:
59	    case SNil{}:
60	      text.rstrip.lone(text.space(hd), hd)
61	    case SCon{a, b}:
62	      SCon{hd, SCon{a, b}}
63	
64	# the text with its trailing whitespace removed
65	def text.rstrip(txt: String) -> String:
66	  match txt:
67	    case SNil{}:
68	      SNil{}
69	    case SCon{+h, t}:
70	      text.rstrip.put(h, text.rstrip(t))
71	
72	# the text with whitespace removed from both ends
73	def text.strip(txt: String) -> String:
74	  text.rstrip(text.lstrip(txt))
75	
76	# --- replace ---
77	
78	# how many characters of a separator follow its first
79	def text.after(sep: String) -> Nat:
80	  match sep:
81	    case SNil{}:
82	      0n
83	    case SCon{_h, t}:
84	      String.length(t)
85	
86	# a nonempty `old` at this character, or not: write `new` and pass over
87	# the rest of `old`, or write the character
88	def text.replace.at(
89	  hit: Bool,
90	  hd: Char,
91	  +new: String,
92	  +left: Nat,
93	  next: Nat -> String
94	) -> String:
95	  match hit:
96	    case True{}:
97	      new ++ next(left)
98	    case False{}:
99	      SCon{hd, next(0n)}
100	
101	# the scan for a nonempty `old`; `skip` characters of a found `old` are
102	# still to pass over
103	def text.replace.go(
104	  txt: String,
105	  skip: Nat,
106	  +old: String,
107	  +new: String
108	) -> String:
109	  match txt skip:
110	    case SNil{} _:
111	      SNil{}
112	    case SCon{_h, t} 1n+k:
113	      text.replace.go(t, k, old, new)
114	    case SCon{+h, +t} 0n:
115	      text.replace.at(String.starts_with(SCon{h, t}, old), h, new,
116	        text.after(old),
117	        k => text.replace.go(t, k, old, new))
118	
119	# an empty `old`: `new` after every character
120	def text.replace.gaps(txt: String, +new: String) -> String:
121	  match txt:
122	    case SNil{}:
123	      SNil{}
124	    case SCon{h, t}:
125	      SCon{h, new ++ text.replace.gaps(t, new)}
126	
127	# every `old` replaced by `new`, left to right, never overlapping; an empty
128	# `old` puts `new` before every character and at the end
129	def text.replace(txt: String, +old: String, +new: String) -> String:
130	  match old:
131	    case SNil{}:
132	      new ++ text.replace.gaps(txt, new)
133	    case SCon{oh, ot}:
134	      text.replace.go(txt, 0n, SCon{oh, ot}, new)
135	
136	# --- split ---
137	
138	# a character on the front of the first piece
139	def text.split.push(hd: Char, ps: List<&2, String>) -> List<&2, String>:
140	  match ps:
141	    case Nil{}:
142	      [SCon{hd, SNil{}}]
143	    case p <> rest:
144	      SCon{hd, p} <> rest
145	
146	# a separator at this character ends a piece; else the character starts it
147	def text.split.at(
148	  hit: Bool,
149	  hd: Char,
150	  +left: Nat,
151	  next: Nat -> List<&2, String>
152	) -> List<&2, String>:
153	  match hit:
154	    case True{}:
155	      SNil{} <> next(left)
156	    case False{}:
157	      text.split.push(hd, next(0n))
158	
159	# the scan for a nonempty separator; `skip` characters of a found separator
160	# are still to pass over
161	def text.split.go(txt: String, skip: Nat, +sep: String) -> List<&2, String>:
162	  match txt skip:
163	    case SNil{} _:
164	      [SNil{}]
165	    case SCon{_h, t} 1n+k:
166	      text.split.go(t, k, sep)
167	    case SCon{+h, +t} 0n:
168	      text.split.at(String.starts_with(SCon{h, t}, sep), h,
169	        text.after(sep),
170	        k => text.split.go(t, k, sep))
171	
172	# the pieces between the separators, in order; an empty separator splits
173	# nothing
174	def text.split(txt: String, +sep: String) -> List<&2, String>:
175	  match sep:
176	    case SNil{}:
177	      [txt]
178	    case SCon{sh, st}:
179	      text.split.go(txt, 0n, SCon{sh, st})
180	
181	# --- find ---
182	
183	# a place one character further on
184	def text.find.inc(got: Maybe<&2, U32>) -> Maybe<&2, U32>:
185	  match got:
186	    case None{}:
187	      None{}
188	    case Some{+i}:
189	      Some{(i + 1 : U32)}
190	
191	# the needle here, or further on
192	def text.find.at(here: Bool, rest: Unit -> Maybe<&2, U32>) -> Maybe<&2, U32>:
193	  match here:
194	    case True{}:
195	      Some{0}
196	    case False{}:
197	      text.find.inc(rest(Unit{}))
198	
199	# at the end of the text only an empty needle is found
200	def text.find.end(needle: String) -> Maybe<&2, U32>:
201	  match needle:
202	    case SNil{}:
203	      Some{0}
204	    case SCon{_h, _t}:
205	      None{}
206	
207	# the index, in code points, of the first place the needle starts
208	def text.find(txt: String, +needle: String) -> Maybe<&2, U32>:
209	  match txt:
210	    case SNil{}:
211	      text.find.end(needle)
212	    case SCon{+h, +t}:
213	      text.find.at(String.starts_with(SCon{h, t}, needle),
214	        _u => text.find(t, needle))
215	
216	# --- case ---
217	
218	# a run of code points `lo` to `hi`, every `step`-th one from `lo`, mapped
219	# in order onto the code points from `to`
220	type Rule is Data:
221	  Rule{lo: U32, hi: U32, step: U32, to: U32}
222	
223	# a code point that maps to more than one
224	type Multi is Data:
225	  Multi{from: U32, to: String}
226	
227	# whether a rule maps the code point
228	def text.case.covers(rule: Rule, +cp: U32) -> Bool:
229	  match rule:
230	    case Rule{+lo, +hi, +step, _to}:
231	      Bool.and(Bool.and(U32.is_ge(cp, lo), U32.is_le(cp, hi)),
232	        U32.is_eq(((cp - lo) % step : U32), 0))
233	
234	# where a rule maps a code point it covers
235	def text.case.target(rule: Rule, +cp: U32) -> U32:
236	  match rule:
237	    case Rule{+lo, _hi, _step, +to}:
238	      (to + (cp - lo) : U32)
239	
240	# the first rule's mapping, or the rest's
241	def text.case.pick(
242	  hit: Bool,
243	  +rule: Rule,
244	  +cp: U32,
245	  rest: Unit -> U32
246	) -> U32:
247	  match hit:
248	    case True{}:
249	      text.case.target(rule, cp)
250	    case False{}:
251	      rest(Unit{})
252	
253	# the code point the first rule that covers it maps it to; itself when none
254	# does
255	def text.case.apply(rules: List<&2, Rule>, +cp: U32) -> U32:
256	  match rules:
257	    case Nil{}:
258	      cp
259	    case +r <> rest:
260	      text.case.pick(text.case.covers(r, cp), r, cp,
261	        _u => text.case.apply(rest, cp))
262	
263	# this entry's text, or the rest's
264	def text.case.found(
265	  hit: Bool,
266	  to: String,
267	  rest: Unit -> Maybe<&2, String>
268	) -> Maybe<&2, String>:
269	  match hit:
270	    case True{}:
271	      Some{to}
272	    case False{}:
273	      rest(Unit{})
274	
275	# the text a code point that maps to more than one maps to
276	def text.case.multi(ms: List<&2, Multi>, +cp: U32) -> Maybe<&2, String>:
277	  match ms:
278	    case Nil{}:
279	      None{}
280	    case Multi{+from, +to} <> rest:
281	      text.case.found(U32.is_eq(from, cp), to,
282	        _u => text.case.multi(rest, cp))
283	
284	# a multiple mapping's text, or the rules' one code point
285	def text.case.one(
286	  got: Maybe<&2, String>,
287	  +cp: U32,
288	  rules: List<&2, Rule>
289	) -> String:
290	  match got:
291	    case Some{s}:
292	      s
293	    case None{}:
294	      SCon{Chr{text.case.apply(rules, cp)}, SNil{}}
295	
296	# a code point mapped by a table: its multiple mapping, else the rules
297	def text.case.of(
298	  ms: List<&2, Multi>,
299	  rules: List<&2, Rule>,
300	  +cp: U32
301	) -> String:
302	  text.case.one(text.case.multi(ms, cp), cp, rules)
303	
304	# Unicode 13's lowercase mappings (Python's str.lower) of U+0000 to U+017F
305	# and U+0370 to U+04FF that are one code point
306	def text.lower.rules() -> List<&2, Rule>:
307	  [
308	    Rule{65, 90, 1, 97},
309	    Rule{192, 214, 1, 224},
310	    Rule{216, 222, 1, 248},
311	    Rule{256, 302, 2, 257},
312	    Rule{306, 310, 2, 307},
313	    Rule{313, 327, 2, 314},
314	    Rule{330, 374, 2, 331},
315	    Rule{376, 376, 1, 255},
316	    Rule{377, 381, 2, 378},
317	    Rule{880, 882, 2, 881},
318	    Rule{886, 886, 1, 887},
319	    Rule{895, 895, 1, 1011},
320	    Rule{902, 902, 1, 940},
321	    Rule{904, 906, 1, 941},
322	    Rule{908, 908, 1, 972},
323	    Rule{910, 911, 1, 973},
324	    Rule{913, 929, 1, 945},
325	    Rule{931, 939, 1, 963},
326	    Rule{975, 975, 1, 983},
327	    Rule{984, 1006, 2, 985},
328	    Rule{1012, 1012, 1, 952},
329	    Rule{1015, 1015, 1, 1016},
330	    Rule{1017, 1017, 1, 1010},
331	    Rule{1018, 1018, 1, 1019},
332	    Rule{1021, 1023, 1, 891},
333	    Rule{1024, 1039, 1, 1104},
334	    Rule{1040, 1071, 1, 1072},
335	    Rule{1120, 1152, 2, 1121},
336	    Rule{1162, 1214, 2, 1163},
337	    Rule{1216, 1216, 1, 1231},
338	    Rule{1217, 1229, 2, 1218},
339	    Rule{1232, 1278, 2, 1233}
340	  ]
341	
342	# the lowercase mapping of U+0130 is two code points
343	def text.lower.multi() -> List<&2, Multi>:
344	  [Multi{304, "i\u{307}"}]
345	
346	# Unicode 13's uppercase mappings (Python's str.upper) of U+0000 to U+017F
347	# and U+0370 to U+04FF that are one code point
348	def text.upper.rules() -> List<&2, Rule>:
349	  [
350	    Rule{97, 122, 1, 65},
351	    Rule{181, 181, 1, 924},
352	    Rule{224, 246, 1, 192},
353	    Rule{248, 254, 1, 216},
354	    Rule{255, 255, 1, 376},
355	    Rule{257, 303, 2, 256},
356	    Rule{305, 305, 1, 73},
357	    Rule{307, 311, 2, 306},
358	    Rule{314, 328, 2, 313},
359	    Rule{331, 375, 2, 330},
360	    Rule{378, 382, 2, 377},
361	    Rule{383, 383, 1, 83},
362	    Rule{881, 883, 2, 880},
363	    Rule{887, 887, 1, 886},
364	    Rule{891, 893, 1, 1021},
365	    Rule{940, 940, 1, 902},
366	    Rule{941, 943, 1, 904},
367	    Rule{945, 961, 1, 913},
368	    Rule{962, 962, 1, 931},
369	    Rule{963, 971, 1, 931},
370	    Rule{972, 972, 1, 908},
371	    Rule{973, 974, 1, 910},
372	    Rule{976, 976, 1, 914},
373	    Rule{977, 977, 1, 920},
374	    Rule{981, 981, 1, 934},
375	    Rule{982, 982, 1, 928},
376	    Rule{983, 983, 1, 975},
377	    Rule{985, 1007, 2, 984},
378	    Rule{1008, 1008, 1, 922},
379	    Rule{1009, 1009, 1, 929},
380	    Rule{1010, 1010, 1, 1017},
381	    Rule{1011, 1011, 1, 895},
382	    Rule{1013, 1013, 1, 917},
383	    Rule{1016, 1016, 1, 1015},
384	    Rule{1019, 1019, 1, 1018},
385	    Rule{1072, 1103, 1, 1040},
386	    Rule{1104, 1119, 1, 1024},
387	    Rule{1121, 1153, 2, 1120},
388	    Rule{1163, 1215, 2, 1162},
389	    Rule{1218, 1230, 2, 1217},
390	    Rule{1231, 1231, 1, 1216},
391	    Rule{1233, 1279, 2, 1232}
392	  ]
393	
394	# the uppercase mappings of U+00DF, U+0149, U+0390 and U+03B0 are more than
395	# one code point
396	def text.upper.multi() -> List<&2, Multi>:
397	  [
398	    Multi{223, "SS"},
399	    Multi{329, "\u{2BC}N"},
400	    Multi{912, "\u{399}\u{308}\u{301}"},
401	    Multi{944, "\u{3A5}\u{308}\u{301}"}
402	  ]
403	
404	# one character in lowercase
405	def text.lower.char(chr: Char) -> String:
406	  match chr:
407	    case Chr{+x}:
408	      text.case.of(text.lower.multi(), text.lower.rules(), x)
409	
410	# one character in uppercase
411	def text.upper.char(chr: Char) -> String:
412	  match chr:
413	    case Chr{+x}:
414	      text.case.of(text.upper.multi(), text.upper.rules(), x)
415	
416	# the text in lowercase, character by character
417	def text.lower(txt: String) -> String:
418	  match txt:
419	    case SNil{}:
420	      SNil{}
421	    case SCon{h, t}:
422	      text.lower.char(h) ++ text.lower(t)
423	
424	# the text in uppercase, character by character
425	def text.upper(txt: String) -> String:
426	  match txt:
427	    case SNil{}:
428	      SNil{}
429	    case SCon{h, t}:
430	      text.upper.char(h) ++ text.upper(t)
431	
432	# --- width ---
433	
434	# the text with spaces after it up to `n` code points; a longer text is
435	# kept whole
436	def text.pad_right(txt: String, width: Nat) -> String:
437	  match txt width:
438	    case SNil{} k:
439	      String.repeat(" ", k)
440	    case SCon{h, t} 0n:
441	      SCon{h, t}
442	    case SCon{h, t} 1n+k:
443	      SCon{h, text.pad_right(t, k)}
444	
445	# the first `n` code points of the text, or all of it when it is shorter
446	def text.truncate(txt: String, width: Nat) -> String:
447	  match txt width:
448	    case SNil{} _:
449	      SNil{}
450	    case SCon{_h, _t} 0n:
451	      SNil{}
452	    case SCon{h, t} 1n+k:
453	      SCon{h, text.truncate(t, k)}
454	
455	# --- digit strings ---
456	
457	# a leading '0' is dropped, and the zeros after it
458	def text.digits.zero.if(
459	  zero: Bool,
460	  hd: Char,
461	  tl: String,
462	  more: Unit -> String
463	) -> String:
464	  match zero:
465	    case True{}:
466	      more(Unit{})
467	    case False{}:
468	      SCon{hd, tl}
469	
470	# the text with its leading '0's removed
471	def text.digits.trim(txt: String) -> String:
472	  match txt:
473	    case SNil{}:
474	      SNil{}
475	    case SCon{+h, +t}:
476	      text.digits.zero.if(Char.is_eq(h, '0'), h, t,
477	        _u => text.digits.trim(t))
478	
479	# the longer text is the greater; texts of one length compare code point
480	# by code point
481	def text.digits.by(chr: Cmp, +lhs: String, +rhs: String) -> Cmp:
482	  match chr:
483	    case LT{}:
484	      LT{}
485	    case EQ{}:
486	      String.order(lhs, rhs)
487	    case GT{}:
488	      GT{}
489	
490	# two digit strings in numeric order: leading zeros dropped, then the
491	# longer is the greater, and two of one length compare digit by digit
492	def text.digits.cmp(lhs: String, rhs: String) -> Cmp:
493	  +x = text.digits.trim(lhs)
494	  +y = text.digits.trim(rhs)
495	  text.digits.by(Nat.cmp(String.length(x), String.length(y)), x, y)