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