shrink.bend
bend-kit-property@0.2.0.0 · 169 lines · 0 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.1.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))))