(***************************************************
** RoundDownLazyRational.sml
** sml
**
** Aleksandar Nanevski
**
** A rational value is equipped with an
** approximating interval, and a history.
** This way the exact computation is carried
** only when the predicates cannot compute their
** result from the approximating interval.
**
** WARNING: requres round-to-neginf
**
** TODO:
** - the name of this structure should be changed
** into something normal.
****************************************************)
structure RoundDownLazyRational :> RATIONAL =
struct
structure Q = NormalizedRational
structure I = RoundDownFloatInterval
type rat = (I.interval * (unit -> Q.rat)) ref
type t = rat
fun force (aa as ref (_, a2)) =
let val c = a2()
in
(#1 (!aa), c)
end
(* arithmetic *)
val zero = ref (I.zero, fn () => Q.zero)
val one = ref (I.one, fn () => Q.one)
fun unop (approx, exact) =
let val init = (I.zero, fn () => raise Domain)
in
fn (ref (a1, a2)) =>
let val x = ref init
in
x before
x := (approx a1,
fn () => let val c = exact (a2())
in
c before
x := (I.fromBounds (Q.intervalApprox c), fn () => c)
end)
end
end
fun binop (approx, exact) =
let val init = (I.zero, fn () => raise Domain)
in
fn (ref (a1, a2), ref (b1, b2)) =>
let val x = ref init
in
x before
x := (approx(a1, b1),
fn () => let val c = exact(a2(), b2())
in
c before
x := (I.fromBounds (Q.intervalApprox c), fn () => c)
end)
end
end
val op + = binop(I.+, Q.+)
val op - = binop(I.-, Q.-)
val op * = binop(I.*, Q.* )
val op / = binop(I./, Q./)
val op inv = unop(I.inv, Q.inv)
val op ~ = unop(I.~, Q.~)
val abs = unop(I.threadAbs, Q.abs)
(* total ordering *)
fun filteredTest (approxTest, exactTest) =
fn (aa as ref (a1, a2), bb as ref (b1, b2)) =>
approxTest(a1, b1) orelse
let val (a1, a2) = force aa
val (b1, b2) = force bb
in
approxTest(a1, b1) orelse exactTest(a2, b2)
end
val op != = filteredTest (I.disjoint, Q.!=)
val op == = not o (op !=)
val op < = filteredTest (I.<<, Q.<)
val op <= = filteredTest (I.<<, Q.<=)
val op > = filteredTest (I.>>, Q.>)
val op >= = filteredTest (I.>>, Q.>=)
val min = binop(I.inf, Q.min)
val max = binop(I.sup, Q.max)
fun compare (aa as ref(a1, a2), bb as ref (b1, b2)) =
if I.<<(a1, b1) then LESS
else if I.>>(a1, b1) then GREATER
else if ((I.singleton a1) andalso
(I.==(a1, b1)) andalso (I.isFinite a1)) then EQUAL
else
let val (a1, a2) = force aa
val (b1, b2) = force bb
in
if I.<<(a1, b1) then LESS
else if I.>>(a1, b1) then GREATER
else if ((I.singleton a1) andalso
(I.==(a1, b1)) andalso (I.isFinite a1)) then EQUAL
else
Q.compare (a2, b2)
end
fun sign (aa as ref(a1, a2)) =
(I.sign a1) handle _ => Q.sign (a2())
(* coercions *)
fun fromInt a =
let val c = Q.fromInt a
in
ref (I.fromNumber(Real.fromInt a), fn _ => c)
end
fun fromIntInf a =
let val c = Q.fromIntInf a
in
ref (I.fromBounds(Q.intervalApprox c), fn _ => c)
end
fun fromIntFrac a =
let val c = Q.fromIntFrac a
in
ref (I.fromBounds(Q.intervalApprox c), fn _ => c)
end
fun fromFrac a =
let val c = Q.fromFrac a
in
ref (I.fromBounds(Q.intervalApprox c), fn _ => c)
end
fun fromManExp a =
let val c = Q.fromManExp a
in
ref (I.fromBounds(Q.intervalApprox c), fn _ => c)
end
fun fromReal x =
if (Real.isNan x) then raise Domain
else if (Real.==(x, Real.posInf) orelse
Real.==(x, Real.negInf)) then raise Overflow
else
ref (I.fromNumber x, fn _ => Q.fromReal x)
fun toFrac (ref (a1, a2)) = Q.toFrac (a2())
fun toString (ref (a1, a2)) = Q.toString (a2())
fun approx rm (ref (a1, a2)) = Q.approx rm (a2())
fun intervalApprox aa =
let val (a1, _) = force aa
in
I.toBounds a1
end
end