shrink.bend

bend-kit-property@0.4.0.0 · 169 lines · 21 definitions

1# Shrinkers: each maps a value to its simpler candidates, simplest first.
2# Candidates come as List<&1, T> for every T, so Data and affine types share one runner.
3# A shrinker never lists its input, so a runner that takes the first failing candidate and
4# shrinks again halts at a value none of whose candidates fail.
5# Numbers try 0, then the halving steps n - n/2, n - n/4, ..., n - 1: at most 33 candidates,
6# and n - 1 is always among them, so a descent reaches the exact failure boundary.
7# Lists try [], then drop chunks of n/2, n/4, ..., 1 elements (about 2n candidates), then
8# simplify one element at a time, left to right, through the element's own shrinker.
9import Base
10import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
11
12# (n - d), then (n - d/2), ..., while d > 0; stop tells whether d is 0.
13def u32.go(f: Nat, stop: Bool, +n: U32, +d: U32) -> List<&1, U32>:
14  match f stop:
15    case 0n _:
16      Nil{}
17    case 1n+p True{}:
18      Nil{}
19    case 1n+p False{}:
20      +h = (d >> 1n : U32)
21      (n - d : U32) <> u32.go(p, U32.is_eq(h, 0), n, h)
22
23# 0, n - n/2, n - n/4, ..., n - 1. None for 0.
24def u32(n: U32) -> List<&1, U32>:
25  +m = n
26  u32.go(33n, U32.is_eq(m, 0), m, m)
27
28def nat.go(f: Nat, stop: Bool, +n: Nat, +d: Nat) -> List<&1, Nat>:
29  match f stop:
30    case 0n _:
31      Nil{}
32    case 1n+p True{}:
33      Nil{}
34    case 1n+p False{}:
35      +h = Nat.div(d, 2n)
36      (n - d : Nat) <> nat.go(p, Nat.is_eq(h, 0n), n, h)
37
38# 0n, n - n/2, n - n/4, ..., n - 1. None for 0n.
39def nat(n: Nat) -> List<&1, Nat>:
40  +m = n
41  nat.go(m, Nat.is_eq(m, 0n), m, m)
42
43# Every run of k elements at offsets o, o + k, ... that fits in n; stop tells whether o + k > n.
44def list.chunks(-A: Data, f: Nat, stop: Bool, +o: Nat, +k: Nat, +n: Nat, +xs: List<&2, A>) -> List<&1, List<&2, A>>:
45  match f stop:
46    case 0n _:
47      Nil{}
48    case 1n+p True{}:
49      Nil{}
50    case 1n+p False{}:
51      +e = (o + k : Nat)
52      List.append(&2, A, List.take(&2, A, xs, o), List.drop(&2, A, xs, e))
53        <> list.chunks(A, p, Nat.is_gt((e + k : Nat), n), e, k, n, xs)
54
55# Chunk deletions for k = n, n/2, ..., 1; k = n is the lone candidate [].
56def list.dels(-A: Data, f: Nat, stop: Bool, +k: Nat, +n: Nat, +xs: List<&2, A>) -> List<&1, List<&2, A>>:
57  match f stop:
58    case 0n _:
59      Nil{}
60    case 1n+p True{}:
61      Nil{}
62    case 1n+p False{}:
63      +h = Nat.div(k, 2n)
64      List.append(&1, List<&2, A>, list.chunks(A, n, Nat.is_gt(k, n), 0n, k, n, xs),
65        list.dels(A, p, Nat.is_eq(h, 0n), h, n, xs))
66
67def list.heads(-A: Data, cs: List<&1, A>, +t: List<&2, A>) -> List<&1, List<&2, A>>:
68  match cs:
69    case Nil{}:
70      Nil{}
71    case c <> r:
72      (c <> t) <> list.heads(A, r, t)
73
74def list.cons(-A: Data, +h: A, rs: List<&1, List<&2, A>>) -> List<&1, List<&2, A>>:
75  match rs:
76    case Nil{}:
77      Nil{}
78    case r <> t:
79      (h <> r) <> list.cons(A, h, t)
80
81# One element replaced by one of its candidates: the head's first, then the tail's.
82def list.ones(~A: Data, ~shrink: A -> List<&1, A>, +xs: List<&2, A>) -> List<&1, List<&2, A>>:
83  match xs:
84    case Nil{}:
85      Nil{}
86    case h <> t:
87      List.append(&1, List<&2, A>, list.heads(A, shrink(h), t),
88        list.cons(A, h, list.ones(~A, ~shrink, t)))
89
90# [], chunk deletions (halves down to single elements), then single-element simplifications.
91def list(~A: Data, ~shrink: A -> List<&1, A>, xs: List<&2, A>) -> List<&1, List<&2, A>>:
92  +ys = xs
93  +n = List.length(&2, A, ys)
94  List.append(&1, List<&2, A>, list.dels(A, n, Nat.is_eq(n, 0n), n, n, ys),
95    list.ones(~A, ~shrink, ys))
96
97def maybe.some(-A: Data, xs: List<&1, A>) -> List<&1, Maybe<&2, A>>:
98  match xs:
99    case Nil{}:
100      Nil{}
101    case x <> t:
102      Some{x} <> maybe.some(A, t)
103
104# None, then Some of each candidate of x. None for None.
105def maybe(~A: Data, ~shrink: A -> List<&1, A>, m: Maybe<&2, A>) -> List<&1, Maybe<&2, A>>:
106  match m:
107    case None{}:
108      Nil{}
109    case Some{x}:
110      None{} <> maybe.some(A, shrink(x))
111
112def char.lift(xs: List<&1, U32>, +base: U32) -> List<&1, Char>:
113  match xs:
114    case Nil{}:
115      Nil{}
116    case x <> t:
117      Chr{(base + x : U32)} <> char.lift(t, base)
118
119def char.of(o: Cmp, +c: U32) -> List<&1, Char>:
120  match o:
121    case LT{}:
122      Chr{97} <> char.lift(u32(c), 0)
123    case EQ{}:
124      Nil{}
125    case GT{}:
126      char.lift(u32((c - 97 : U32)), 97)
127
128# Toward 'a': a code above it halves toward it; one below tries 'a', then halves toward 0.
129def char(c: Char) -> List<&1, Char>:
130  match c:
131    case Chr{+x}:
132      char.of(U32.cmp(x, 97), x)
133
134def string.of(xs: List<&1, List<&2, Char>>) -> List<&1, String>:
135  match xs:
136    case Nil{}:
137      Nil{}
138    case x <> t:
139      String.from_list(x) <> string.of(t)
140
141# A String as a list of Chars under char.
142def string(s: String) -> List<&1, String>:
143  string.of(list(~Char, ~char, String.to_list(s)))
144
145def bytes.codes(s: String) -> List<&2, U32>:
146  match s:
147    case SNil{}:
148      Nil{}
149    case SCon{Chr{x}, t}:
150      x <> bytes.codes(t)
151
152def bytes.chars(xs: List<&2, U32>) -> String:
153  match xs:
154    case Nil{}:
155      SNil{}
156    case x <> t:
157      SCon{Chr{x}, bytes.chars(t)}
158
159def bytes.of(xs: List<&1, List<&2, U32>>) -> List<&1, Bytes.Bytes>:
160  match xs:
161    case Nil{}:
162      Nil{}
163    case x <> t:
164      Bytes.from_string(bytes.chars(x)) <> bytes.of(t)
165
166# Bytes is affine, so this never copies b: it reads the octets out once and builds each
167# candidate as a fresh buffer, shrinking the octets as a list with bytes toward 0.
168def bytes(b: Bytes.Bytes) -> List<&1, Bytes.Bytes>:
169  bytes.of(list(~U32, ~u32, bytes.codes(Bytes.to_string(b))))