0 | module Data.Fixed

  2 | import Data.String

  4 | %hide Data.List.replicate

 11 | public export

 12 | data Fixed : (res : Integer) -> Type where

 13 |   MkFixed :  Integer

 14 |           -> Fixed res

 25 | showFixed :  {res : Integer}

 26 |           -> (chop : Bool)

 27 |           -> (fa : Fixed res)

 28 |           -> String

 29 | showFixed chop fa@(MkFixed a) =

 30 |   case a < 0 of

 31 |     True =>

 32 |       let fixed = assert_total $

 33 |                   showFixed {res}

 34 |                             chop

 35 |                             (MkFixed (negate a))

 36 |         in "-" ++ fixed

 37 |     False =>

 38 |       let (i, d)  = divMod a res

 39 |           digits  = cast {to=Int} (length (show res)) - 1

 40 |           maxnum  = pow 10 (cast {to=Double} digits)

 41 |           fracnum = divCeil (d * cast {to=Integer} maxnum) res

 42 |           dot     = withDot (showIntegerZeros chop (cast digits) fracnum)

 43 |        in show i ++ dot

 44 |   where

 45 |     sigNum :  Integer

 46 |            -> Integer

 47 |     sigNum n =

 48 |       case n < 0 of

 49 |         True  =>

 50 |           -1

 51 |         False =>

 52 |           case n == 0 of

 53 |             True  =>

 54 |               0

 55 |             False =>

 56 |               1

 57 |     divMod :  Integer

 58 |            -> Integer

 59 |            -> (Integer, Integer)

 60 |     divMod n d =

 61 |       let q = div n d

 62 |           r = mod n d

 63 |         in case sigNum r == negate (sigNum d) of

 64 |              True  =>

 65 |                (q - 1, r + d)

 66 |              False =>

 67 |                (q, r)

 68 |     chopZeros :  Integer

 69 |               -> String

 70 |     chopZeros 0 =

 71 |       ""

 72 |     chopZeros x =

 73 |       case mod x 10 == 0 of

 74 |         True  =>

 75 |           chopZeros (assert_smaller x (div x 10))

 76 |         False =>

 77 |           show x

 78 |     showIntegerZeros :  Bool

 79 |                      -> Nat

 80 |                      -> Integer

 81 |                      -> String

 82 |     showIntegerZeros True _      0 =

 83 |       ""

 84 |     showIntegerZeros chop digits n =

 85 |       let s       = show n

 86 |           s'      = case chop of

 87 |                       True  =>

 88 |                         chopZeros n

 89 |                       False =>

 90 |                         s

 91 |           padding = replicate (digits `minus` length s) '0'

 92 |         in padding ++ s'

 93 |     withDot :  String

 94 |             -> String

 95 |     withDot "" =

 96 |       ""

 97 |     withDot s  =

 98 |       "." ++ s

 99 |     divCeil :  Integer

100 |             -> Integer

101 |             -> Integer

102 |     divCeil x y =

103 |       (x + y - 1) `div` y

109 | public export

110 | {n : Integer} -> Num (Fixed n) where

111 |   (MkFixed a) + (MkFixed b) = MkFixed (a + b)

112 |   (MkFixed a) * (MkFixed b) = MkFixed (div (a * b) n)

113 |   fromInteger i             = MkFixed (i * n)

115 | public export

116 | {n : Integer} -> Neg (Fixed n) where

117 |   negate (MkFixed a)          = MkFixed (negate a)

118 |   (-) (MkFixed a) (MkFixed b) = MkFixed (a - b)

120 | public export

121 | {n : Integer} -> Fractional (Fixed n) where

122 |   (MkFixed a) / (MkFixed b) = MkFixed (div (a * n) b)

123 |   recip (MkFixed a)         = MkFixed (div (n * n) a)

125 | public export

126 | {n : Integer} -> Eq (Fixed n) where

127 |   (MkFixed a) == (MkFixed b) = a == b

129 | public export

130 | {n : Integer} -> Ord (Fixed n) where

131 |   compare (MkFixed a) (MkFixed b) = compare a b

133 | public export

134 | {n : Integer} -> Show (Fixed n) where

135 |   showPrec p fixed@(MkFixed a) =

136 |     showParens (p >= App && a < 0) $

137 |       showFixed False fixed

148 | public export

149 | Uni : Type

150 | Uni = Fixed 1

161 | public export

162 | Deci : Type

163 | Deci = Fixed 10

174 | public export

175 | Centi : Type

176 | Centi = Fixed 100

187 | public export

188 | Milli : Type

189 | Milli = Fixed 1000

200 | public export

201 | TenthMilli : Type

202 | TenthMilli = Fixed 10000

213 | public export

214 | HundredthMilli : Type

215 | HundredthMilli = Fixed 100000

226 | public export

227 | Micro : Type

228 | Micro = Fixed 1000000

239 | public export

240 | DeciMicro : Type

241 | DeciMicro = Fixed 10000000

252 | public export

253 | CentiMicro : Type

254 | CentiMicro = Fixed 100000000

265 | public export

266 | Nano : Type

267 | Nano = Fixed 1000000000

278 | public export

279 | DeciNano : Type

280 | DeciNano = Fixed 10000000000

291 | public export

292 | CentiNano : Type

293 | CentiNano = Fixed 100000000000

304 | public export

305 | Pico : Type

306 | Pico = Fixed 1000000000000

314 | withResolution :  {res : Integer}

315 |                -> (f : Integer -> b)

316 |                -> b

317 | withResolution f =

318 |   f res