
  0 | module Text.Printf
  1 | 
  2 | import Data.DPair
  3 | import Data.Refined.Integer
  4 | 
  5 | %default total
  6 | 
  7 | pow10 : Nat -> Integer
  8 | pow10 0     = 1
  9 | pow10 (S k) = 10 * pow10 k
 10 | 
 11 | ||| Extract the `n` most significant digits from a
 12 | ||| non-negative integer plus the exponent representing
 13 | ||| the remaining digits.
 14 | |||
 15 | ||| For example, for `v = 123456789` and `n = 3`, this
 16 | ||| would return `(123,5)`, so that `v ~ 123 * 10^5`.
 17 | export
 18 | significant :
 19 |      (v : Integer)
 20 |   -> (n : Nat)
 21 |   -> {auto 0 _ : 0 <= v}
 22 |   -> (Integer,Nat)
 23 | significant v n = go v 0 (pow10 n)
 24 |   -- This just keeps dividing the remainder by 10
 25 |   -- until it drops below the number of desired digits.
 26 |   -- The complexity comes from the totality proof, which
 27 |   -- is definitely overkill here but still oddly satisfying.
 28 |   where
 29 |     go :
 30 |          (rem : Integer)
 31 |       -> (exp : Nat)
 32 |       -> (max : Integer)
 33 |       -> (Integer,Nat)
 34 |     go rem exp max = case lt rem max of
 35 |       Nothing0 => go (assert_smaller rem (rem `div` 10)) (S exp) max
 36 |       Just0 x  => (rem,exp)
 37 |