0 | module Data.Fixed

  2 | import Data.String

  4 | %hide Data.List.replicate

 12 | public export

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

 14 |   MkFixed :  Integer

 15 |           -> Fixed res

 27 | showFixed :  {res : Integer}

 28 |           -> (chop : Bool)

 29 |           -> (fa : Fixed res)

 30 |           -> String

 31 | showFixed chop fa@(MkFixed a) =

 32 |   case a < 0 of

 33 |     True =>

 34 |       let fixed = assert_total $

 35 |                   showFixed {res}

 36 |                             chop

 37 |                             (MkFixed (negate a))

 38 |         in "-" ++ fixed

 39 |     False =>

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

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

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

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

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

 45 |        in show i ++ dot

 46 |   where

 47 |     sigNum :  Integer

 48 |            -> Integer

 49 |     sigNum n =

 50 |       case n < 0 of

 51 |         True  =>

 52 |           -1

 53 |         False =>

 54 |           case n == 0 of

 55 |             True  =>

 56 |               0

 57 |             False =>

 58 |               1

 59 |     divMod :  Integer

 60 |            -> Integer

 61 |            -> (Integer, Integer)

 62 |     divMod n d =

 63 |       let q = div n d

 64 |           r = mod n d

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

 66 |              True  =>

 67 |                (q - 1, r + d)

 68 |              False =>

 69 |                (q, r)

 70 |     chopZeros :  Integer

 71 |               -> String

 72 |     chopZeros 0 =

 73 |       ""

 74 |     chopZeros x =

 75 |       case mod x 10 == 0 of

 76 |         True  =>

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

 78 |         False =>

 79 |           show x

 80 |     showIntegerZeros :  Bool

 81 |                      -> Nat

 82 |                      -> Integer

 83 |                      -> String

 84 |     showIntegerZeros True _      0 =

 85 |       ""

 86 |     showIntegerZeros chop digits n =

 87 |       let s       = show n

 88 |           s'      = case chop of

 89 |                       True  =>

 90 |                         chopZeros n

 91 |                       False =>

 92 |                         s

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

 94 |         in padding ++ s'

 95 |     withDot :  String

 96 |             -> String

 97 |     withDot "" =

 98 |       ""

 99 |     withDot s  =

100 |       "." ++ s

101 |     divCeil :  Integer

102 |             -> Integer

103 |             -> Integer

104 |     divCeil x y =

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

111 | public export

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

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

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

115 |   fromInteger i             = MkFixed (i * n)

117 | public export

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

119 |   negate (MkFixed a)          = MkFixed (negate a)

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

122 | public export

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

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

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

127 | public export

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

129 |   (MkFixed a) == (MkFixed b) = a == b

131 | public export

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

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

135 | public export

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

137 |   showPrec p fixed@(MkFixed a) =

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

139 |       showFixed False fixed

151 | public export

152 | Uni : Type

153 | Uni = Fixed 1

165 | public export

166 | Deci : Type

167 | Deci = Fixed 10

179 | public export

180 | Centi : Type

181 | Centi = Fixed 100

193 | public export

194 | Milli : Type

195 | Milli = Fixed 1000

207 | public export

208 | TenthMilli : Type

209 | TenthMilli = Fixed 10000

221 | public export

222 | HundredthMilli : Type

223 | HundredthMilli = Fixed 100000

235 | public export

236 | Micro : Type

237 | Micro = Fixed 1000000

249 | public export

250 | DeciMicro : Type

251 | DeciMicro = Fixed 10000000

263 | public export

264 | CentiMicro : Type

265 | CentiMicro = Fixed 100000000

277 | public export

278 | Nano : Type

279 | Nano = Fixed 1000000000

291 | public export

292 | DeciNano : Type

293 | DeciNano = Fixed 10000000000

305 | public export

306 | CentiNano : Type

307 | CentiNano = Fixed 100000000000

319 | public export

320 | Pico : Type

321 | Pico = Fixed 1000000000000

330 | withResolution :  {res : Integer}

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

332 |                -> b

333 | withResolution f =

334 |   f res