ADD mathy stuff
This commit is contained in:
parent
2a38b52fc4
commit
ab70012642
|
|
@ -0,0 +1,147 @@
|
|||
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 }
|
||||
|
|
@ -4,6 +4,10 @@ let List/map =
|
|||
|
||||
let T = ./Types.dhall
|
||||
|
||||
let D = ./Decimal.dhall
|
||||
|
||||
let M = ./math.dhall
|
||||
|
||||
let nullSplit =
|
||||
\(a : T.SplitAcnt) ->
|
||||
\(c : T.SplitCur) ->
|
||||
|
|
@ -112,19 +116,6 @@ let part1_ =
|
|||
\(a : T.SplitAcnt) ->
|
||||
partN c a "" ([] : List PartSplit)
|
||||
|
||||
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 addDay =
|
||||
\(x : T.GregorianM) ->
|
||||
\(d : Natural) ->
|
||||
|
|
@ -170,8 +161,6 @@ in { nullSplit
|
|||
, partN
|
||||
, part1
|
||||
, part1_
|
||||
, d
|
||||
, d_
|
||||
, addDay
|
||||
, comma = 44
|
||||
, tab = 9
|
||||
|
|
@ -186,3 +175,5 @@ in { nullSplit
|
|||
, PartSplit
|
||||
}
|
||||
/\ T
|
||||
/\ D
|
||||
/\ M
|
||||
|
|
|
|||
|
|
@ -0,0 +1,192 @@
|
|||
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 foldWhile
|
||||
: forall (n : Natural) ->
|
||||
forall (res : Type) ->
|
||||
forall (succ : res -> Optional res) ->
|
||||
forall (zero : res) ->
|
||||
res
|
||||
= \(n : Natural) ->
|
||||
\(R : Type) ->
|
||||
\(succ : R -> Optional R) ->
|
||||
\(zero : R) ->
|
||||
let Acc
|
||||
: Type
|
||||
= { current : R, done : Bool }
|
||||
|
||||
let update
|
||||
: Acc -> Acc
|
||||
= \(acc : Acc) ->
|
||||
if acc.done
|
||||
then acc
|
||||
else merge
|
||||
{ Some = \(r : R) -> acc // { current = r }
|
||||
, None = acc // { done = True }
|
||||
}
|
||||
(succ acc.current)
|
||||
|
||||
let init
|
||||
: Acc
|
||||
= { current = zero, done = False }
|
||||
|
||||
let result
|
||||
: Acc
|
||||
= Natural/fold n Acc update init
|
||||
|
||||
in result.current
|
||||
|
||||
let DivRes = \(a : Type) -> { remainder : a, quotiant : a }
|
||||
|
||||
let QED = assert : True === True
|
||||
|
||||
let downwardSteps =
|
||||
\(x : Natural) ->
|
||||
\(y : Natural) ->
|
||||
let initAcc
|
||||
: DivRes Natural
|
||||
= { remainder = x, quotiant = 0 }
|
||||
|
||||
let updateAcc
|
||||
: DivRes Natural -> Optional (DivRes Natural)
|
||||
= \(acc : DivRes Natural) ->
|
||||
if Nat.lessThan acc.remainder y
|
||||
then None (DivRes Natural)
|
||||
else Some
|
||||
{ remainder = Natural/subtract y acc.remainder
|
||||
, quotiant = acc.quotiant + 1
|
||||
}
|
||||
|
||||
in foldWhile (x + 1) (DivRes Natural) updateAcc initAcc
|
||||
|
||||
let Natural/quotRemUnsafe
|
||||
: forall (a : Natural) -> Natural -> DivRes Natural
|
||||
= \(x : Natural) -> \(y : Natural) -> downwardSteps y x
|
||||
|
||||
let Natural/quotRem
|
||||
: forall (a : Natural) ->
|
||||
Nat.isZero a == False === True ->
|
||||
Natural ->
|
||||
DivRes Natural
|
||||
= \(x : Natural) ->
|
||||
\(_ : Nat.isZero x == False === True) ->
|
||||
\(y : Natural) ->
|
||||
Natural/quotRemUnsafe x y
|
||||
|
||||
let Natural/div
|
||||
: forall (a : Natural) ->
|
||||
Nat.isZero a == False === True ->
|
||||
Natural ->
|
||||
Natural
|
||||
= \(x : Natural) ->
|
||||
\(a : Nat.isZero x == False === True) ->
|
||||
\(y : Natural) ->
|
||||
(Natural/quotRem x a y).quotiant
|
||||
|
||||
let d1 = assert : Natural/div 1 QED 1 === 1
|
||||
|
||||
let d2 = assert : Natural/div 2 QED 1 === 0
|
||||
|
||||
let d3 = assert : Natural/div 2 QED 5 === 2
|
||||
|
||||
let Natural/rem
|
||||
: forall (a : Natural) ->
|
||||
Nat.isZero a == False === True ->
|
||||
Natural ->
|
||||
Natural
|
||||
= \(x : Natural) ->
|
||||
\(a : Nat.isZero x == False === True) ->
|
||||
\(y : Natural) ->
|
||||
(Natural/quotRem x a y).remainder
|
||||
|
||||
let r1 = assert : Natural/rem 2 QED 4 === 0
|
||||
|
||||
let r2 = assert : Natural/rem 2 QED 5 === 1
|
||||
|
||||
let Natural/pow
|
||||
: Natural -> Natural -> Natural
|
||||
= \(b : Natural) ->
|
||||
\(p : Natural) ->
|
||||
Natural/fold p Natural (\(x : Natural) -> x * b) 1
|
||||
|
||||
let p1 = assert : Natural/pow 10 1 === 10
|
||||
|
||||
let p2 = assert : Natural/pow 10 3 === 1000
|
||||
|
||||
let p3 = assert : Natural/pow 10 0 === 1
|
||||
|
||||
let Integer/quotRemUnsafe
|
||||
: Natural -> Integer -> DivRes Integer
|
||||
= \(x : Natural) ->
|
||||
\(y : Integer) ->
|
||||
if Int.equal y +0
|
||||
then { quotiant = +0, remainder = +0 }
|
||||
else let sign = if Int.positive y then +1 else -1
|
||||
|
||||
let toInt = \(x : Natural) -> Int.multiply sign (Nat.toInteger x)
|
||||
|
||||
let res = Natural/quotRemUnsafe x (Int.abs y)
|
||||
|
||||
in { quotiant = toInt res.quotiant
|
||||
, remainder = toInt res.remainder
|
||||
}
|
||||
|
||||
let Integer/quotRem
|
||||
: forall (a : Natural) ->
|
||||
Nat.isZero a == False === True ->
|
||||
Integer ->
|
||||
DivRes Integer
|
||||
= \(x : Natural) ->
|
||||
\(_ : Nat.isZero x == False === True) ->
|
||||
\(y : Integer) ->
|
||||
Integer/quotRemUnsafe x y
|
||||
|
||||
let Integer/div
|
||||
: forall (a : Natural) ->
|
||||
Nat.isZero a == False === True ->
|
||||
Integer ->
|
||||
Integer
|
||||
= \(x : Natural) ->
|
||||
\(a : Nat.isZero x == False === True) ->
|
||||
\(y : Integer) ->
|
||||
(Integer/quotRem x a y).quotiant
|
||||
|
||||
let id1 = assert : Integer/div 1 QED +3 === +3
|
||||
|
||||
let id2 = assert : Integer/div 1 QED -3 === -3
|
||||
|
||||
let id3 = assert : Integer/div 2 QED -7 === -3
|
||||
|
||||
let Integer/rem
|
||||
: forall (a : Natural) ->
|
||||
Nat.isZero a == False === True ->
|
||||
Integer ->
|
||||
Integer
|
||||
= \(x : Natural) ->
|
||||
\(a : Nat.isZero x == False === True) ->
|
||||
\(y : Integer) ->
|
||||
(Integer/quotRem x a y).remainder
|
||||
|
||||
let ir1 = assert : Integer/rem 1 QED +3 === +0
|
||||
|
||||
let ir2 = assert : Integer/rem 1 QED -3 === -0
|
||||
|
||||
let ir3 = assert : Integer/rem 2 QED -7 === -1
|
||||
|
||||
in { QED
|
||||
, DivRes
|
||||
, Natural/div
|
||||
, Natural/rem
|
||||
, Natural/quotRem
|
||||
, Natural/quotRemUnsafe
|
||||
, Natural/pow
|
||||
, Integer/quotRem
|
||||
, Integer/quotRemUnsafe
|
||||
, Integer/div
|
||||
, Integer/rem
|
||||
}
|
||||
Loading…
Reference in New Issue