Skip to content

Instantly share code, notes, and snippets.

@yuga

yuga/decimal.idr

Last active Aug 29, 2015
Embed
What would you like to do?
not deal with seriously
module decimal
record Decimal : Nat -> Type where
MkDecimal : (places : Nat) -> (mantissa : Integer) -> Decimal places
signum : Integer -> Integer
signum n = case compare n 0 of
LT => (-1)
EQ => 0
GT => 1
divRound : Integer -> Integer -> Integer
divRound n1 n2 = if (abs r * 2) >= (abs n2) then n + (signum n1) else n where
n = n1 `div` n2
r = n1 `mod` n2
power' : Integer -> Nat -> Integer
power' x Z = 1
power' x n = x * (x `power'` (n-1))
roundTo : (np : Nat) -> Decimal op-> Decimal np
roundTo np d = case d of
MkDecimal op m => MkDecimal np (calc m)
where
divisor : Integer
divisor = 10 `power'` (op-np)
multiplier : Integer
multiplier = 10 `power'` (np-op)
calc : Integer -> Integer
calc m = case compare np op of
LT => m `divRound` divisor
EQ => m
GT => m * multiplier
*decimal> :let d : Decimal 3; d = MkDecimal 3 123456
*decimal> d
MkDecimal 3 123456 : Decimal 3
*decimal> mantissa d
123456 : Integer
*decimal> roundTo 2 d
MkDecimal 2 12346 : Decimal 2
*decimal> roundTo 5 d
MkDecimal 5 12345600 : Decimal 5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment