pwncash/dhall/math.dhall

193 lines
5.0 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 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
}