Added rational numbers #711

Closed
zxq9 wants to merge 28 commits from github/fork/radrow/frac into lima
Showing only changes of commit 12377f23e3 - Show all commits

View File

@ -7,6 +7,7 @@ namespace Frac =
datatype frac = Pos(int, int) | Zero | Neg(int, int) datatype frac = Pos(int, int) | Zero | Neg(int, int)
// Checks if internal representation is correct. Numerator and denominator must be positive.
function is_sane(f : frac) : bool = switch(f) function is_sane(f : frac) : bool = switch(f)
Pos(n, d) => n > 0 && d > 0 Pos(n, d) => n > 0 && d > 0
Zero => true Zero => true
@ -37,6 +38,7 @@ namespace Frac =
Neg(n, d) => String.concat("-", to_str(Pos(n, d))) Neg(n, d) => String.concat("-", to_str(Pos(n, d)))
Zero => "0" Zero => "0"
// Reduce fraction to normal form
function simplify(f : frac) : frac = function simplify(f : frac) : frac =
switch(f) switch(f)
Neg(n, d) => Neg(n, d) =>
@ -47,7 +49,7 @@ namespace Frac =
let cd = gcd(n, d) let cd = gcd(n, d)
Pos(n / cd, d / cd) Pos(n / cd, d / cd)
function make_frac(n : int, d : int): frac = function make_frac(n : int, d : int) : frac =
if (d == 0) abort("Division by zero") if (d == 0) abort("Division by zero")
elif (n == 0) Zero elif (n == 0) Zero
elif ((n < 0) == (d < 0)) simplify(Pos(abs_int(n), abs_int(d))) elif ((n < 0) == (d < 0)) simplify(Pos(abs_int(n), abs_int(d)))
@ -109,6 +111,7 @@ namespace Frac =
Zero => 0 Zero => 0
Neg(n, d) => -(n + d - 1) / d Neg(n, d) => -(n + d - 1) / d
// Round towards nearest integer. If two integers are in the same distance, choose the even one.
function round(f : frac) : int = function round(f : frac) : int =
let fl = floor(f) let fl = floor(f)
let cl = ceil(f) let cl = ceil(f)
@ -154,3 +157,15 @@ namespace Frac =
let half = int_exp_(b, e / 2) let half = int_exp_(b, e / 2)
if (e mod 2 == 1) mul(mul(half, half), b) if (e mod 2 == 1) mul(mul(half, half), b)
else mul(half, half) else mul(half, half)
// Reduces the fraction's in-memory size by dividing its components by two until the
// the error is bigger than `loss` value
function optimize(f : frac, loss : frac) : frac =
require(geq(loss, Zero), "negative loss optimize")
let s = sign(f)
mul(from_int(s), run_optimize(abs(f), loss))
private function run_optimize(f : frac, loss : frac) : frac =
let t = make_frac((num(f) + 1) / 2, (den(f) + 1)/2)
if(gt(abs(sub(t, f)), loss)) f
elif (eq(t, f)) f
else run_optimize(t, loss)