1	# ez/sorted: strings in order, sorted by a walk the termination check can read.
2	#
3	# Base's List.sort takes its comparison as an erased (`~`) argument and is a
4	# fuelled bottom-up merge sort besides. Bend cannot show either terminates, so
5	# every def whose closure reaches it falls outside the proof guarantees and is
6	# counted unsafe. An insertion shrinks its list at every step and costs nothing,
7	# and the lists here are a handful of hashes.
8	import Base
9	
10	# where one string belongs in a list already sorted, once the rest of that list
11	# has been placed. The recursion is done before the choice, because a def may
12	# not call itself inside a branch.
13	def sort.ins.put(
14	  le: Bool,
15	  +item: String,
16	  head: String,
17	  tail: List<&2, String>,
18	  rest: List<&2, String>
19	) -> List<&2, String>:
20	  match le:
21	    case True{}:
22	      item <> (head <> tail)
23	    case False{}:
24	      head <> rest
25	
26	# one string dropped into a sorted list
27	def sort.ins(+item: String, ss: List<&2, String>) -> List<&2, String>:
28	  match ss:
29	    case []:
30	      [item]
31	    case +h <> +t:
32	      sort.ins.put(String.is_le(item, h), item, h, t, sort.ins(item, t))
33	
34	# the strings in order. Base's List.sort takes its comparison as an erased
35	# argument and is fuelled besides, so nothing downstream of it can be proved;
36	# an insertion shrinks its list every step and stays inside the check.
37	def sort(ss: List<&2, String>) -> List<&2, String>:
38	  match ss:
39	    case []:
40	      []
41	    case +h <> t:
42	      sort.ins(h, sort(t))