1	import Base
2	
3	def take.go(n: Nat, s: String, acc: String) -> String:
4	  match n s:
5	    case 1n+k SCon{c, rest}:
6	      take.go(k, rest, SCon{c, acc})
7	    case _ _:
8	      String.reverse(acc)
9	
10	# The first `n` characters of `s`. Base's String.take is not tail-recursive, so long text would overflow the stack.
11	def take(s: String, n: Nat) -> String:
12	  take.go(n, s, "")
13	
14	# The text of `text` from `beg` to `end`, in code points.
15	def slice(text: String, +beg: U32, end: U32) -> String:
16	  take(String.drop(text, U32.to_nat(beg)), U32.to_nat((end - beg: U32)))
17	
18	def line_start.go(s: String, +i: U32, +at: U32, start: U32, going: Bool) -> U32:
19	  match s going:
20	    case _ False{}:
21	      start
22	    case SNil{} True{}:
23	      start
24	    case SCon{c, rest} True{}:
25	      line_start.go(
26	        rest,
27	        (i + 1: U32),
28	        at,
29	        Bool.pick(U32, Char.is_eq(c, '\n'), (i + 1: U32), start),
30	        U32.is_lt((i + 1: U32), at)
31	      )
32	
33	# Where the line of `text` that holds the offset `at` starts: after the last newline before it.
34	def line_start(text: String, +at: U32) -> U32:
35	  line_start.go(text, 0, at, 0, U32.is_lt(0, at))
36	
37	def line_end.go(s: String, i: U32) -> U32:
38	  match s:
39	    case SNil{}:
40	      i
41	    case SCon{'\n', rest}:
42	      (i + 1: U32)
43	    case SCon{c, rest}:
44	      line_end.go(rest, (i + 1: U32))
45	
46	# Where the line of `text` that starts at `beg` ends: after its newline, or at the end of the text.
47	def line_end(text: String, +beg: U32) -> U32:
48	  line_end.go(String.drop(text, U32.to_nat(beg)), beg)
49	
50	def starts_with(s: String, c: Char) -> Bool:
51	  match s:
52	    case SCon{h, t}:
53	      Char.is_eq(h, c)
54	    case SNil{}:
55	      False{}
56	
57	def before.go(s: String, +sep: Char, acc: String, at: Bool) -> String:
58	  match s at:
59	    case SNil{} _:
60	      ""
61	    case _ True{}:
62	      String.reverse(acc)
63	    case SCon{c, +rest} False{}:
64	      before.go(rest, sep, SCon{c, acc}, starts_with(rest, sep))
65	
66	# What comes before the first `sep` of `s`, or "" if there is none.
67	def before(+s: String, +sep: Char) -> String:
68	  before.go(s, sep, "", starts_with(s, sep))
69	
70	def after_last.go(s: String, +sep: Char, seg: String) -> String:
71	  match s:
72	    case SNil{}:
73	      String.reverse(seg)
74	    case SCon{+c, rest}:
75	      after_last.go(rest, sep, Bool.pick(String, Char.is_eq(c, sep), "", SCon{c, seg}))
76	
77	# What comes after the last `sep` of `s`, or all of `s` if there is none.
78	def after_last(s: String, sep: Char) -> String:
79	  after_last.go(s, sep, "")
80	
81	# The chunks of `chunks` (last first) as one text, before `out`. Each chunk is copied once, so it is linear.
82	def onto(chunks: List<&2, String>, out: String) -> String:
83	  match chunks:
84	    case Nil{}:
85	      out
86	    case Con{c, rest}:
87	      onto(rest, c ++ out)