Skip to content

Commit

Permalink
separate test files
Browse files Browse the repository at this point in the history
  • Loading branch information
@winitzki
winitzki committed Oct 20, 2024
1 parent 2fd2455 commit fa40942
Show file tree
Hide file tree
Showing 13 changed files with 540 additions and 410 deletions.
10 changes: 5 additions & 5 deletions tutorial/Float/Type.dhall
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,9 +42,9 @@ let Float/mantissa = λ(a : Float) → a.mantissa

let Float/exponent = λ(a : Float) → a.exponent

let D = ./Numerics.dhall
let N = ./numerics.dhall

let Result = D.Result
let Result = N.Result

let divmod
: Natural → Natural → Result
Expand All @@ -53,7 +53,7 @@ let divmod
stop.predicate_Natural
(Natural → Result)
(λ(_ : Natural) → { div = 0, rem = 0 })
D.divrem
N.divrem

let log
: Natural → Natural → Natural
Expand All @@ -62,7 +62,7 @@ let log
stop.predicate_Natural
(Natural → Natural)
(λ(_ : Natural) → 0)
D.log
N.log

let power
: Natural → Natural → Natural
Expand All @@ -71,7 +71,7 @@ let power
stop.predicate_Natural
(Natural → Natural)
(λ(_ : Natural) → 0)
D.power
N.power

let dummyFloat =
{ mantissa = 0
Expand Down
124 changes: 17 additions & 107 deletions tutorial/Float/add.dhall
View file
Original file line number Diff line number Diff line change
Expand Up @@ -502,7 +502,9 @@ let _ = assert : checkTotalUnderflow +1 +0 +123456789 +6 14 ≡ False

let _ = assert : checkTotalUnderflow +1 +0 +123456789 +6 15 ≡ False

let unsigned =
let unsigned
-- Adding numbers without underflow check, which forces rounding.
=
λ(x : Integer) →
λ(ex : Integer) →
λ(y : Integer) →
Expand All @@ -516,48 +518,7 @@ let unsigned =
prec
)

let _ = assert : unsigned +321 +0 +123 +0 10 ≡ Float/create +444 +0

let _ = assert : unsigned +32154 +0 +12345 +0 10 ≡ Float/create +44499 +0

let _ = assert : unsigned +321 +2 +12345 +0 10 ≡ Float/create +44445 +0

let _ = assert : unsigned +321 +2 +12345 +0 3 ≡ Float/create +4444 +1

let _ = assert : unsigned +321 +2 +12345 +0 2 ≡ Float/create +444 +2

let _ = assert : unsigned +321 +2 +12345 +0 1 ≡ Float/create +44 +3

let _ = assert : unsigned +321 +2 +12345 +0 0 ≡ Float/create +4 +4

let _ = assert : unsigned +321 -20 +12345 -22 3 ≡ Float/create +4444 -21

let _ = assert : unsigned +321 +20 +12345 +18 3 ≡ Float/create +4444 +19

let _ = assert : unsigned +123456789000000 +0 +1 +0 3 ≡ Float/create +1235 +11

let _ = assert : unsigned +123456789000000 +0 +1 +0 4 ≡ Float/create +12346 +10

let _ = assert : unsigned +123456789 +6 +1 +0 4 ≡ Float/create +12346 +10

let checkAdd =
λ(x : Integer) →
λ(ex : Integer) →
λ(y : Integer) →
λ(ey : Integer) →
λ(prec : Natural) →
Float/add (Float/create x ex) (Float/create y ey) prec

let checkAddShow =
λ(x : Integer) →
λ(ex : Integer) →
λ(y : Integer) →
λ(ey : Integer) →
λ(prec : Natural) →
λ(expected : Text) →
Float/show (checkAdd x ex y ey prec) ≡ expected

let _ = assert : checkAdd +321 +0 +123 +0 10 ≡ Float/create +444 +0
let _ = assert : unsigned +123456789 +0 +1 +0 10 ≡ Float/create +123456790 +0

let _ = assert : unsigned +123456789 +0 +1 +0 5 ≡ Float/create +123457 +3

Expand All @@ -569,85 +530,34 @@ let _ = assert : unsigned +123456789 +0 +1 +0 8 ≡ Float/create +123456790 +0

let _ = assert : unsigned +123456789 +0 +1 +0 9 ≡ Float/create +123456790 +0

