148 lines
4.4 KiB
Plaintext
148 lines
4.4 KiB
Plaintext
let Nat =
|
|
https://prelude.dhall-lang.org/v21.1.0/Natural/package.dhall
|
|
sha256:ee9ed2b28a417ed4e9a0c284801b928bf91b3fbdc1a68616347678c1821f1ddf
|
|
|
|
let Int =
|
|
https://prelude.dhall-lang.org/v21.1.0/Integer/package.dhall
|
|
sha256:d1a572ca3a764781496847e4921d7d9a881c18ffcfac6ae28d0e5299066938a0
|
|
|
|
let T = ./Types.dhall
|
|
|
|
let M = ./math.dhall
|
|
|
|
let dec =
|
|
\(s : Bool) ->
|
|
\(w : Natural) ->
|
|
\(d : Natural) ->
|
|
\(p : Natural) ->
|
|
{ whole = w, decimal = d, precision = p, sign = s } : T.Decimal
|
|
|
|
let dec2 = \(s : Bool) -> \(w : Natural) -> \(d : Natural) -> dec s w d 2
|
|
|
|
let d = dec2 True
|
|
|
|
let d_ = dec2 False
|
|
|
|
let Decimal/toNatural =
|
|
\(a : T.Decimal) ->
|
|
let p = M.Natural/pow 10 a.precision in a.whole * p + a.decimal
|
|
|
|
let Decimal/toInteger =
|
|
\(x : T.Decimal) ->
|
|
let n = Nat.toInteger (Decimal/toNatural x)
|
|
|
|
in if x.sign == True then n else Int.negate n
|
|
|
|
let Decimal/add
|
|
: T.Decimal -> T.Decimal -> T.Decimal
|
|
= \(a : T.Decimal) ->
|
|
\(b : T.Decimal) ->
|
|
let final_precision = Nat.max a.precision b.precision
|
|
|
|
let to_int =
|
|
\(z : T.Decimal) ->
|
|
Decimal/toInteger
|
|
( z
|
|
// { precision = final_precision
|
|
, decimal =
|
|
z.decimal
|
|
* M.Natural/pow
|
|
10
|
|
(Nat.subtract z.precision final_precision)
|
|
}
|
|
)
|
|
|
|
let x = to_int a
|
|
|
|
let y = to_int b
|
|
|
|
let p = M.Natural/pow 10 final_precision
|
|
|
|
let res = M.Integer/quotRemUnsafe p (Int.add x y)
|
|
|
|
in dec
|
|
(Int.positive res.quotiant)
|
|
(Int.abs res.quotiant)
|
|
(Int.abs res.remainder)
|
|
final_precision
|
|
|
|
let test =
|
|
assert : Decimal/add (dec True 1 0 0) (dec True 1 0 0) === dec True 2 0 0
|
|
|
|
let test =
|
|
assert
|
|
: Decimal/add (dec True 1 5 1) (dec False 2 0 0) === dec False 0 5 1
|
|
|
|
let Decimal/multiply
|
|
: T.Decimal -> T.Decimal -> T.Decimal
|
|
= \(a : T.Decimal) ->
|
|
\(b : T.Decimal) ->
|
|
let x = Decimal/toNatural a
|
|
|
|
let y = Decimal/toNatural b
|
|
|
|
let p = a.precision + b.precision
|
|
|
|
let res = M.Natural/quotRemUnsafe (M.Natural/pow 10 p) (x * y)
|
|
|
|
in dec (a.sign == b.sign) res.quotiant res.remainder p
|
|
|
|
let test =
|
|
assert
|
|
: Decimal/multiply (dec True 1 0 1) (dec True 0 0 0) === dec True 0 0 1
|
|
|
|
let test =
|
|
assert
|
|
: Decimal/multiply (dec True 1 0 1) (dec True 1 0 0) === dec True 1 0 1
|
|
|
|
let test =
|
|
assert
|
|
: Decimal/multiply (dec True 1 4 1) (dec False 2 0 2)
|
|
=== dec False 2 800 3
|
|
|
|
let Decimal/round
|
|
: Natural -> T.Decimal -> T.Decimal
|
|
= \(p : Natural) ->
|
|
\(a : T.Decimal) ->
|
|
if Nat.equal a.precision p
|
|
then a
|
|
else if Nat.greaterThan p a.precision
|
|
then a
|
|
// { precision = p
|
|
, decimal =
|
|
a.decimal * M.Natural/pow 10 (Nat.subtract a.precision p)
|
|
}
|
|
else let subp = M.Natural/pow 10 (Nat.subtract (p + 1) a.precision)
|
|
|
|
let subRes =
|
|
M.Natural/quotRem
|
|
10
|
|
M.QED
|
|
(M.Natural/quotRemUnsafe subp a.decimal).quotiant
|
|
|
|
in if Nat.lessThan subRes.remainder 5
|
|
then a // { precision = p, decimal = subRes.quotiant }
|
|
else let dec = subRes.quotiant + 1
|
|
|
|
in if Nat.equal dec (M.Natural/pow 10 p)
|
|
then a
|
|
// { whole = a.whole + 1
|
|
, decimal = 0
|
|
, precision = p
|
|
}
|
|
else a // { decimal = dec, precision = p }
|
|
|
|
let test = assert : Decimal/round 2 (dec True 0 49 2) === dec True 0 49 2
|
|
|
|
let test = assert : Decimal/round 1 (dec True 0 49 2) === dec True 0 5 1
|
|
|
|
let test = assert : Decimal/round 0 (dec True 0 49 2) === dec True 0 0 0
|
|
|
|
let test =
|
|
assert
|
|
: Decimal/round 3 (dec True 0 49 2) === Decimal/round 3 (dec True 0 490 3)
|
|
|
|
let test = assert : Decimal/round 1 (dec True 0 95 2) === dec True 1 0 1
|
|
|
|
in { dec, dec2, d, d_, Decimal/add, Decimal/multiply, Decimal/round }
|