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