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