shrink.bend checks
raw source on the hub · import bend-kit-property@0.2.0.0/shrink.bend as Shrink
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.
2 imports
import Base import bend-kit-bytes@0.3.1.0/bytes.bend as Bytes
Definitions
def u32.go source · line 13 · raw
@f:Nat -> @stop:Bool -> @+n:U32 -> @+d:U32 -> List<&1, U32>
(n - d), then (n - d/2), ..., while d > 0; stop tells whether d is 0.
def u32 source · line 24 · raw
@n:U32 -> List<&1, U32>
0, n - n/2, n - n/4, ..., n - 1. None for 0.
def nat.go source · line 28 · raw
@f:Nat -> @stop:Bool -> @+n:Nat -> @+d:Nat -> List<&1, Nat>
def nat source · line 39 · raw
@n:Nat -> List<&1, Nat>
0n, n - n/2, n - n/4, ..., n - 1. None for 0n.
def list.chunks source · line 44 · raw
@-A:Data -> @f:Nat -> @stop:Bool -> @+o:Nat -> @+k:Nat -> @+n:Nat -> @+xs:List<&2, A> -> List<&1, List<&2, A>>
Every run of k elements at offsets o, o + k, ... that fits in n; stop tells whether o + k > n.
def list.dels source · line 56 · raw
@-A:Data -> @f:Nat -> @stop:Bool -> @+k:Nat -> @+n:Nat -> @+xs:List<&2, A> -> List<&1, List<&2, A>>
Chunk deletions for k = n, n/2, ..., 1; k = n is the lone candidate [].
def list.heads source · line 67 · raw
@-A:Data -> @cs:List<&1, A> -> @+t:List<&2, A> -> List<&1, List<&2, A>>
def list.cons source · line 74 · raw
@-A:Data -> @+h:A -> @rs:List<&1, List<&2, A>> -> List<&1, List<&2, A>>
def maybe.some source · line 97 · raw
@-A:Data -> @xs:List<&1, A> -> List<&1, Maybe<&2, A>>
def char.lift source · line 112 · raw
@xs:List<&1, U32> -> @+base:U32 -> List<&1, Char>
def char.of source · line 119 · raw
@o:Cmp -> @+c:U32 -> List<&1, Char>
def char source · line 129 · raw
@c:Char -> List<&1, Char>
Toward 'a': a code above it halves toward it; one below tries 'a', then halves toward 0.
def string.of source · line 134 · raw
@xs:List<&1, List<&2, Char>> -> List<&1, String>
def string source · line 142 · raw
@s:String -> List<&1, String>
A String as a list of Chars under char.
def bytes.codes source · line 145 · raw
@s:String -> List<&2, U32>
def bytes.chars source · line 152 · raw
@xs:List<&2, U32> -> String
def bytes.of source · line 159 · raw
@xs:List<&1, List<&2, U32>> -> List<&1, 0xb7603dcfa1d7f60d01e06c928738cc73/bytes.Bytes>
def bytes source · line 168 · raw
@b:0xb7603dcfa1d7f60d01e06c928738cc73/bytes.Bytes -> List<&1, 0xb7603dcfa1d7f60d01e06c928738cc73/bytes.Bytes>
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.
Templates
template list.ones source · line 82 · raw
@-A:Data -> @-shrink:(@_:A -> List<&1, A>) -> @+xs:List<&2, A> -> List<&1, List<&2, A>>
One element replaced by one of its candidates: the head's first, then the tail's.
template list source · line 91 · raw
@-A:Data -> @-shrink:(@_:A -> List<&1, A>) -> @xs:List<&2, A> -> List<&1, List<&2, A>>
[], chunk deletions (halves down to single elements), then single-element simplifications.
template maybe source · line 105 · raw
@-A:Data -> @-shrink:(@_:A -> List<&1, A>) -> @m:Maybe<&2, A> -> List<&1, Maybe<&2, A>>
None, then Some of each candidate of x. None for None.