1structure Arbrat :> Arbrat = 2struct 3 4(* representation is a reduced pair of int and num *) 5 6type num = Arbnum.num 7type aint = Arbint.int 8type rat = aint * num 9 10fun norm (n,d) = 11 let 12 val n' = Arbint.toNat (Arbint.abs n) 13 val g = Arbnum.gcd(n',d) 14 in 15 if g = Arbnum.one 16 then (n,d) 17 else (Arbint.div (n, Arbint.fromNat g), Arbnum.div (d, g)) 18 end 19 20fun fromAInt i = (i, Arbnum.one) 21fun fromNat n = fromAInt (Arbint.fromNat n) 22fun fromInt i = fromAInt (Arbint.fromInt i) 23 24val zero = fromInt 0 25val one = fromInt 1 26val two = fromInt 2 27 28fun numerator (n, d) = n 29fun denominator (n, d) = d 30 31fun toString (n, d) = Arbint.toString n ^ "/" ^ Arbnum.toString d 32fun fromString s = fromAInt (Arbint.fromString s) 33 34fun toAInt (n, d) = 35 if d = Arbnum.one then n else raise Fail "Arbrat.toAInt: not integral" 36 37fun toInt r = Arbint.toInt (toAInt r) 38fun toNat r = Arbint.toNat (toAInt r) 39 40fun (n1, d1) + (n2, d2) = 41 norm (Arbint.+ (Arbint.* (n1, Arbint.fromNat d2), 42 Arbint.* (n2, Arbint.fromNat d1)), 43 Arbnum.* (d1, d2)) 44 45fun (n1, d1) * (n2, d2) = norm (Arbint.* (n1, n2), Arbnum.* (d1, d2)) 46 47fun ~(n, d) = (Arbint.~ n, d) 48 49val negate = ~ 50 51fun inv (n, d) = 52 if n = Arbint.zero 53 then raise Fail "inv: arg = 0" 54 else (if Arbint.< (n, Arbint.zero) 55 then Arbint.~ (Arbint.fromNat d) 56 else Arbint.fromNat d, 57 Arbint.toNat (Arbint.abs n)) 58 59fun r1 - r2 = r1 + ~r2 60fun r1 / r2 = r1 * inv r2 61 62fun abs(n, d) = (Arbint.abs n, d) 63 64fun (n1, d1) < (n2, d2) = 65 Arbint.< (Arbint.* (n1, Arbint.fromNat d2), Arbint.* (n2, Arbint.fromNat d1)) 66 67fun r1 <= r2 = r1 < r2 orelse r1 = r2 68fun r1 > r2 = r2 < r1 69fun r1 >= r2 = r2 <= r1 70 71fun floor (n, d) = 72 let 73 val di = Arbint.fromNat d 74 open Arbint 75 in 76 if di = one 77 then n 78 else if n < zero 79 then ~(abs(n) div di + one) 80 else n div di 81 end 82 83fun ceil r = Arbint.~ (floor (~r)) 84 85fun compare (r1, r2) = 86 if r1 = r2 then EQUAL else if r1 < r2 then LESS else GREATER 87 88fun min(r1, r2) = if r1 < r2 then r1 else r2 89fun max(r1, r2) = if r1 > r2 then r1 else r2 90 91fun pp_rat r = HOLPP.add_string (toString r) 92 93end 94