0 | module Geom.Scale
 1 |
 2 | import Derive.Prelude
 3 | import Derive.Refined
 4 |
 5 | %language ElabReflection
 6 | %default total
 7 |
 8 | ||| Scaling factor in the range [1.0e-6,1.0e6].
 9 | public export
10 | ValidScale : Double -> Bool
11 | ValidScale x = 1.0e-6 <= x && x <= 1.0e6
12 |
13 | ||| A scaling factor
14 | public export
15 | record Scale where
16 |   constructor S
17 |   value       : Double
18 |   {auto 0 prf : Holds ValidScale value}
19 |
20 | %runElab derive "Scale" [Show,Eq,Ord,RefinedDouble]
21 |
22 | ||| Safely convert a floating point number to a `Scale`
23 | export
24 | scale : Double -> Scale
25 | scale x = case refineScale x of
26 |   Just s  => s
27 |   Nothing => if x < 1.0e-6 then S 1.0e-6 else S 1.0e6
28 |
29 | ||| Invert the scaling factor so that `x * inverse x == 1`
30 | ||| (modulo rounding errors).
31 | export %inline
32 | inverse : Scale -> Scale
33 | inverse (S v) = scale $ 1 / v
34 |
35 | ||| Multiply two scaling factors.
36 | export %inline
37 | (*) : Scale -> Scale -> Scale
38 | S x * S y = scale $ x * y
39 |
40 | ||| Divide a scaling factor by another one
41 | export %inline
42 | (/) : Scale -> Scale -> Scale
43 | S x / S y = scale $ x / y
44 |