(*************************************************** 
 ** RoundDownFilteredRational.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.
 ** 
 ** The difference from the RoundDownLazyRational
 ** is in the way the history of a number is stored.
 ** This file has a a datatype defining expressions,
 ** while RoundDownLazyRational stores the history
 ** as a closure. The conjecture is that the closure
 ** approach is more efficient on accesses, but more
 ** expensive on creations.  Experiments have not been
 ** taken to establish this yet.
 ****************************************************)


structure RoundDownFilteredRational :> RATIONAL = 
struct
    structure Q = NormalizedRational
    structure I = RoundDownFloatInterval

    (* interval field is always filled;  *)
    (* exact may not have a value *)

    datatype history = 
	Float of real
      | Rat of Q.rat
      | Plus of rat * rat 
      | Minus of rat * rat
      | Times of rat * rat
      | Div of rat * rat
      | UMinus of rat
      | Inv of rat
      | Abs of rat
      | Max of rat * rat
      | Min of rat * rat 
    withtype rat = {approx:I.interval, exact: Q.rat option, history:history} ref

    type t = rat

    val zero = ref {approx=I.zero,
		    exact=SOME Q.zero,
		    history=Rat Q.zero}

    val one = ref {approx=I.one,
		   exact=SOME Q.one,
		   history=Rat Q.one}

    fun fromIntFrac a =
	let val z = Q.fromIntFrac a 
	in
	    ref {approx=I.fromBounds(Q.intervalApprox z),
		 exact=SOME z,
		 history=Rat z}
	end


    fun fromFrac a =
	let val z = Q.fromFrac a 
	in
	    ref {approx=I.fromBounds(Q.intervalApprox z),
		 exact=SOME z,
		 history=Rat z}
	end

    fun fromInt x =
	let val z = Q.fromInt x
	in
	    ref {approx=I.fromNumber(Real.fromInt x),
		 exact = SOME z,
		 history = Rat z}
	end

    fun fromIntInf x =
	let val z = Q.fromIntInf x
	in
	    ref {approx=I.fromBounds(Q.intervalApprox z),
		 exact = SOME z,
		 history = Rat z}
	end


    fun fromManExp x =
	let val z = Q.fromManExp x
	in
	    ref {approx=I.fromBounds(Q.intervalApprox z),
		 exact = SOME z,
		 history = Rat z}
	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 {approx = I.fromNumber x, 
		      exact = NONE,
		      history = Float x}


    fun eval (xx as (ref x)) = 
	case (#history x) of
	    Float xv =>
		(case #exact x of
		     NONE =>
			let val xe = Q.fromReal xv
			in
			    xx before
			    xx := {approx = #approx x,
				   exact = SOME xe,
				   history = Float xv}
			end
		  | SOME _ => xx)
	  | Rat _ => xx
	  | Plus(xv, yv) => 
		let val (ref x, ref y) = (eval xv, eval yv)
		    val ze = Q.+(valOf (#exact x), valOf (#exact y))
		in
		    xx before
		    xx := {approx = I.fromBounds(Q.intervalApprox ze),
			   exact = SOME ze,
			   history = Rat ze}
		end
	  | Minus(xv, yv) =>
		let val (ref x, ref y) = (eval xv, eval yv)
		    val ze = Q.-(valOf (#exact x), valOf (#exact y))
		in
		    xx before
		    xx := {approx = I.fromBounds(Q.intervalApprox ze),
			   exact = SOME ze,
			   history = Rat ze}
		end
	  | Times(xv, yv) =>
 		let val (ref x, ref y) = (eval xv, eval yv)
		    val ze = Q.*(valOf (#exact x), valOf (#exact y))
		in
		    xx before
		    xx := {approx = I.fromBounds(Q.intervalApprox ze),
			   exact = SOME ze,
			   history = Rat ze}
		end
	  | Div(xv, yv) => 
		let val (ref x, ref y) = (eval xv, eval yv)
		    val ze = Q./(valOf (#exact x), valOf (#exact y))
		in
		    xx before
		    xx := {approx = I.fromBounds(Q.intervalApprox ze),
			   exact = SOME ze,
			   history = Rat ze}
		end
	  | Max(xv, yv) => 
		let val (ref x, ref y) = (eval xv, eval yv)
		    val ze = Q.max(valOf (#exact x), valOf (#exact y))
		in
		    xx before
		    xx := {approx = I.fromBounds(Q.intervalApprox ze),
			   exact = SOME ze,
			   history = Rat ze}
		end
	  | Min(xv, yv) => 
		let val (ref x, ref y) = (eval xv, eval yv)
		    val ze = Q.min(valOf (#exact x), valOf (#exact y))
		in
		    xx before
		    xx := {approx = I.fromBounds(Q.intervalApprox ze),
			   exact = SOME ze,
			   history = Rat ze}
		end
	  | UMinus xv =>
		let val (ref {approx=xa, exact=SOME xe, ...}) = eval xv
		    val ze = Q.~ xe
		in
		    xx before
		    xx := {approx=I.~ xa, exact=SOME ze, history=Rat ze}
		end
	  | Inv xv =>
		let val (ref {exact=SOME xe,...}) = eval xv
		    val ze = Q.inv xe
		in
		    xx before
		    xx := {approx = I.fromBounds(Q.intervalApprox ze),
			   exact = SOME ze,
			   history = Rat ze}
		end
	  | Abs xv => 
		let val (ref {exact=SOME xe, ...}) = eval xv
		    val ze = Q.abs xe
		in
		    xx before
		    xx := {approx = I.fromBounds(Q.intervalApprox ze),
			   exact = SOME ze,
			   history = Rat ze}
		end

	    

    fun filteredTest (approxTest, exactTest) =
	fn (xx as ref x, yy as ref y) =>
	let val (xi, yi) = (#approx x, #approx y)
	in
	    if approxTest(xi, yi) then true
	    else
		case (#history x, #history y) of
		    (Float _, Float _) => false (* should have passed before *)
		  | (Rat _, Float _) => 
			let val yv = (case (#exact y) of 
					  NONE => valOf (#exact(!(eval yy)))
					| SOME yv => yv)
			in
			    exactTest (valOf (#exact x), yv)
			end
		  | (Rat _, Rat _) => 
			exactTest (valOf (#exact x), valOf (#exact y))
		  | (Rat _, _) => 
		        let val (ref y) = eval yy
			in
			    exactTest (valOf (#exact x), valOf (#exact y))
			end
		  | (Float _, Rat _) =>
			let val xv = (case (#exact x) of
					  NONE => valOf (#exact(!(eval xx)))
					| SOME xv => xv)
			in
			    exactTest (xv, valOf (#exact y))
			end
		  | (_, Rat _) => 
		        let val (ref x) = eval xx
			in 
			    exactTest (valOf (#exact x), valOf (#exact y))
			end
		  | (_, _) => 
		        let val (ref x, ref y) = (eval xx, eval yy)
			in
			    approxTest(#approx x, #approx y) orelse
			    exactTest (valOf (#exact x), valOf (#exact y))
			end
	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.>=)

	

    fun op + (xx as ref x, yy as ref y) = 
	ref {approx=I.+(#approx x, #approx y),
	     exact=NONE,
	     history=Plus(xx, yy)}


    fun op - (xx as ref x, yy as ref y) = 
	ref {approx=I.-(#approx x, #approx y),
	     exact=NONE,
	     history=Minus(xx, yy)}
	
    fun op * (xx as ref x, yy as ref y) = 
	ref {approx=I.*(#approx x, #approx y),
	     exact=NONE,
	     history=Times(xx, yy)}

    fun op / (xx as ref x, yy as ref y) = 
	ref {approx=I./(#approx x, #approx y),
	     exact=NONE,
	     history=Div(xx, yy)}

    fun op ~ (xx as ref x) = 
	ref {approx=I.~(#approx x),
	     exact=NONE,
	     history=UMinus xx}
	

    fun op inv (xx as ref x) =
	ref {approx=I.inv (#approx x),
	     exact=NONE,
	     history=Inv xx}


    fun sign (xx as ref x) =
	let val s = I.sign (#approx x) handle Domain => 0
	in
	    if (s <> 0) then s
	    else
		let val (ref x) = eval xx
		    val s = I.sign (#approx x) (* can't go NaN here, so no need for handle *)
		in
		    if (s <> 0) then s
		    else
			let val (SOME xe) = #exact x
			in
			    Q.sign xe
			end
		end
	end


    fun abs (xx as ref x) =
	ref {approx=I.threadAbs(#approx x),
	     exact=NONE,
	     history=Abs xx}


    fun min (xx as ref x, yy as ref y) =
	ref {approx=I.inf(#approx x, #approx y),
	     exact=NONE,
	     history=Min(xx, yy)}


    fun max (xx as ref x, yy as ref y) =
	ref {approx=I.sup(#approx x, #approx y),
	     exact=NONE,
	     history=Max(xx, yy)}


    fun inv (xx as ref x) =
	ref {approx=I.inv (#approx x),
	     exact=NONE,
	     history=Inv xx}


    fun compare (xx as ref x, yy as ref y) =
	let val (xi, yi) = (#approx x, #approx y)
	in
	    if I.<<(xi, yi) then LESS
	    else if I.>>(xi, yi) then GREATER 
		 else
		     let val (ref x, ref y) = (eval xx, eval yy)
			 val (xi, yi) = (#approx x, #approx y)
		     in 
			 if I.<<(xi, yi) then LESS
			 else if I.>>(xi, yi) then GREATER
			      else
				  let val (SOME xe, SOME ye) = (#exact x, #exact y)
				  in
				      Q.compare (xe, ye)
				  end
		     end
	end	


    fun approx rm (xx as ref x) =
	case (#history x) of
	    Float xv => xv
	  | _ =>
		let val (ref x) = eval xx
		    val (SOME xe) = #exact x
		in
		    Q.approx rm xe
		end


    fun intervalApprox (xx as ref x) =
	case (#history x) of
	    Float xv => {lo=xv, hi=xv}
	  | Rat xv => (I.toBounds (#approx x))
	  | _ => 
		let val (ref x) = eval xx
		in
		    I.toBounds (#approx x)
		end




    fun toFrac (xx as ref x) =
	let val (ref {exact=SOME xe,...}) = eval xx
	in
	    Q.toFrac xe
	end


    fun toString (xx as ref x) =
	let val (ref {exact=SOME xe,...}) = eval xx
	in
	    Q.toString xe
	end

end