bend-kit-property Releases (4): 0.4.0.0 0x8505247e2ece13e96984c45de190878c indexed https://jend.leeeet.dev/files.txt?path=bend-kit-property@0.4.0.0 0.3.0.0 0x1ab394b06520ad11584bde1d8d187794 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-property@0.3.0.0 0.2.0.0 0x37dffd823fd9cfaa0f8d0b8861238158 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-property@0.2.0.0 0.1.0.0 0x3d583666c77e74b1325ef80c1d9aa07f unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-property@0.1.0.0 Definitions (67): Generate.cap (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=cap) # n, capped at 1024. def cap(+n: U32) -> U32: Generate.u32 (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=u32) # A uniform U32. def u32(r: Rand.Rng) -> U32 & Rand.Rng: Generate.u32.range (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=u32.range) # A uniform U32 in [lo, hi); lo when hi <= lo + 1. def u32.range(+lo: U32, hi: U32, r: Rand.Rng) -> U32 & Rand.Rng: Generate.size (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=size) # A uniform size in [0, min(max, 1024)]. def size(+max: U32, r: Rand.Rng) -> U32 & Rand.Rng: Generate.nat.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=nat.fin) def nat.fin(xr: U32 & Rand.Rng) -> Nat & Rand.Rng: Generate.nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=nat) # A uniform Nat in [0, min(max, 1024)]. def nat(+max: U32, r: Rand.Rng) -> Nat & Rand.Rng: Generate.char.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=char.fin) def char.fin(xr: U32 & Rand.Rng) -> Char & Rand.Rng: Generate.char (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=char) # A printable ASCII char, ' ' (32) through '~' (126). def char(r: Rand.Rng) -> Char & Rand.Rng: Generate.string.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=string.go) # n + 1 chars prepended to acc; cr holds the next char. def string.go(n: Nat, acc: String, cr: Char & Rand.Rng) -> String & Rand.Rng: Generate.string.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=string.of) # Exactly n printable ASCII chars. def string.of(n: Nat, r: Rand.Rng) -> String & Rand.Rng: Generate.string.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=string.fin) def string.fin(nr: Nat & Rand.Rng) -> String & Rand.Rng: Generate.string (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=string) # Printable ASCII of length in [0, min(max, 1024)]. def string(+max: U32, r: Rand.Rng) -> String & Rand.Rng: Generate.bytes.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=bytes.go) # Byte i and the n bytes after it; xr holds byte i (Bytes.set keeps its low 8 bits). def bytes.go(n: Nat, b: Bytes.Bytes, +i: U32, xr: U32 & Rand.Rng) -> Bytes.Bytes & Rand.Rng: Generate.bytes.start (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=bytes.start) def bytes.start(n: Nat, +len: U32, r: Rand.Rng) -> Bytes.Bytes & Rand.Rng: Generate.bytes.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=bytes.of) # Exactly min(len, 1024) uniform octets, one draw each. def bytes.of(+len: U32, r: Rand.Rng) -> Bytes.Bytes & Rand.Rng: Generate.bytes.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=bytes.fin) def bytes.fin(nr: U32 & Rand.Rng) -> Bytes.Bytes & Rand.Rng: Generate.bytes (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=bytes) # Uniform octets, length in [0, min(max, 1024)]. def bytes(+max: U32, r: Rand.Rng) -> Bytes.Bytes & Rand.Rng: Generate.list.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=list.go) # n + 1 items prepended to acc; hr holds the next item. def list.go(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, n: Nat, acc: List<&2, T>, hr: T & Rand.Rng) -> List<&2, T> & Rand.Rng: Generate.list.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=list.of) # Exactly n items from gen. The first draw ends up last; replay is unaffected. def list.of(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, n: Nat, r: Rand.Rng) -> List<&2, T> & Rand.Rng: Generate.list.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=list.fin) def list.fin(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, nr: Nat & Rand.Rng) -> List<&2, T> & Rand.Rng: Generate.list (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=list) # Items from gen, length in [0, min(max, 1024)]. def list(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, +max: U32, r: Rand.Rng) -> List<&2, T> & Rand.Rng: Generate.maybe.some (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=maybe.some) def maybe.some(~T: Data, hr: T & Rand.Rng) -> Maybe<&2, T> & Rand.Rng: Generate.maybe.if (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=maybe.if) def maybe.if(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, none: Bool, r: Rand.Rng) -> Maybe<&2, T> & Rand.Rng: Generate.maybe.pick (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=maybe.pick) def maybe.pick(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, xr: U32 & Rand.Rng) -> Maybe<&2, T> & Rand.Rng: Generate.maybe (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=maybe) # None one time in four, else Some from gen. def maybe(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, r: Rand.Rng) -> Maybe<&2, T> & Rand.Rng: Generate.map.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=map.fin) def map.fin(~A: Type, ~B: Type, ~f: A -> B, ar: A & Rand.Rng) -> B & Rand.Rng: Generate.map (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=map) # gen's value through f. def map(~A: Type, ~B: Type, ~f: A -> B, ~gen: Rand.Rng -> A & Rand.Rng, r: Rand.Rng) -> B & Rand.Rng: Generate.bind.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=bind.fin) def bind.fin(~A: Type, ~B: Type, ~k: A -> Rand.Rng -> B & Rand.Rng, ar: A & Rand.Rng) -> B & Rand.Rng: Generate.bind (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=bind) # gen's value picks the next generator: bind(~Nat, ~List<&2, U32>, ~(r => Gen.nat(8, r)), ~(n => r => Gen.list.of(~U32, ~Gen.u32, n, r)), r). def bind(~A: Type, ~B: Type, ~gen: Rand.Rng -> A & Rand.Rng, ~k: A -> Rand.Rng -> B & Rand.Rng, r: Rand.Rng) -> B & Rand.Rng: Generate.pair.snd (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=pair.snd) def pair.snd(~A: Type, ~B: Type, a: A, br: B & Rand.Rng) -> (A & B) & Rand.Rng: Generate.pair.fst (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=pair.fst) def pair.fst(~A: Type, ~B: Type, ~gb: Rand.Rng -> B & Rand.Rng, ar: A & Rand.Rng) -> (A & B) & Rand.Rng: Generate.pair (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/generate.bend&name=pair) # ga's value then gb's, drawn in that order. def pair(~A: Type, ~B: Type, ~ga: Rand.Rng -> A & Rand.Rng, ~gb: Rand.Rng -> B & Rand.Rng, r: Rand.Rng) -> (A & B) & Rand.Rng: Property.Failure (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=Failure) type Failure<-T: Type> is Type: Failure{seed: U32, trial: Nat, value: T} Property.smaller (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=smaller) # Scan candidates in order; a predicate returns its input so affine values work. def smaller(~T: Type, ~test: T -> T & Bool, xs: List<&1, T>, tested: T & Bool) -> Maybe<&1, T>: Property.smaller.start (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=smaller.start) def smaller.start(~T: Type, ~test: T -> T & Bool, xs: List<&1, T>) -> Maybe<&1, T>: Property.attempt.pair (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=attempt.pair) def attempt.pair(~T: Type, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, pair: T & T) -> T & Maybe<&1, T>: Property.attempt (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=attempt) def attempt(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, value: T) -> T & Maybe<&1, T>: Property.minimize (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=minimize) # Each accepted failure restarts shrinking; fuel bounds user-supplied shrinkers. def minimize(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, fuel: Nat, state: T & Maybe<&1, T>) -> T: Property.minimize.start (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=minimize.start) def minimize.start(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, value: T) -> T: Property.draw.pair (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=draw.pair) def draw.pair(~T: Type, ~test: T -> T & Bool, pair: T & Rand.Rng) -> (T & Bool) & Rand.Rng: Property.draw (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=draw) def draw(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~test: T -> T & Bool, rng: Rand.Rng) -> (T & Bool) & Rand.Rng: Property.check.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=check.go) def check.go(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, remaining: Nat, +seed: U32, +trial: Nat, state: (T & Bool) & Rand.Rng) -> Maybe<&1, Failure>: Property.check.start (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=check.start) def check.start(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, remaining: Nat, seed: U32, rng: Rand.Rng) -> Maybe<&1, Failure>: Property.check (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=check) # Return the first failure and its smallest reachable counterexample. def check(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, +seed: U32, trials: Nat) -> Maybe<&1, Failure>: Property.report (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=report) # Print the seed and draw index so a failing check can be replayed. def report(~T: Type, ~show: T -> String, result: Maybe<&1, Failure>) -> IO(Bool): Property.run (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/property.bend&name=run) def run(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, ~show: T -> String, seed: U32, trials: Nat) -> IO(Bool): Shrink.u32.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=u32.go) # (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>: Shrink.u32 (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=u32) # 0, n - n/2, n - n/4, ..., n - 1. None for 0. def u32(n: U32) -> List<&1, U32>: Shrink.nat.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=nat.go) def nat.go(f: Nat, stop: Bool, +n: Nat, +d: Nat) -> List<&1, Nat>: Shrink.nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=nat) # 0n, n - n/2, n - n/4, ..., n - 1. None for 0n. def nat(n: Nat) -> List<&1, Nat>: Shrink.list.chunks (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=list.chunks) # 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>>: Shrink.list.dels (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=list.dels) # 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>>: Shrink.list.heads (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=list.heads) def list.heads(-A: Data, cs: List<&1, A>, +t: List<&2, A>) -> List<&1, List<&2, A>>: Shrink.list.cons (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=list.cons) def list.cons(-A: Data, +h: A, rs: List<&1, List<&2, A>>) -> List<&1, List<&2, A>>: Shrink.list.ones (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=list.ones) # 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>>: Shrink.list (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=list) # [], 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>>: Shrink.maybe.some (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=maybe.some) def maybe.some(-A: Data, xs: List<&1, A>) -> List<&1, Maybe<&2, A>>: Shrink.maybe (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=maybe) # 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>>: Shrink.char.lift (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=char.lift) def char.lift(xs: List<&1, U32>, +base: U32) -> List<&1, Char>: Shrink.char.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=char.of) def char.of(o: Cmp, +c: U32) -> List<&1, Char>: Shrink.char (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=char) # Toward 'a': a code above it halves toward it; one below tries 'a', then halves toward 0. def char(c: Char) -> List<&1, Char>: Shrink.string.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=string.of) def string.of(xs: List<&1, List<&2, Char>>) -> List<&1, String>: Shrink.string (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=string) # A String as a list of Chars under char. def string(s: String) -> List<&1, String>: Shrink.bytes.codes (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=bytes.codes) def bytes.codes(s: String) -> List<&2, U32>: Shrink.bytes.chars (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=bytes.chars) def bytes.chars(xs: List<&2, U32>) -> String: Shrink.bytes.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=bytes.of) def bytes.of(xs: List<&1, List<&2, U32>>) -> List<&1, Bytes.Bytes>: Shrink.bytes (https://jend.leeeet.dev/definition.txt?path=bend-kit-property@0.4.0.0/shrink.bend&name=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. def bytes(b: Bytes.Bytes) -> List<&1, Bytes.Bytes>: