Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@winitzki
winitzki committed Oct 14, 2024
1 parent efaf218 commit 24487e4
Show file tree
Hide file tree
Showing 5 changed files with 254 additions and 108 deletions.
195 changes: 143 additions & 52 deletions tutorial/Float/Type.dhall
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,34 @@ let Float = FloatBare ⩓ FloatExtraData

let D = ./Arithmetic.dhall

let divmod = D.divrem
let Result = D.Result

let divmod
: Natural → Natural → Result
= stop.reduce_growth
Natural
stop.predicate_Natural
(Natural → Result)
(λ(_ : Natural) → { div = 0, rem = 0 })
D.divrem

let log
: Natural → Natural → Natural
= stop.reduce_growth
Natural
stop.predicate_Natural
(Natural → Natural)
(λ(_ : Natural) → 0)
D.log

let power
: Natural → Natural → Natural
= stop.reduce_growth
Natural
stop.predicate_Natural
(Natural → Natural)
(λ(_ : Natural) → 0)
D.power

let dummyFloat =
{ mantissa = 0
Expand All @@ -57,48 +84,66 @@ let Float/addExtraData
Float
dummyFloat
( λ(args : FloatBare) →
let topPower = D.log Base args.mantissa
let topPower = log Base args.mantissa

let r = divmod args.mantissa (D.power Base topPower)
let r = divmod args.mantissa (power Base topPower)

in args ⫽ { topPower, leadDigit = r.div, remaining = r.rem }
)

let FloatBare/create
: Integer → Integer → FloatBare
= λ(x : Integer) →
λ(exp : Integer) →
{ mantissa = Integer/abs x
, mantissaPositive = Integer/positive x
, exponent = exp
}
= stop.reduce_growth
Integer
stop.predicate_Integer
(Integer → FloatBare)
(λ(_ : Integer) → dummyFloat.(FloatBare))
( λ(x : Integer) →
λ(exp : Integer) →
{ mantissa = Integer/abs x
, mantissaPositive = Integer/positive x
, exponent = exp
}
)

let Float/zero = Float/addExtraData (FloatBare/create +0 +0)

let normalizeStep
: FloatBare → FloatBare
= λ(x : FloatBare) →
if Natural/isZero x.mantissa
then Float/zero.(FloatBare)
else if Natural/lessThan x.mantissa Base
then x
else let r = divmod x.mantissa Base

in if Natural/isZero r.rem
then x
⫽ { mantissa = r.div
, exponent = Integer/add x.exponent +1
}
else x
= stop.reduce_growth_noop
FloatBare
(λ(x : FloatBare) → stop.predicate_Natural x.mantissa)
FloatBare
dummyFloat.(FloatBare)
( λ(x : FloatBare) →
if Natural/isZero x.mantissa
then Float/zero.(FloatBare)
else if Natural/lessThan x.mantissa Base
then x
else let r = divmod x.mantissa Base

in if Natural/isZero r.rem
then x
⫽ { mantissa = r.div
, exponent = Integer/add x.exponent +1
}
else x
)

let _ = assert : normalizeStep Float/zero.(FloatBare) ≡ Float/zero.(FloatBare)

let _ = assert : normalizeStep (FloatBare/create -0 -1) ≡ Float/zero.(FloatBare)

let FloatBare/normalize
: FloatBare → FloatBare
= λ(args : FloatBare) →
Natural/fold (1 + args.mantissa) FloatBare normalizeStep args
= stop.reduce_growth_noop
FloatBare
(λ(x : FloatBare) → stop.predicate_Natural x.mantissa)
FloatBare
dummyFloat.(FloatBare)
( λ(args : FloatBare) →
Natural/fold (1 + args.mantissa) FloatBare normalizeStep args
)

let _ =
assert
Expand Down Expand Up @@ -143,57 +188,103 @@ let Float/isZero = λ(x : Float) → Natural/isZero x.mantissa

let Float/create
: Integer → Integer → Float
= λ(x : Integer) →
λ(exp : Integer) →
Float/addExtraData (FloatBare/normalize (FloatBare/create x exp))
= stop.reduce_growth
Integer
stop.predicate_Integer
(Integer → Float)
(λ(_ : Integer) → Float/zero)
( λ(x : Integer) →
stop.reduce_growth
Integer
stop.predicate_Integer
Float
Float/zero
( λ(exp : Integer) →
Float/addExtraData
(FloatBare/normalize (FloatBare/create x exp))
)
)

let _ = assert : Float/create +0 +0 ≡ Float/zero

let float2float_reduce =
λ(f : Float → Float) →
stop.reduce_growth
Float
(λ(x : Float) → stop.predicate_Natural x.mantissa)
Float
Float/zero
f

let float2float_reduce_noop =
λ(f : Float → Float) →
stop.reduce_growth_noop
Float
(λ(x : Float) → stop.predicate_Natural x.mantissa)
Float
Float/zero
f

let Float/normalize
: Float → Float
= stop.reduce_growth
Float
(λ(x : Float) → stop.predicate_Natural x.mantissa)
Float
Float/zero
= float2float_reduce
(λ(x : Float) → Float/addExtraData (FloatBare/normalize x.(FloatBare)))

let Float/pad
: Float → Natural → Float
= λ(x : Float) →
λ(padding : Natural) →
if Float/isZero x || Natural/isZero padding
then x
else let p = D.power Base padding

in x
⫽ { mantissa = x.mantissa * p
, topPower = x.topPower + padding
, exponent =
Integer/subtract (Natural/toInteger padding) x.exponent
, remaining = x.remaining * p
}
= stop.reduce_growth
Float
(λ(x : Float) → stop.predicate_Natural x.mantissa)
(Natural → Float)
(λ(_ : Natural) → Float/zero)
( λ(x : Float) →
stop.reduce_growth_noop
Natural
stop.predicate_Natural
Float
Float/zero
( λ(padding : Natural) →
if Float/isZero x || Natural/isZero padding
then x
else let p = power Base padding

in x
⫽ { mantissa = x.mantissa * p
, topPower = x.topPower + padding
, exponent =
Integer/subtract
(Natural/toInteger padding)
x.exponent
, remaining = x.remaining * p
}
)
)

let _ =
assert
: (Float/pad (Float/create +123 +0) 2).(FloatBare)
≡ FloatBare/create +12300 -2

let Float/negate =
λ(a : Float) →
if Float/isZero a
then a
else a
⫽ { mantissaPositive = if a.mantissaPositive then False else True
}
float2float_reduce
( λ(a : Float) →
if Float/isZero a
then a
else a
⫽ { mantissaPositive =
if a.mantissaPositive then False else True
}
)

let Float/abs
: Float → Float
= λ(x : Float) → x ⫽ { mantissaPositive = True }
= float2float_reduce (λ(x : Float) → x ⫽ { mantissaPositive = True })

in { Base
, Pair
, divmod
, log
, power
, Float
, FloatBare
, Float/abs
Expand Down
61 changes: 41 additions & 20 deletions tutorial/Float/add.dhall
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,6 @@ let T = ./Type.dhall

let Base = T.Base

let D = ./Arithmetic.dhall

let Pair = T.Pair

let S = ./show.dhall
Expand Down Expand Up @@ -70,14 +68,20 @@ let divmod = T.divmod
let clampDigits -- Make sure x has exactly prec digits. The value x_log_floor must be precomputed.
-- TODO add rounding to the clamping operation.
=
λ(x : Natural) →
λ(x_log_floor : Natural) →
λ(prec : Natural) →
let h = 1 + x_log_floor

in if Natural/lessThanEqual h prec
then x * D.power Base (Natural/subtract h prec)
else (divmod x (D.power Base (Natural/subtract prec h))).div
stop.reduce_growth
Natural
stop.predicate_Natural
Natural
0
( λ(x : Natural) →
let h = 1 + x_log_floor

in if Natural/lessThanEqual h prec
then x * T.power Base (Natural/subtract h prec)
else (divmod x (T.power Base (Natural/subtract prec h))).div
)

let totalUnderflow
-- Detect if `a` is negligible compared to `b` within given precision.
Expand All @@ -104,11 +108,28 @@ let flipTorsor
(λ(torsor : TorsorType) → torsor ⫽ { x = torsor.y, y = torsor.x })

let torsorXLessEqualY =
λ(torsor : TorsorType) → Natural/lessThanEqual torsor.x torsor.y

let Natural/plus = λ(a : Natural) → λ(b : Natural) → a + b

let Natural/minus = λ(a : Natural) → λ(b : Natural) → Natural/subtract b a
stop.reduce_growth
TorsorType
predicate_TorsorType
Bool
False
(λ(torsor : TorsorType) → Natural/lessThanEqual torsor.x torsor.y)

let Natural/plus =
stop.reduce_growth_noop
Natural
stop.predicate_Natural
(Natural → Natural)
(λ(_ : Natural) → 0)
(λ(a : Natural) → λ(b : Natural) → a + b)

let Natural/minus =
stop.reduce_growth_noop
Natural
stop.predicate_Natural
(Natural → Natural)
(λ(_ : Natural) → 0)
(λ(a : Natural) → λ(b : Natural) → Natural/subtract b a)

let addOrSubtractUnsignedAIsGreater
-- Compute a + b or a - b, assuming that a >= b > 0.
Expand Down Expand Up @@ -161,9 +182,9 @@ let addOrSubtractUnsignedAIsGreater

let bClamped =
clampDigits
b.mantissa
b.topPower
(Natural/subtract difference clampTo)
b.mantissa

let resultWithNewMantissaOnly =
aClamped
Expand Down Expand Up @@ -359,17 +380,17 @@ let Float/add
λ(prec : Natural) →
addFloatPair prec { _1 = a, _2 = b }

let _ = assert : clampDigits 123 (D.log 10 123) 0 ≡ 0
let _ = assert : clampDigits (T.log 10 123) 0 123 ≡ 0

let _ = assert : clampDigits 123 (D.log 10 123) 1 ≡ 1
let _ = assert : clampDigits (T.log 10 123) 1 123 ≡ 1

let _ = assert : clampDigits 123 (D.log 10 123) 2 ≡ 12
let _ = assert : clampDigits (T.log 10 123) 2 123 ≡ 12

let _ = assert : clampDigits 123 (D.log 10 123) 3 ≡ 123
let _ = assert : clampDigits (T.log 10 123) 3 123 ≡ 123

let _ = assert : clampDigits 123 (D.log 10 123) 4 ≡ 1230
let _ = assert : clampDigits (T.log 10 123) 4 123 ≡ 1230

let _ = assert : clampDigits 123 (D.log 10 123) 10 ≡ 1230000000
let _ = assert : clampDigits (T.log 10 123) 10 123 ≡ 1230000000

let mkTorsor =
λ(x : Float) →
Expand Down
Loading

0 comments on commit 24487e4

Please sign in to comment.