--- a/src/Pure/library.ML Sat Aug 06 18:06:56 2005 +0200
+++ b/src/Pure/library.ML Sun Aug 07 12:28:10 2005 +0200
@@ -144,6 +144,10 @@
type rat
exception RAT of string
val rep_rat: rat -> IntInf.int * IntInf.int
+ val ratge0: rat -> bool
+ val ratgt0: rat -> bool
+ val ratle: rat * rat -> bool
+ val ratlt: rat * rat -> bool
val ratadd: rat * rat -> rat
val ratmul: rat * rat -> rat
val ratinv: rat -> rat
@@ -151,6 +155,7 @@
val ratneg: rat -> rat
val rat_of_int: int -> rat
val rat_of_intinf: IntInf.int -> rat
+ val rat0: rat
(*strings*)
val nth_elem_string: int * string -> string
@@ -1224,6 +1229,7 @@
(** rational numbers **)
+(* Keep them normalized! *)
datatype rat = Rat of bool * IntInf.int * IntInf.int
@@ -1236,9 +1242,27 @@
val m = gcd(absp,q)
in Rat(a = (0 <= p), absp div m, q div m) end;
-fun ratadd(Rat(a,p,q),Rat(b,r,s)) =
+fun ratcommon(p,q,r,s) =
let val den = lcm(q,s)
- val p = p*(den div q) and r = r*(den div s)
+ in (p*(den div q), r*(den div s), den) end
+
+fun ratge0(Rat(a,p,q)) = a;
+fun ratgt0(Rat(a,p,q)) = a andalso p > 0;
+
+fun ratle(Rat(a,p,q),Rat(b,r,s)) =
+ not a andalso b orelse
+ a = b andalso
+ let val (p,r,_) = ratcommon(p,q,r,s)
+ in if a then p <= r else r <= p end
+
+fun ratlt(Rat(a,p,q),Rat(b,r,s)) =
+ not a andalso b orelse
+ a = b andalso
+ let val (p,r,_) = ratcommon(p,q,r,s)
+ in if a then p < r else r < p end
+
+fun ratadd(Rat(a,p,q),Rat(b,r,s)) =
+ let val (p,q,den) = ratcommon(p,q,r,s)
val num = (if a then p else ~p) + (if b then r else ~r)
in ratnorm(true,num,den) end;
@@ -1255,6 +1279,7 @@
fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
+val rat0 = rat_of_int 0;
(** misc **)