0 | module Data.ScientificNotation
  1 |
  2 | import Data.List
  3 | import Data.Nat
  4 | import Data.Num
  5 | import Data.String
  6 |
  7 | import Misc
  8 |
  9 | {-------------------------------------------------------------------------------
 10 | {-------------------------------------------------------------------------------
 11 | This file contains custom scientific formatting for numeric types.
 12 |
 13 | While Idris' `Show` for numeric primitives already exists, it:
 14 | * does not permit precise control over ranges the scientific notation is invoked
 15 | * is backend-dependent, meaning that Scheme formats differently than JS
 16 | * does not allow us to do a two-pass formatting such that global tensor 
 17 |   information dictates the render for a particular element. (I.e. if any number
 18 |   is within scientific notation range, then all numbers get rendered in scientific notation)
 19 |
 20 | -------------------------------------------------------------------------------}
 21 | -------------------------------------------------------------------------------}
 22 |
 23 | ||| Interface for displaying numeric types that dynamically switches between
 24 | ||| standard and scientific notation based on magnitude
 25 | ||| If `forceScientific` is `True`, then we render in scientific notation no
 26 | ||| matter what the value is
 27 | public export
 28 | interface Num a => ScientificDisplay a where
 29 |   -- ideally we'd use something this: {default False forceScientific : Bool} -> 
 30 |   showSci : a -> String
 31 |
 32 | ||| Magnitude above which `Double` values switch to scientific notation.
 33 | public export
 34 | sciUpperM : Double
 35 | sciUpperM = 1.0e6
 36 |
 37 | ||| Magnitude below which `Double` values switch to scientific notation.
 38 | public export
 39 | sciLowerM : Double
 40 | sciLowerM = 1.0e-4
 41 |
 42 | ||| Default precision used by numeric primitives with scientific notation
 43 | ||| This is maximum, trailing zeros are removed.
 44 | public export
 45 | defaultScientificPrecision : Nat
 46 | defaultScientificPrecision = 4
 47 |
 48 | ||| Symbol used to denote the exponent in scientific notation, i.e. `1.0e+03`
 49 | public export
 50 | sciSymbol : Char
 51 | sciSymbol = 'e'
 52 |
 53 | ||| True when `d` is non-zero and outside the range
 54 | public export
 55 | needsScientific : Double -> Bool
 56 | needsScientific d = d /= 0.0 && (m < sciLowerM || m >= sciUpperM)
 57 |   where m = abs d
 58 |
 59 | --------------------------------------------------------------------------------
 60 | -- Formatting primitives
 61 | --------------------------------------------------------------------------------
 62 |
 63 | ||| Format an integer exponent as `e+XX` or `e-XX`.
 64 | ||| `formatExp 5 == "e+05"`
 65 | ||| `formatExp -123 == "e-123"`
 66 | public export
 67 | formatExp : Integer -> String
 68 | formatExp n = singleton sciSymbol ++ sign ++ applyWhen (length ds < 2) ("0" ++) ds
 69 |   where sign : String
 70 |         sign = if n < 0 then "-" else "+"
 71 |         ds : String
 72 |         ds = show (abs n)
 73 |
 74 |
 75 | ||| Multiply a decimal number by `10^prec`, and round it to the nearest integer
 76 | ||| `round 2 3.14159 == 314`
 77 | ||| `round 3 3.14159 == 3142`
 78 | ||| `round 3 3.14100 == 3141`
 79 | roundScaled : (prec : Nat) -> Double -> Integer
 80 | roundScaled prec d = cast (floor (abs d * pow 10.0 (cast prec) + 0.5))
 81 |
 82 | ||| Format a non-negative integer as a decimal string.
 83 | ||| `prec` controls how many digits appear after the decimal point
 84 | ||| Input is taken to already be multiplied by `10^prec`
 85 | ||| Zero-padding is added on the left when there are not enough digits.
 86 | ||| ```
 87 | ||| formatDigits 5 314159 == "3.14159"
 88 | ||| formatDigits 3 314159 == "314.159"
 89 | ||| formatDigits 2 5      == "0.05"
 90 | ||| formatDigits 0 42     == "42"
 91 | ||| ```
 92 | public export
 93 | formatDigits : (prec : Nat) -> (digits : Integer) -> String
 94 | formatDigits 0 n = show n
 95 | formatDigits prec n = substr 0 nDig padded ++ "." ++ substr nDig prec padded
 96 |   where len : Nat
 97 |         len = length (show n)
 98 |         padded : String
 99 |         padded = applyWhen (len <= prec)
