0 | module Hedgehog.Internal.Range

  2 | import Data.Bounded

  3 | import Data.Fin

  4 | import Data.Maybe

  5 | import Decidable.Equality

  6 | import Derive.Prelude

  7 | import Derive.Pretty

  9 | import Hedgehog.Internal.Util

 11 | %hide Prelude.Range

 13 | %language ElabReflection

 14 | %default total

 16 | public export

 17 | MaxSizeNat : Nat

 18 | MaxSizeNat = 100

 25 | public export

 26 | record Size where

 27 |   constructor MkSize

 28 |   size     : Nat

 29 |   0 sizeOk : size <= MaxSizeNat = True

 31 | %runElab derive "Size" [Show,Eq,Ord]

 34 | Pretty Size where

 35 |   prettyPrec _ (MkSize n _) = line $ show n

 37 | public export

 38 | mkSize : (n : Nat) -> {auto 0 ok : n <= MaxSizeNat = True} -> Size

 39 | mkSize n = MkSize n ok

 41 | public export

 42 | minSize : Size

 43 | minSize = mkSize 0

 45 | public export

 46 | maxSize : Size

 47 | maxSize = mkSize MaxSizeNat

 50 | mkSizeMay : Nat -> Maybe Size

 51 | mkSizeMay n with (decEq (n <= MaxSizeNat) True)

 52 |   mkSizeMay n | Yes _ = Just $ mkSize n

 53 |   mkSizeMay n | No  c = Nothing

 56 | mkSizeOrZero : Nat -> Size

 57 | mkSizeOrZero = fromMaybe minSize . mkSizeMay

 60 | mkSizeOrMax : Nat -> Size

 61 | mkSizeOrMax = fromMaybe maxSize . mkSizeMay

 63 | public export

 64 | resize : (Nat -> Nat) -> Size -> Size

 65 | resize f s = mkSizeOrMax (f s.size)

 72 | MinBound Size where

 73 |   minBound = minSize

 76 | MaxBound Size where

 77 |   maxBound = maxSize

 80 | Num Size where

 81 |   a + b = mkSizeOrMax $ size a + size b

 82 |   a * b = mkSizeOrMax $ size a * size b

 83 |   fromInteger = mkSizeOrMax . fromInteger

 85 | public export

 86 | ToInteger Size where toInteger = toInteger . size

 92 | public export

 93 | record Range a where

 94 |   constructor MkRange

 95 |   origin  : a

 96 |   bounds' : Size -> (a,a)

 99 | bounds : Size -> Range a -> (a,a)

100 | bounds s r = r.bounds' s

104 | lowerBound : Ord a => Size -> Range a -> a

105 | lowerBound sz = uncurry min . bounds sz

109 | upperBound : Ord a => Size -> Range a -> a

110 | upperBound sz = uncurry max . bounds sz

113 | Functor Range where

