-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathgen.ml
286 lines (241 loc) · 7.79 KB
/
gen.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
module Trace_buf = struct
type trace_pick =
| Bool of bool
| Int of {
value : int;
shrink : int;
}
type t = trace_pick Dynarray.t
let create = Dynarray.create
let copy = Dynarray.copy
let reset = Dynarray.clear
let bits trace_buf =
let rand = Buffer.create 0 in
Dynarray.iter
(function
| Bool value -> Buffer.add_uint8 rand (Bool.to_int value)
| Int pick -> Buffer.add_int64_ne rand (Int64.of_int pick.value))
trace_buf;
Buffer.contents rand
let add_bool trace_buf value = Dynarray.add_last trace_buf (Bool value)
let add_int trace_buf value ~shrink =
Dynarray.add_last trace_buf (Int { value; shrink })
end
exception Bad_input
module Input = struct
type t =
| Random of Random.State.t
| Bits of {
rand : string;
mutable pos : int;
}
let bool = function
| Random rng -> Random.State.bool rng
| Bits repro ->
if not (repro.pos < String.length repro.rand) then
raise_notrace Bad_input;
let p = repro.rand.[repro.pos] <> '\x00' in
repro.pos <- repro.pos + 1;
p
let get_int rand pos =
if not (pos + 8 <= String.length rand) then raise_notrace Bad_input;
Int64.to_int (String.get_int64_ne rand pos)
let full_int input bound =
match input with
| Random rng -> Random.State.full_int rng bound
| Bits repro ->
let n = get_int repro.rand repro.pos in
if not (0 <= n && n < bound) then raise_notrace Bad_input;
repro.pos <- repro.pos + 8;
n
let int_in_range input ~min ~max =
match input with
| Random rng -> Random.State.int_in_range rng ~min ~max
| Bits repro ->
let n = get_int repro.rand repro.pos in
if not (min <= n && n <= max) then raise_notrace Bad_input;
repro.pos <- repro.pos + 8;
n
end
type ('sample, 'a) t = {
forward : Trace_buf.t -> Input.t -> 'a;
backward : Trace_buf.t -> 'sample -> 'a;
}
type 'a simple = ('a, 'a) t
let exact x (equal : 'a -> 'a -> bool) =
let backward _trace sample =
if not (equal sample x) then raise_notrace Bad_input;
x
in
{ forward = (fun _ _ -> x); backward }
let create_forwarded () =
let gen_ref =
let f _ _ = invalid_arg "generator not implemented" in
ref { forward = f; backward = f }
in
let forward trace_buf input = !gen_ref.forward trace_buf input in
let backward trace_buf sample = !gen_ref.backward trace_buf sample in
({ forward; backward }, gen_ref)
let bool =
let forward trace_buf input =
let value = Input.bool input in
Trace_buf.add_bool trace_buf value;
value
in
let backward trace_buf sample =
Trace_buf.add_bool trace_buf sample;
sample
in
{ forward; backward }
let full_int ?shrink strictness bound =
if not (0 < bound) then invalid_arg "expected 0 < bound";
let shrink = Option.value shrink ~default:0 in
if not (0 <= shrink && shrink < bound) then
invalid_arg "expected 0 <= shrink < bound";
let forward trace_buf input =
let value = Input.full_int input bound in
Trace_buf.add_int trace_buf value ~shrink;
value
in
let backward =
let non_strict trace_buf sample =
Trace_buf.add_int trace_buf sample ~shrink;
sample
in
let strict trace_buf sample =
if not (0 <= sample && sample < bound) then raise_notrace Bad_input;
non_strict trace_buf sample
in
match strictness with `Non_strict -> non_strict | `Strict -> strict
in
{ forward; backward }
let int_in_range ?shrink strictness ~min ~max =
if not (min < max) then invalid_arg "expected min < max";
let shrink = Option.value shrink ~default:min in
if not (min <= shrink && shrink <= max) then
invalid_arg "expected min <= shrink <= max";
let forward trace_buf input =
let value = Input.int_in_range input ~min ~max in
Trace_buf.add_int trace_buf value ~shrink;
value
in
let backward =
let non_strict trace_buf sample =
Trace_buf.add_int trace_buf sample ~shrink;
sample
in
let strict trace_buf sample =
if not (min <= sample && sample <= max) then raise_notrace Bad_input;
non_strict trace_buf sample
in
match strictness with `Non_strict -> non_strict | `Strict -> strict
in
{ forward; backward }
let small_int = int_in_range `Non_strict ~min:0 ~max:99
let filter_map mapping gen =
let forward trace_buf input =
match mapping (gen.forward trace_buf input) with
| Some x -> x
| None -> raise_notrace Bad_input
in
let backward trace_buf sample =
match mapping (gen.backward trace_buf sample) with
| Some x -> x
| None -> raise_notrace Bad_input
in
{ forward; backward }
let map mapping gen =
let forward trace_buf input = mapping (gen.forward trace_buf input) in
let backward trace_buf sample = mapping (gen.backward trace_buf sample) in
{ forward; backward }
let bind binder gen =
let forward trace_buf input =
let x = gen.forward trace_buf input in
(binder x).forward trace_buf input
in
let backward trace_buf sample =
let x = gen.backward trace_buf sample in
(binder x).backward trace_buf sample
in
{ forward; backward }
let choose cases =
let cases = Array.of_list cases in
let index_gen = full_int `Strict (Array.length cases) in
let forward trace_buf input =
let i = index_gen.forward trace_buf input in
cases.(i).forward trace_buf input
in
let rec backward i trace_buf sample =
let checkpoint = Dynarray.length trace_buf in
ignore (index_gen.backward trace_buf i);
try cases.(i).backward trace_buf sample
with Bad_input ->
Dynarray.truncate trace_buf checkpoint;
backward (i + 1) trace_buf sample
in
{ forward; backward = backward 0 }
module Syntax = struct
let ( let+ ) gen mapping = map mapping gen
let ( let* ) gen binder = bind binder gen
end
let try_focus mapping gen =
let backward trace_buf sample =
match mapping sample with
| None -> raise_notrace Bad_input
| Some x -> gen.backward trace_buf x
in
{ gen with backward }
let focus mapping gen =
let backward trace_buf sample = gen.backward trace_buf (mapping sample) in
{ gen with backward }
let option elem_gen =
let is_some_gen = bool in
let forward trace_buf input =
if is_some_gen.forward trace_buf input then
Some (elem_gen.forward trace_buf input)
else None
in
let backward trace_buf sample =
ignore (is_some_gen.backward trace_buf (Option.is_some sample));
Option.map (elem_gen.backward trace_buf) sample
in
{ forward; backward }
let result ~ok:ok_gen ~error:error_gen =
let is_ok_gen = bool in
let forward trace_buf input =
if is_ok_gen.forward trace_buf input then
Ok (ok_gen.forward trace_buf input)
else Error (error_gen.forward trace_buf input)
in
let backward trace_buf sample =
ignore (is_ok_gen.backward trace_buf (Result.is_ok sample));
match sample with
| Ok ok -> Ok (ok_gen.backward trace_buf ok)
| Error error -> Error (error_gen.backward trace_buf error)
in
{ forward; backward }
let list len_gen elem_gen =
let forward trace_buf input =
let len = len_gen.forward trace_buf input in
List.init len (fun _ -> elem_gen.forward trace_buf input)
in
let backward trace_buf sample =
ignore (len_gen.backward trace_buf (List.length sample));
List.map (elem_gen.backward trace_buf) sample
in
{ forward; backward }
let generate_from_rng rng gen ~trace_buf =
Trace_buf.reset trace_buf;
match gen.forward trace_buf (Random rng) with
| x -> Some x
| exception Bad_input -> None
let generate_from_bits rand gen ~trace_buf =
Trace_buf.reset trace_buf;
match gen.forward trace_buf (Bits { rand; pos = 0 }) with
| x -> Some x
| exception Bad_input -> None
let retrace sample gen ~trace_buf =
Trace_buf.reset trace_buf;
match gen.backward trace_buf sample with
| x -> Some x
| exception Bad_input -> None