src/ez/sorted.bend source

src/ez/sorted.bend on the hub · documented module

# ez/sorted: strings in order, sorted by a walk the termination check can read.## Base's List.sort takes its comparison as an erased (`~`) argument and is a# fuelled bottom-up merge sort besides. Bend cannot show either terminates, so# every def whose closure reaches it falls outside the proof guarantees and is# counted unsafe. An insertion shrinks its list at every step and costs nothing,# and the lists here are a handful of hashes.import Base# where one string belongs in a list already sorted, once the rest of that list# has been placed. The recursion is done before the choice, because a def may# not call itself inside a branch.def sort.ins.put(  le: Bool,  +item: String,  head: String,  tail: List<&2, String>,  rest: List<&2, String>) -> List<&2, String>:  match le:    case True{}:      item <> (head <> tail)    case False{}:      head <> rest# one string dropped into a sorted listdef sort.ins(+item: String, ss: List<&2, String>) -> List<&2, String>:  match ss:    case []:      [item]    case +h <> +t:      sort.ins.put(String.is_le(item, h), item, h, t, sort.ins(item, t))# the strings in order. Base's List.sort takes its comparison as an erased# argument and is fuelled besides, so nothing downstream of it can be proved;# an insertion shrinks its list every step and stays inside the check.def sort(ss: List<&2, String>) -> List<&2, String>:  match ss:    case []:      []    case +h <> t:      sort.ins(h, sort(t))