src/ez/sorted.bend

ezx@1.9.0.0 · 42 lines · 0 definitions

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))