
   0 | module Hedgehog.Internal.Shrink
   1 | 
   2 | import Data.Colist
   3 | import Data.Cotree
   4 | import Data.Nat
   5 | 
   6 | import Hedgehog.Internal.Util
   7 | 
   8 | %default total
   9 | 
  10 | public export
  11 | halvesInteger : Integer -> Colist Integer
  12 | halvesInteger = iterateBefore0 (`safeDiv` 2)
  13 | 
  14 | public export
  15 | halves : ToInteger a => a -> Colist a
  16 | halves = map fromInteger . halvesInteger . toInteger
  17 | 
  18 | public export
  19 | towardsInteger : (destination, val : Integer) -> Colist Integer
  20 | towardsInteger dest x =
  21 |   if dest == x
  22 |      then []
  23 |      else
  24 |        let diff := (x `safeDiv` 2) - (dest `safeDiv` 2)
  25 |         in dest `consNub` map (x -) (halvesInteger diff)
  26 | 
  27 | ||| Shrink an integral number by edging towards a destination.
  28 | |||
  29 | ||| >>> towards 0 100
  30 | ||| [0,50,75,88,94,97,99]
  31 | |||
  32 | ||| >>> towards 500 1000
  33 | ||| [500,750,875,938,969,985,993,997,999]
  34 | |||
  35 | ||| >>> towards (-50) (-26)
  36 | ||| [-50,-38,-32,-29,-27]
  37 | |||
  38 | ||| Note we always try the destination first, as that is the optimal shrink.
  39 | public export
  40 | towards : ToInteger a => (destination, val : a) -> Colist a
  41 | towards dest x =
  42 |   map
  43 |     fromInteger
  44 |     (towardsInteger (toInteger dest) (toInteger x))
  45 | 
  46 | public export
  47 | towardsDouble : Double -> Double -> Colist Double
  48 | towardsDouble destination x =
  49 |   if destination == x
  50 |     then []
  51 |     else
  52 |       let diff := x - destination
  53 |           ok   := (/= x)
  54 |        in takeWhile ok .  map (x -) $ iterate (/ 2) diff
  55 | 
  56 | public export
  57 | removes : Nat -> List a -> Colist $ List a
  58 | removes 0     _ = []
  59 | removes (S n) x = run (S n) [] x
  60 | 
  61 |   where
  62 |     run : Nat -> List a -> List a -> Colist $ List a
  63 |     run 0     _   []       = [[]]
  64 |     run 0     xs (y :: ys) =
  65 |       let rest := run n [y] ys
  66 |        in (y :: ys) :: map (prepRev xs) rest
  67 |     run (S k) _  []        = []
  68 |     run (S k) xs (y :: ys) = run k (y :: xs) ys
  69 | 
  70 | ||| All ways a list can be split
  71 | |||
  72 | ||| Note: The first list in the triple will be in reverse order
  73 | public export
  74 | splits : (a -> b) -> List a -> List (List a, b, List a)
  75 | splits _ []        = []
  76 | splits f (x :: xs) = run [] x xs
  77 | 
  78 |   where
  79 |     run : List a -> a -> List a -> List (List a, b, List a)
  80 |     run xs x []          = [(xs,f x,[])]
  81 |     run xs x l@(y :: ys) = (xs,f x,l) :: run (x::xs) y ys
  82 | 
  83 | ||| Shrink a list by edging towards the empty list.
  84 | |||
  85 | ||| >>> list [1,2,3]
  86 | ||| [[],[2,3],[1,3],[1,2]]
  87 | |||
  88 | ||| >>> list "abcd"
  89 | ||| ["","cd","ab","bcd","acd","abd","abc"]
  90 | |||
  91 | ||| Note we always try the empty list first, as that is the optimal shrink.
  92 | public export
  93 | list : (minLength : Nat) -> List a -> Colist $ List a
  94 | list ml xs = let diff = length xs `minus` ml
  95 |               in concatMapColist (`removes` xs) (halves diff)
  96 | 
  97 | public export
  98 | interleave : (minLength : Nat) -> List (Cotree a) -> Cotree (List a)
  99 | interleave ml ts = MkCotree (map value ts) $ dropThenShrink (list ml ts)
 100 | 
 101 |   where
 102 |     shrinkOne :
 103 |          List (List (Cotree a), Coforest a, List (Cotree a))
 104 |       -> Coforest (List a)
 105 |     shrinkOne []                      = []
 106 |     shrinkOne ((xs,[]   ,ys) :: rest) = shrinkOne rest
 107 |     shrinkOne ((xs,t::ts,ys) :: rest) =
 108 |       interleave ml (prepRev xs (t::ys)) :: shrinkOne ((xs,ts,ys) :: rest)
 109 | 
 110 |     dropThenShrink : Colist (List $ Cotree a) -> Coforest (List a)
 111 |     dropThenShrink []        = shrinkOne (splits (\t => t.forest) ts)
 112 |     dropThenShrink (x :: xs) = interleave ml x :: dropThenShrink xs
 113 | 
 114 | --------------------------------------------------------------------------------
 115 | --          Tests
 116 | --------------------------------------------------------------------------------
 117 | 
 118 | HalvesFrom10 : List Int
 119 | HalvesFrom10 = take 10 $ halves 10
 120 | 
 121 | halvesFrom10Test : HalvesFrom10 = [10,5,2,1]
 122 | halvesFrom10Test = Refl
 123 | 
 124 | Towards0_100 : List Int
 125 | Towards0_100 = take 10 $ towards 0 100
 126 | 
 127 | Towards500_1000 : List Int
 128 | Towards500_1000 = take 10 $ towards 500 1000
 129 | 
 130 | Towards50_26 : List Int
 131 | Towards50_26 = take 10 $ towards (-50) (-26)
 132 | 
 133 | towards0_100Test : Towards0_100 = [0,50,75,88,94,97,99]
 134 | towards0_100Test = Refl
 135 | 
 136 | towards500_1000Test : Towards500_1000 = [500,750,875,938,969,985,993,997,999]
 137 | towards500_1000Test = Refl
 138 | 
 139 | towards50_26Test : Towards50_26 = [-50,-38,-32,-29,-27]
 140 | towards50_26Test = Refl
 141 | 
 142 | TowardsFloat0_100 : List Double
 143 | TowardsFloat0_100 = take 7 $ towardsDouble 0.0 100
 144 | 
 145 | TowardsFloat1_5 : List Double
 146 | TowardsFloat1_5 = take 7 $ towardsDouble 1 0.5
 147 | 
 148 | towardsFloat0_100Test : TowardsFloat0_100 = [0.0,50.0,75.0,87.5,93.75,96.875,98.4375]
 149 | towardsFloat0_100Test = Refl
 150 | 
 151 | towardsFloat1_5Test : TowardsFloat1_5 = [1.0,0.75,0.625,0.5625,0.53125,0.515625,0.5078125]
 152 | towardsFloat1_5Test = Refl
 153 | 
 154 | Removes2_2 : List $ List Int
 155 | Removes2_2 = take 10 $ removes 2 [1,2]
 156 | 
 157 | removes2_2Test : Removes2_2 = [[]]
 158 | removes2_2Test = Refl
 159 | 
 160 | Removes2_3 : List $ List Int
 161 | Removes2_3 = take 10 $ removes 2 [1,2,3]
 162 | 
 163 | removes2_3Test : Removes2_3 = [[3]]
 164 | removes2_3Test = Refl
 165 | 
 166 | Removes2_4 : List $ List Int
 167 | Removes2_4 = take 10 $ removes 2 [1,2,3,4]
 168 | 
 169 | removes2_4Test : Removes2_4 = [[3,4],[1,2]]
 170 | removes2_4Test = Refl
 171 | 
 172 | Removes2_5 : List $ List Int
 173 | Removes2_5 = take 10 $ removes 2 [1,2,3,4,5]
 174 | 
 175 | removes2_5Test : Removes2_5 = [[3,4,5],[1,2,5]]
 176 | removes2_5Test = Refl
 177 | 
 178 | Removes2_6 : List $ List Int
 179 | Removes2_6 = take 10 $ removes 2 [1,2,3,4,5,6]
 180 | 
 181 | removes2_6Test : Removes2_6 = [[3,4,5,6],[1,2,5,6],[1,2,3,4]]
 182 | removes2_6Test = Refl
 183 | 
 184 | Removes3_10 : List $ List Int
 185 | Removes3_10 = take 10 $ removes 3 [1,2,3,4,5,6,7,8,9,10]
 186 | 
 187 | removes3_10Test : Removes3_10 = [[4,5,6,7,8,9,10],[1,2,3,7,8,9,10],[1,2,3,4,5,6,10]]
 188 | removes3_10Test = Refl
 189 | 
 190 | List3 : List $ List Int
 191 | List3 = take 10 $ list 0 [1,2,3]
 192 | 
 193 | List4 : List $ List Int
 194 | List4 = take 10 $ list 0 [1,2,3,4]
 195 | 
 196 | List5 : List $ List Int
 197 | List5 = take 10 $ list 2 [1,2,3,4,5]
 198 | 
 199 | list3Test : List3 = [[],[2,3],[1,3],[1,2]]
 200 | list3Test = Refl
 201 | 
 202 | list4Test : List4 = [[],[3,4],[1,2],[2,3,4],[1,3,4],[1,2,4],[1,2,3]]
 203 | list4Test = Refl
 204 | 
 205 | list5Test : List5 = [[4,5],[2,3,4,5],[1,3,4,5],[1,2,4,5],[1,2,3,5],[1,2,3,4]]
 206 | list5Test = Refl
 207 |