114 |   map f (MkRange origin bounds') =

115 |     MkRange

116 |       (f origin)

117 |       (\si => let (x,y) := bounds' si in (f x, f y))

131 | singleton : a -> Range a

132 | singleton x = MkRange x $ \_ => (x, x)

153 | constantFrom : (origin,lower,upper : a) -> Range a

154 | constantFrom o l u = MkRange o $ \_ => (l, u)

167 | constant : a -> a -> Range a

168 | constant x y = constantFrom x x y

181 | constantBounded : (MinBound a, MaxBound a) => Num a => Range a

182 | constantBounded = constantFrom 0 minBound maxBound

196 | clamp : Ord a => (lower,upper,val : a) -> a

197 | clamp l u v =

198 |   if l > u

199 |      then min l (max u v)

200 |      else min u (max l v)

204 | scaleLinear : ToInteger a => Size -> (origin,bound : a) -> a

205 | scaleLinear sz o0 b0 =

206 |   let o    := toInteger o0

207 |       b    := toInteger b0

208 |       rng  := b - o

209 |       diff := (rng * toInteger sz) `safeDiv` 100

210 |    in fromInteger $ o + diff

214 | scaleLinearFrac : Fractional a => Neg a => Size -> (origin,bound : a) -> a

215 | scaleLinearFrac sz o b =

216 |   let diff = (b - o) * (fromIntegral sz / 100)

217 |    in o + diff

219 | export %inline

220 | scaled :

221 |      {auto _ : Ord a}

222 |   -> (scale : Size -> (origin,bound : a) -> a)

223 |   -> (origin,lower,upper : a)

224 |   -> Range a

225 | scaled f o l u =

226 |   MkRange o $ \sz =>

227 |     let x_sized := clamp l u $ f sz o l

228 |         y_sized := clamp l u $ f sz o u

229 |      in (x_sized, y_sized)

242 | linearFrom : Ord a => ToInteger a => (origin,lower,upper : a) -> Range a

243 | linearFrom = scaled scaleLinear

246 | linear : Ord a => ToInteger a => (origin,upper : a) -> Range a

247 | linear origin upper = linearFrom origin origin upper

250 | linearFin : (n : Nat) -> Range (Fin $ S n)

251 | linearFin n = map toFin $ linearFrom 0 0 (natToInteger n)

253 |   where

254 |     toFin : Integer -> Fin (S n)

255 |     toFin k = fromMaybe FZ (integerToFin k (S n))

261 | linearFracFrom :

262 |      {auto _ : Ord a}

263 |   -> {auto _ : Fractional a}

264 |   -> {auto _ : Neg a}

265 |   -> (origin,lower,uppder : a) -> Range a

266 | linearFracFrom = scaled scaleLinearFrac

280 | linearBounded :  (MinBound a, MaxBound a) => Ord a => ToInteger a => Range a

281 | linearBounded = linearFrom minBound minBound maxBound

287 | EulerMinus1 : Double

288 | EulerMinus1 = euler - 1

294 | scaleExponentialDouble : Size -> (origin,bound : Double) -> Double

295 | scaleExponentialDouble sz o b =

296 |   let e     := fromIntegral sz / 100.0

297 |       delta := b - o

298 |       diff  := pow (abs delta + 1) e - 1

299 |    in o + diff * signum delta

303 | scaleExponential : ToInteger a => Size -> (origin,bound : a) -> a

304 | scaleExponential sz o b =

305 |   round (scaleExponentialDouble sz (fromIntegral o) (fromIntegral b))

308 | exponentialDoubleFrom : (origin,lower,upper : Double) -> Range Double

309 | exponentialDoubleFrom = scaled scaleExponentialDouble

312 | exponentialDouble : (lower,upper : Double) -> Range Double

313 | exponentialDouble l u = exponentialDoubleFrom l l u

316 | exponentialFrom : Ord a => ToInteger a => (origin,lower,upper : a) -> Range a

317 | exponentialFrom = scaled scaleExponential

320 | exponential : Ord a => ToInteger a => (lower,upper : a) -> Range a

321 | exponential l u = exponentialFrom l l u

324 | exponentialFin : (n : Nat) -> Range (Fin $ S n)

325 | exponentialFin n = map toFin $ exponentialFrom 0 0 (natToInteger n)

327 |   where

328 |     toFin : Integer -> Fin (S n)

329 |     toFin k = fromMaybe FZ (integerToFin k (S n))

335 | singletonOriginId : origin (singleton x) = x

336 | singletonOriginId = Refl

338 | singletonBoundsId : bounds s (singleton x) = (x,x)

339 | singletonBoundsId = Refl

341 | constantFromOrigin : origin (constantFrom o l u) = o

342 | constantFromOrigin = Refl

344 | constantFromBounds : bounds s (constantFrom o l u) = (l,u)

345 | constantFromBounds = Refl

347 | constantOrigin : origin (constant o u) = o

348 | constantOrigin = Refl

350 | constantBounds : bounds s (constant o u) = (o,u)

351 | constantBounds = Refl

353 | One : Int

354 | One = 1

356 | Zero : Int

357 | Zero = 0

359 | clamp1_100_0 : clamp One 100 0 = One

360 | clamp1_100_0 = Refl

362 | clamp100_1_0 : clamp 100 One 0 = One

363 | clamp100_1_0 = Refl

365 | clamp1_100_150 : clamp One 100 150 = 100

366 | clamp1_100_150 = Refl

368 | clamp100_1_150 : clamp 100 One 150 = 100

369 | clamp100_1_150 = Refl

371 | clamp1_100_50 : clamp One 100 50 = 50

372 | clamp1_100_50 = Refl

374 | clamp100_1_50 : clamp 100 One 50 = 50

375 | clamp100_1_50 = Refl