shrink.bend source
shrink.bend on the hub · documented module
# Shrinkers: each maps a value to its simpler candidates, simplest first.# Candidates come as List<&1, T> for every T, so Data and affine types share one runner.# A shrinker never lists its input, so a runner that takes the first failing candidate and# shrinks again halts at a value none of whose candidates fail.# Numbers try 0, then the halving steps n - n/2, n - n/4, ..., n - 1: at most 33 candidates,# and n - 1 is always among them, so a descent reaches the exact failure boundary.# Lists try [], then drop chunks of n/2, n/4, ..., 1 elements (about 2n candidates), then# simplify one element at a time, left to right, through the element's own shrinker.import Baseimport bend-kit-bytes@0.3.1.0/bytes.bend as Bytes# (n - d), then (n - d/2), ..., while d > 0; stop tells whether d is 0.def u32.go(f: Nat, stop: Bool, +n: U32, +d: U32) -> List<&1, U32>: match f stop: case 0n _: Nil{} case 1n+p True{}: Nil{} case 1n+p False{}: +h = (d >> 1n : U32) (n - d : U32) <> u32.go(p, U32.is_eq(h, 0), n, h)# 0, n - n/2, n - n/4, ..., n - 1. None for 0.def u32(n: U32) -> List<&1, U32>: +m = n u32.go(33n, U32.is_eq(m, 0), m, m)def nat.go(f: Nat, stop: Bool, +n: Nat, +d: Nat) -> List<&1, Nat>: match f stop: case 0n _: Nil{} case 1n+p True{}: Nil{} case 1n+p False{}: +h = Nat.div(d, 2n) (n - d : Nat) <> nat.go(p, Nat.is_eq(h, 0n), n, h)# 0n, n - n/2, n - n/4, ..., n - 1. None for 0n.def nat(n: Nat) -> List<&1, Nat>: +m = n nat.go(m, Nat.is_eq(m, 0n), m, m)# Every run of k elements at offsets o, o + k, ... that fits in n; stop tells whether o + k > n.def list.chunks(-A: Data, f: Nat, stop: Bool, +o: Nat, +k: Nat, +n: Nat, +xs: List<&2, A>) -> List<&1, List<&2, A>>: match f stop: case 0n _: Nil{} case 1n+p True{}: Nil{} case 1n+p False{}: +e = (o + k : Nat) List.append(&2, A, List.take(&2, A, xs, o), List.drop(&2, A, xs, e)) <> list.chunks(A, p, Nat.is_gt((e + k : Nat), n), e, k, n, xs)# Chunk deletions for k = n, n/2, ..., 1; k = n is the lone candidate [].def list.dels(-A: Data, f: Nat, stop: Bool, +k: Nat, +n: Nat, +xs: List<&2, A>) -> List<&1, List<&2, A>>: match f stop: case 0n _: Nil{} case 1n+p True{}: Nil{} case 1n+p False{}: +h = Nat.div(k, 2n) List.append(&1, List<&2, A>, list.chunks(A, n, Nat.is_gt(k, n), 0n, k, n, xs), list.dels(A, p, Nat.is_eq(h, 0n), h, n, xs))def list.heads(-A: Data, cs: List<&1, A>, +t: List<&2, A>) -> List<&1, List<&2, A>>: match cs: case Nil{}: Nil{} case c <> r: (c <> t) <> list.heads(A, r, t)def list.cons(-A: Data, +h: A, rs: List<&1, List<&2, A>>) -> List<&1, List<&2, A>>: match rs: case Nil{}: Nil{} case r <> t: (h <> r) <> list.cons(A, h, t)# One element replaced by one of its candidates: the head's first, then the tail's.def list.ones(~A: Data, ~shrink: A -> List<&1, A>, +xs: List<&2, A>) -> List<&1, List<&2, A>>: match xs: case Nil{}: Nil{} case h <> t: List.append(&1, List<&2, A>, list.heads(A, shrink(h), t), list.cons(A, h, list.ones(~A, ~shrink, t)))# [], chunk deletions (halves down to single elements), then single-element simplifications.def list(~A: Data, ~shrink: A -> List<&1, A>, xs: List<&2, A>) -> List<&1, List<&2, A>>: +ys = xs +n = List.length(&2, A, ys) List.append(&1, List<&2, A>, list.dels(A, n, Nat.is_eq(n, 0n), n, n, ys), list.ones(~A, ~shrink, ys))def maybe.some(-A: Data, xs: List<&1, A>) -> List<&1, Maybe<&2, A>>: match xs: case Nil{}: Nil{} case x <> t: Some{x} <> maybe.some(A, t)# None, then Some of each candidate of x. None for None.def maybe(~A: Data, ~shrink: A -> List<&1, A>, m: Maybe<&2, A>) -> List<&1, Maybe<&2, A>>: match m: case None{}: Nil{} case Some{x}: None{} <> maybe.some(A, shrink(x))def char.lift(xs: List<&1, U32>, +base: U32) -> List<&1, Char>: match xs: case Nil{}: Nil{} case x <> t: Chr{(base + x : U32)} <> char.lift(t, base)def char.of(o: Cmp, +c: U32) -> List<&1, Char>: match o: case LT{}: Chr{97} <> char.lift(u32(c), 0) case EQ{}: Nil{} case GT{}: char.lift(u32((c - 97 : U32)), 97)# Toward 'a': a code above it halves toward it; one below tries 'a', then halves toward 0.def char(c: Char) -> List<&1, Char>: match c: case Chr{+x}: char.of(U32.cmp(x, 97), x)def string.of(xs: List<&1, List<&2, Char>>) -> List<&1, String>: match xs: case Nil{}: Nil{} case x <> t: String.from_list(x) <> string.of(t)# A String as a list of Chars under char.def string(s: String) -> List<&1, String>: string.of(list(~Char, ~char, String.to_list(s)))def bytes.codes(s: String) -> List<&2, U32>: match s: case SNil{}: Nil{} case SCon{Chr{x}, t}: x <> bytes.codes(t)def bytes.chars(xs: List<&2, U32>) -> String: match xs: case Nil{}: SNil{} case x <> t: SCon{Chr{x}, bytes.chars(t)}def bytes.of(xs: List<&1, List<&2, U32>>) -> List<&1, Bytes.Bytes>: match xs: case Nil{}: Nil{} case x <> t: Bytes.from_string(bytes.chars(x)) <> bytes.of(t)# Bytes is affine, so this never copies b: it reads the octets out once and builds each# candidate as a fresh buffer, shrinking the octets as a list with bytes toward 0.def bytes(b: Bytes.Bytes) -> List<&1, Bytes.Bytes>: bytes.of(list(~U32, ~u32, bytes.codes(Bytes.to_string(b))))