let _ = assert : unsigned +123456789 +0 +1 +0 10 ≡ Float/create +123456790 +0
let _ = assert : unsigned +123456789 +6 +1 +0 4 ≡ Float/create +12346 +10

let _ = assert : unsigned +1234567890 +0 +9 +0 10 ≡ Float/create +1234567899 +0

let _ = assert : unsigned +1234567890 +0 +9 +0 9 ≡ Float/create +1234567899 +0

let _ = assert : unsigned +1234567890 +0 +9 +0 8 ≡ Float/create +1234567890 +0

let _ = assert : checkAdd +1234567890 +0 +9 +0 8 ≡ Float/create +1234567890 +0

let _ = assert : checkAdd +1234567890 +0 +9 +0 9 ≡ Float/create +1234567890 +0

let _ = assert : checkAdd +1234567890 +0 +9 +0 10 ≡ Float/create +1234567899 +0

let _ = assert : checkAdd +123456789 +6 +1 +0 5 ≡ Float/create +123456789 +6

let _ = assert : checkAdd +123456789 +6 +1 +0 10 ≡ Float/create +123456789 +6

let _ = assert : checkAddShow +123456789 +6 +1 +0 10 "+1.23456789e+14"

let _ = assert : checkAddShow +1 +0 +123456789 +6 10 "+1.23456789e+14"

let _ = assert : checkAddShow +123456789 +0 -123456789 +0 10 "0."

let _ = assert : checkAddShow +0 +0 -2 +0 10 "-2."

let _ = assert : checkAddShow -2 +0 +0 +0 10 "-2."

let _ = assert : checkAddShow +3 +0 -2 +0 10 "+1."

let _ = assert : checkAddShow -2 +0 +3 +0 10 "+1."

let _ = assert : checkAddShow -3 +0 +2 +0 10 "-1."

let _ = assert : checkAddShow +1 +0 -2 +0 10 "-1."

let _ = assert : checkAddShow -2 +0 +1 +0 10 "-1."

let _ = assert : checkAddShow +20 +0 -1 +0 10 "+19."

let _ = assert : checkAddShow -1 +0 +20 +0 10 "+19."

let _ = assert : checkAddShow -20 +0 +1 +0 10 "-19."

let _ = assert : checkAddShow +1 +0 -20 +0 10 "-19."

let _ = assert : checkAddShow +1234 +0 -1 +0 10 "+1233."

let _ = assert : checkAddShow +1234 +0 -12 +0 10 "+1222."

let _ = assert : checkAddShow +12 +0 -1234 +0 10 "-1222."

let _ = assert : checkAddShow +1234 +0 -123 +0 10 "+1111."

let _ =
let a1 = Float/create -12345678 -8

let a2 = Float/create +123 -2
let _ = assert : unsigned +1234567890 +0 +9 +0 9 ≡ Float/create +1234567899 +0

let _ = assert : Float/show a1 ≡ "-0.12345678"
let _ = assert : unsigned +123456789000000 +0 +1 +0 3 ≡ Float/create +1235 +11

let _ = assert : Float/show a2 ≡ "+1.23"
let _ = assert : unsigned +123456789000000 +0 +1 +0 4 ≡ Float/create +12346 +10

in True
let _ = assert : unsigned +321 +0 +123 +0 10 ≡ Float/create +444 +0

let _ = assert : checkAddShow +12345678 -8 +123 -2 5 "+1.35345"
let _ = assert : unsigned +321 +2 +12345 +0 0 ≡ Float/create +4 +4

let _ = assert : checkAddShow +12345678 -8 +123 -2 6 "+1.353456"
let _ = assert : unsigned +321 +2 +12345 +0 1 ≡ Float/create +44 +3

let _ = assert : checkAddShow +12345678 -8 +123 -2 7 "+1.3534567"
let _ = assert : unsigned +321 +2 +12345 +0 10 ≡ Float/create +44445 +0

let _ = assert : checkAddShow +12345678 -8 +123 -2 8 "+1.35345678"
let _ = assert : unsigned +321 +2 +12345 +0 2 ≡ Float/create +444 +2

let _ = assert : checkAddShow +12345678 -8 +123 -2 9 "+1.35345678"
let _ = assert : unsigned +321 +2 +12345 +0 3 ≡ Float/create +4444 +1

