generate.bend
bend-kit-property@0.4.0.0 · 169 lines · 32 definitions
1
2import Base
3import bend-kit-random@0.1.0.1/random.bend as Rand
4import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
5
6
7
8
9
10
11def cap(+n: U32) -> U32:
12 U32.min(n, 1024)
13
14
15def u32(r: Rand.Rng) -> U32 & Rand.Rng:
16 Rand.next(r)
17
18
19def u32.range(+lo: U32, hi: U32, r: Rand.Rng) -> U32 & Rand.Rng:
20 Rand.range(lo, hi, r)
21
22
23def size(+max: U32, r: Rand.Rng) -> U32 & Rand.Rng:
24 Rand.below((cap(max) + 1 : U32), r)
25
26def nat.fin(xr: U32 & Rand.Rng) -> Nat & Rand.Rng:
27 (x, r) = xr
28 (U32.to_nat(x), r)
29
30
31def nat(+max: U32, r: Rand.Rng) -> Nat & Rand.Rng:
32 nat.fin(size(max, r))
33
34def char.fin(xr: U32 & Rand.Rng) -> Char & Rand.Rng:
35 (x, r) = xr
36 (Chr{x}, r)
37
38
39def char(r: Rand.Rng) -> Char & Rand.Rng:
40 char.fin(Rand.range(32, 127, r))
41
42
43def string.go(n: Nat, acc: String, cr: Char & Rand.Rng) -> String & Rand.Rng:
44 match n:
45 case 0n:
46 (c, r) = cr
47 (SCon{c, acc}, r)
48 case 1n+p:
49 (c, r) = cr
50 string.go(p, SCon{c, acc}, char(r))
51
52
53def string.of(n: Nat, r: Rand.Rng) -> String & Rand.Rng:
54 match n:
55 case 0n:
56 (SNil{}, r)
57 case 1n+p:
58 string.go(p, SNil{}, char(r))
59
60def string.fin(nr: Nat & Rand.Rng) -> String & Rand.Rng:
61 (n, r) = nr
62 string.of(n, r)
63
64
65def string(+max: U32, r: Rand.Rng) -> String & Rand.Rng:
66 string.fin(nat(max, r))
67
68
69def bytes.go(n: Nat, b: Bytes.Bytes, +i: U32, xr: U32 & Rand.Rng) -> Bytes.Bytes & Rand.Rng:
70 match n:
71 case 0n:
72 (x, r) = xr
73 (Bytes.set(b, i, x), r)
74 case 1n+p:
75 (x, r) = xr
76 bytes.go(p, Bytes.set(b, i, x), (i + 1 : U32), Rand.next(r))
77
78def bytes.start(n: Nat, +len: U32, r: Rand.Rng) -> Bytes.Bytes & Rand.Rng:
79 match n:
80 case 0n:
81 (Bytes.new(0), r)
82 case 1n+p:
83 bytes.go(p, Bytes.new(len), 0, Rand.next(r))
84
85
86def bytes.of(+len: U32, r: Rand.Rng) -> Bytes.Bytes & Rand.Rng:
87 +n = cap(len)
88 bytes.start(U32.to_nat(n), n, r)
89
90def bytes.fin(nr: U32 & Rand.Rng) -> Bytes.Bytes & Rand.Rng:
91 (n, r) = nr
92 bytes.of(n, r)
93
94
95def bytes(+max: U32, r: Rand.Rng) -> Bytes.Bytes & Rand.Rng:
96 bytes.fin(size(max, r))
97
98
99def 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:
100 match n:
101 case 0n:
102 (h, r) = hr
103 (h <> acc, r)
104 case 1n+p:
105 (h, r) = hr
106 list.go(~T, ~gen, p, h <> acc, gen(r))
107
108
109def list.of(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, n: Nat, r: Rand.Rng) -> List<&2, T> & Rand.Rng:
110 match n:
111 case 0n:
112 (Nil{}, r)
113 case 1n+p:
114 list.go(~T, ~gen, p, Nil{}, gen(r))
115
116def list.fin(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, nr: Nat & Rand.Rng) -> List<&2, T> & Rand.Rng:
117 (n, r) = nr
118 list.of(~T, ~gen, n, r)
119
120
121def list(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, +max: U32, r: Rand.Rng) -> List<&2, T> & Rand.Rng:
122 list.fin(~T, ~gen, nat(max, r))
123
124def maybe.some(~T: Data, hr: T & Rand.Rng) -> Maybe<&2, T> & Rand.Rng:
125 (h, r) = hr
126 (Some{h}, r)
127
128def maybe.if(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, none: Bool, r: Rand.Rng) -> Maybe<&2, T> & Rand.Rng:
129 match none:
130 case True{}:
131 (None{}, r)
132 case False{}:
133 maybe.some(~T, gen(r))
134
135def maybe.pick(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, xr: U32 & Rand.Rng) -> Maybe<&2, T> & Rand.Rng:
136 (+x, r) = xr
137 maybe.if(~T, ~gen, U32.is_eq(x, 0), r)
138
139
140def maybe(~T: Data, ~gen: Rand.Rng -> T & Rand.Rng, r: Rand.Rng) -> Maybe<&2, T> & Rand.Rng:
141 maybe.pick(~T, ~gen, Rand.below(4, r))
142
143def map.fin(~A: Type, ~B: Type, ~f: A -> B, ar: A & Rand.Rng) -> B & Rand.Rng:
144 (a, r) = ar
145 (f(a), r)
146
147
148def map(~A: Type, ~B: Type, ~f: A -> B, ~gen: Rand.Rng -> A & Rand.Rng, r: Rand.Rng) -> B & Rand.Rng:
149 map.fin(~A, ~B, ~f, gen(r))
150
151def bind.fin(~A: Type, ~B: Type, ~k: A -> Rand.Rng -> B & Rand.Rng, ar: A & Rand.Rng) -> B & Rand.Rng:
152 (a, r) = ar
153 k(a, r)
154
155
156def bind(~A: Type, ~B: Type, ~gen: Rand.Rng -> A & Rand.Rng, ~k: A -> Rand.Rng -> B & Rand.Rng, r: Rand.Rng) -> B & Rand.Rng:
157 bind.fin(~A, ~B, ~k, gen(r))
158
159def pair.snd(~A: Type, ~B: Type, a: A, br: B & Rand.Rng) -> (A & B) & Rand.Rng:
160 (b, r) = br
161 ((a, b), r)
162
163def pair.fst(~A: Type, ~B: Type, ~gb: Rand.Rng -> B & Rand.Rng, ar: A & Rand.Rng) -> (A & B) & Rand.Rng:
164 (a, r) = ar
165 pair.snd(~A, ~B, a, gb(r))
166
167
168def pair(~A: Type, ~B: Type, ~ga: Rand.Rng -> A & Rand.Rng, ~gb: Rand.Rng -> B & Rand.Rng, r: Rand.Rng) -> (A & B) & Rand.Rng:
169 pair.fst(~A, ~B, ~gb, ga(r))