100 |                    (pack (replicate (S prec `minus` len) '0') ++)
101 |                    (show n)
102 |         nDig : Nat -- number of digits to the left of the decimal point
103 |         nDig = length padded `minus` prec
104 |
105 | ||| Format a Double in standard notation with a fixed number of decimal places.
106 | ||| Rounds the last decimal to the nearest digit, and possibly pads with zeros,
107 | ||| if precision is greater than the number of digits after the decimal point.
108 | ||| ```
109 | ||| showDoublePrecision 3 3.14159  == "3.142"
110 | ||| showDoublePrecision 3 3.14100  == "3.141"
111 | ||| showDoublePrecision 0 3.14159  == "3"
112 | ||| showDoublePrecision 4 100.0    == "100.0000"
113 | ||| ```
114 | public export
115 | showDoublePrecision : (precision : Nat) -> Double -> String
116 | showDoublePrecision prec d = applyWhen (d < 0) ("-" ++) $
117 |   formatDigits prec (roundScaled prec d)
118 |
119 | ||| Decompose `|d|` into `(mantissa, exponent)` with `1 ≤ mantissa < 10`,
120 | ||| correcting the "one-decade" drift that `floor . log10` can produce at
121 | ||| decade boundaries (e.g. `log10 0.999... = -1.4e-16`, not 0).
122 | ||| Pre: `d ≠ 0`.
123 | decimalDecompose : Double -> (Double, Integer)
124 | decimalDecompose d =
125 |   let m  = abs d
126 |       e  = cast (floor (log m / log 10.0))
127 |       m0 = m / pow 10.0 (cast e)
128 |   in if m0 >= 10.0    then (m0 / 10.0, e + 1)
129 |      else if m0 < 1.0 then (m0 * 10.0, e - 1)
130 |      else                  (m0,        e)
131 |
132 | ||| Format a Double in scientific notation with a fixed number of
133 | ||| decimal places in the mantissa.
134 | |||
135 | ||| ```
136 | ||| showDoubleScientific 5 3.14159    == "3.14159e+00"
137 | ||| showDoubleScientific 5 (-0.005)   == "-5.00000e-03"
138 | ||| showDoubleScientific 5 100.0      == "1.00000e+02"
139 | ||| showDoubleScientific 5 0.0000001  == "1.00000e-07"
140 | ||| ```
141 | public export
142 | showDoubleScientific : (precision : Nat) -> Double -> String
143 | showDoubleScientific prec 0.0 = formatDigits prec 0 ++ formatExp 0
144 | showDoubleScientific prec d =
145 |   applyWhen (d < 0) ("-" ++) $ formatDigits prec mantInt ++ formatExp expFinal
146 |   where
147 |     decomp : (Double, Integer)
148 |     decomp = decimalDecompose d
149 |
150 |     -- Round mantissa to a scaled integer with `prec` digits of precision.
151 |     rounded : Integer
152 |     rounded = roundScaled prec (fst decomp)
153 |
154 |     -- If rounding pushed the mantissa to ≥ 10, carry one decade.
155 |     overflow : Bool
156 |     overflow = rounded >= cast (pow 10.0 (cast (S prec)))
157 |
158 |     mantInt : Integer
159 |     mantInt = applyWhen overflow (`div` 10) rounded
160 |
161 |     expFinal : Integer
162 |     expFinal = applyWhen overflow (+ 1) (snd decomp)
163 |
164 | ||| Remove trailing zeros after the decimal point, keeping at least one.
165 | ||| Handles scientific notation, i.e.`"1.0000e-07"` becomes `"1.0e-07"`
166 | public export
167 | trimTrailingZeros : String -> String
168 | trimTrailingZeros s = case break (== sciSymbol) (unpack s) of
169 |   (mant, expPart) => case break (== '.') mant of
170 |     (_, []) => s
171 |     (whole, _ :: frac) =>
172 |       let trimmed : String
173 |           trimmed = case reverse (dropWhile (== '0') (reverse frac)) of
174 |                       [] => "0"
175 |                       xs => pack xs
176 |       in pack whole ++ "." ++ trimmed ++ pack expPart
177 |
178 | --------------------------------------------------------------------------------
179 | -- ScientificDisplay instances
180 | --------------------------------------------------------------------------------
181 |
182 | ||| Render a value using `showDoubleScientific` after casting to `Double`.
183 | ||| Used by integer-like instances when the magnitude warrants sci notation.
184 | showAsScientific : Cast a Double => a -> String
185 | showAsScientific n = trimTrailingZeros $
186 |   showDoubleScientific defaultScientificPrecision (cast n)
187 |
188 | ||| Format a Double for display: fixed notation for values in the range
189 | ||| `[scientificLowerMagnitude, scientificUpperMagnitude)`, scientific
190 | ||| notation outside that range, with redundant trailing zeros removed.
191 | public export
192 | ScientificDisplay Double where
193 |   showSci d = trimTrailingZeros $ case needsScientific d of
194 |     True => showDoubleScientific defaultScientificPrecision d
195 |     False => showDoublePrecision  defaultScientificPrecision d
196 |
197 | public export
198 | ScientificDisplay Integer where
199 |   showSci n = case cast (abs n) < sciUpperM of
200 |     True => show n -- builtin `Show` never uses scientific notation
201 |     False => showAsScientific n
202 |
203 | public export
204 | ScientificDisplay Nat where
205 |   showSci n = case cast n < sciUpperM of
206 |     True => show n -- builtin `Show` never uses scientific notation
207 |     False => showAsScientific n
208 |
209 | public export
210 | ScientificDisplay Unit where
211 |   showSci () = "()"
212 |
213 | public export
214 | ScientificDisplay a => ScientificDisplay b => ScientificDisplay (a, b) where
215 |   showSci (x, y) = "(\{showSci x}, \{showSci y})"
216 |