(*************************************************** ** 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