src/ez/sorted.bend
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.
8import 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.
13def 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
27def 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.
37def sort(ss: List<&2, String>) -> List<&2, String>:
38 match ss:
39 case []:
40 []
41 case +h <> t:
42 sort.ins(h, sort(t))