let _ = assert : checkAddShow -123 -3 +12 -1 10 "+1.077"
let _ = assert : unsigned +321 +20 +12345 +18 3 ≡ Float/create +4444 +19

let _ = assert : checkAddShow -12345678 -8 +123 -2 5 "+1.10655"
let _ = assert : unsigned +321 -20 +12345 -22 3 ≡ Float/create +4444 -21

let _ = assert : checkAddShow -12345678 -8 +123 -2 9 "+1.10654322"
let _ = assert : unsigned +32154 +0 +12345 +0 10 ≡ Float/create +44499 +0

in Float/add
40 changes: 0 additions & 40 deletions tutorial/Float/compare.dhall
View file
Original file line number Diff line number Diff line change
Expand Up @@ -210,46 +210,6 @@ let Float/compare
}
maybeQuickCompare

let _ =
assert
: Float/compare (Float/create +123 +0) (Float/create +12 +1)
≡ Compared.Greater

let _ =
assert
: Float/compare (Float/create +123 +0) (Float/create +12 +2)
≡ Compared.Less

let _ =
assert
: Float/compare (Float/create +120 +0) (Float/create +12 +1)
≡ Compared.Equal

let _ =
assert
: Float/compare (Float/create +123 -100) (Float/create +12 -99)
≡ Compared.Greater

let _ =
assert
: Float/compare (Float/create +123 -100) (Float/create +12 -98)
≡ Compared.Less

let _ =
assert
: Float/compare (Float/create +120 -100) (Float/create +12 -99)
≡ Compared.Equal

let _ =
assert
: Float/compare (Float/create +120 -100) (Float/create -12 -99)
≡ Compared.Greater

let _ =
assert
: Float/compare (Float/create -120 -100) (Float/create +12 -99)
≡ Compared.Less

let zeroTorsor = { x = 0, y = 0 }

let computeTorsor
Expand Down
75 changes: 0 additions & 75 deletions tutorial/Float/divide.dhall
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,79 +46,4 @@ let Float/divide
(Float/create (mantissaApplySign mantissaUnsigned) exponent)
prec

let Float/show = ./show.dhall

let check =
λ(a : Integer) →
λ(ae : Integer) →
λ(b : Integer) →
λ(be : Integer) →
λ(prec : Natural) →
λ(expected : Text) →
Float/show (Float/divide (Float/create a ae) (Float/create b be) prec)
≡ expected

let _ = assert : check +123456 +0 +123456 +0 4 "+1."

let _ = assert : check +123456 +0 +123 +0 2 "+1000."

let _ = assert : check +123456 +0 +123 +0 10 "+1003.707317"

let _ = assert : check +1 +0 +3 +0 10 "+0.3333333333"

let _ = assert : check +1 +10 +3 +0 3 "+3.33e+9"

let _ = assert : check -1 +10 +3 +0 2 "-3.3e+9"

let _ = assert : check -1 +10 -3 +0 2 "+3.3e+9"

let _ = assert : check +1 +10 -3 +0 2 "-3.3e+9"

let _ = assert : check +1 -10 -3 +0 2 "-3.3e-11"

let _ = assert : check +1 +0 +3 +10 2 "+3.3e-11"

let _ = assert : check +1 +0 -3 -10000 2 "-3.3e+9999"

let _ = assert : check +1 +100000 -3 -100000 2 "-3.3e+199999"

let _ = assert : check +1 +100000 -3 +100000 2 "-0.33"

let _
-- Should not be slow even when exponents are very large.
=
let power = +1000000000000000000000000000000000000

in assert : check +1 power -3 power 2 "-0.33"

let _
-- Should not be slow even when exponents are very large.
=
let power = +1000000000000000000000000000000000000

in assert
: check
+1
(Integer/negate power)
-3
(Integer/subtract +1 power)
2
"-3.3e-${Natural/show (Integer/clamp power * 2)}"

let _
-- Should not be slow even when exponents are very large.
=
let power = +1000000000000000000000000000000000000

in assert
: check
+1
power
-3
(Integer/subtract +1 (Integer/negate power))
2
"-3.3e+${Natural/show (Integer/clamp power * 2)}"

let _ = assert : check +1 +0 +239 +0 20 "+0.004184100418410041841"

in Float/divide
Loading

0 comments on commit fa40942

Please sign in to comment.