Source file shrink.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
(*---------------------------------------------------------------------------
   Copyright (c) 2013-2017 Guillaume Bury, Simon Cruanes, Vincent Hugot,
                           Jan Midtgaard
   Copyright (c) 2026 Invariant Systems. All rights reserved.
   SPDX-License-Identifier: BSD-2-Clause

   Shrinking algorithms derived from QCheck2
   (https://github.com/c-cube/qcheck).
  ---------------------------------------------------------------------------*)

(* Binary search shrinking: halve the distance between current candidate and
   destination at each step, producing a sequence that converges on the target. *)

let int_towards dest x () =
  Seq.unfold
    (fun current ->
      if current = x then None
      else
        (* Halve each operand before subtracting to avoid overflow.
           Naive (x - current) / 2 would overflow for int_towards min_int max_int. *)
        let half_diff = (x / 2) - (current / 2) in
        if half_diff = 0 then
          (* current is adjacent to x; emit it, then use x as sentinel to stop *)
          Some (current, x)
        else Some (current, current + half_diff))
    dest ()

let int32_towards dest x () =
  Seq.unfold
    (fun current ->
      if Int32.equal current x then None
      else
        let half_diff = Int32.sub (Int32.div x 2l) (Int32.div current 2l) in
        if Int32.equal half_diff 0l then Some (current, x)
        else Some (current, Int32.add current half_diff))
    dest ()

let int64_towards dest x () =
  Seq.unfold
    (fun current ->
      if Int64.equal current x then None
      else
        let half_diff = Int64.sub (Int64.div x 2L) (Int64.div current 2L) in
        if Int64.equal half_diff 0L then Some (current, x)
        else Some (current, Int64.add current half_diff))
    dest ()

(* Float halving can produce infinitely many distinct values without reaching
   the target, so we cap at 15 iterations to keep shrinking bounded. *)
let nativeint_towards dest x () =
  Seq.unfold
    (fun current ->
      if Nativeint.equal current x then None
      else
        let half_diff =
          Nativeint.sub (Nativeint.div x 2n) (Nativeint.div current 2n)
        in
        if Nativeint.equal half_diff 0n then Some (current, x)
        else Some (current, Nativeint.add current half_diff))
    dest ()

let float_towards dest x () =
  Seq.take 15
    (Seq.unfold
       (fun current ->
         if Float.equal current x then None
         else
           let half_diff = (x /. 2.0) -. (current /. 2.0) in
           if Float.equal half_diff 0.0 then Some (current, x)
           else Some (current, current +. half_diff))
       dest)
    ()