0 | module Test.Hedgehog.BoundedDoubles
  1 |
  2 | import Data.Buffer
  3 | import Data.Bounded
  4 | import Data.Double.Bounded
  5 | import Data.Vect
  6 |
  7 | import Hedgehog
  8 |
  9 | %default total
 10 |
 11 | public export
 12 | ClosestToZero : Double
 13 | ClosestToZero = 2.22507e-308
 14 |
 15 | public export
 16 | data Eps = MkEps Double
 17 |
 18 | EPS : Eps => Double
 19 | EPS @{MkEps x} = x
 20 |
 21 | namespace Double
 22 |
 23 |   export
 24 |   eqUpToEps : Eps => Double -> Double -> Bool
 25 |   eqUpToEps x y = abs (x - y) <= EPS
 26 |
 27 | namespace BoundedDouble
 28 |
 29 |   export
 30 |   eqUpToEps : Eps => DoubleBetween l u -> DoubleBetween l u -> Bool
 31 |   eqUpToEps = eqUpToEps `on` (.asDouble)
 32 |
 33 | export
 34 | veryAnyDouble : Gen Double
 35 | veryAnyDouble = unsafePerformIO . doubleFromBits64 <$> bits64 constantBounded
 36 |   where
 37 |     doubleFromBits64 : HasIO io => Bits64 -> io Double
 38 |     doubleFromBits64 n = do
 39 |       Just bf <- newBuffer 8
 40 |         | Nothing => pure $ 0.0/0
 41 |       setBits64 bf 0 n
 42 |       getDouble bf 0
 43 |
 44 | export
 45 | anySolidDouble : Gen SolidDouble
 46 | anySolidDouble = veryAnyDouble >>= \x => case (decSo $ NegInf <= x, decSo $ x <= PosInf) of
 47 |   (Yes lp, Yes rp) => pure $ BoundedDouble x
 48 |   _                => element [0, ClosestToZero, MinDouble, MaxDouble, NegInf, PosInf] <&> \x => BoundedDouble x @{believe_me Oh} @{believe_me Oh}
 49 |
 50 | export
 51 | boundedDoubleCorrect : {l, u : _} -> DoubleBetween l u -> PropertyT ()
 52 | boundedDoubleCorrect x = do
 53 |   annotate "\{show l} <= \{show x} <= \{show u}"
 54 |   assert $ l <= x.asDouble && x.asDouble <= u
 55 |
 56 | export
 57 | numericDouble : (canNegInf, canPosInf : Bool) -> Gen Double
 58 | numericDouble canNegInf canPosInf = map purify $ double $ exponentialDoubleFrom 0 MinDouble MaxDouble
 59 |   where
 60 |     purify : Double -> Double
 61 |     purify x = if not canPosInf && x == PosInf
 62 |                || not canNegInf && x == NegInf
 63 |                || not (x == x)
 64 |                then 0 else x
 65 |
 66 | export
 67 | nonNegativeDouble : (canPosInf : Bool) -> Gen Double
 68 | nonNegativeDouble canPosInf = md <$> numericDouble canPosInf canPosInf
 69 |   where
 70 |     md : Double -> Double
 71 |     md x = if x < 0 then negate x else x
 72 |
 73 | export
 74 | anyBoundedDouble : (l, u : Double) -> (0 _ : So $ l <= u) => Gen $ DoubleBetween l u
 75 | anyBoundedDouble l u = do
 76 |   let inBounds : Double -> Bool
 77 |       inBounds x = l <= x && x <= u
 78 |   let ifInBounds : Double -> Maybe Double
 79 |       ifInBounds x = if inBounds x then Just x else Nothing
 80 |   let basic : Gen Double
 81 |       basic = element $ reorder $ l :: u :: fromList (mapMaybe ifInBounds [0, ClosestToZero, MinDouble, MaxDouble, NegInf, PosInf])
 82 |   x <- choice
 83 |          [ basic
 84 |          , double (exponentialDouble (l `max` MinDouble) (u `min` MaxDouble)) >>= \x =>
 85 |              if inBounds x then pure x else basic
 86 |          ]
 87 |   pure $ BoundedDouble x @{believe_me Oh} @{believe_me Oh}
 88 |   where
 89 |     reorder : forall k, a. Vect (S k) a -> Vect (S k) a
 90 |     reorder $ a::b::c::rest = c::a::b::rest
 91 |     reorder xs              = xs
 92 |
 93 | export
 94 | someBoundedDouble : Gen (l ** u ** DoubleBetween l u)
 95 | someBoundedDouble = do
 96 |   l <- numericDouble True True
 97 |   u <- numericDouble True True
 98 |   let (l, u) = (min l u, max l u)
 99 |   x <- anyBoundedDouble l u @{believe_me Oh}
100 |   pure (l ** u ** x)
101 |
102 | --- Special common properties ---
103 |
104 | export
105 | un_corr : {l, u, l', u' : _} -> (0 _ : So $ l <= u) => (DoubleBetween l u -> DoubleBetween l' u') -> Property
106 | un_corr f = property $ do
107 |   x <- forAll $ anyBoundedDouble _ _
108 |   boundedDoubleCorrect $ f x
109 |