1 (* Title: Pure/General/rat.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, TU Muenchen |
|
4 |
|
5 Canonical implementation of exact rational numbers. |
|
6 *) |
|
7 |
|
8 signature RAT = |
|
9 sig |
|
10 type rat |
|
11 exception DIVZERO |
|
12 val zero: rat |
|
13 val one: rat |
|
14 val two: rat |
|
15 val rat_of_int: Intt.int -> rat |
|
16 val rat_of_quotient: Intt.int * Intt.int -> rat |
|
17 val quotient_of_rat: rat -> Intt.int * Intt.int |
|
18 val string_of_rat: rat -> string |
|
19 val eq: rat * rat -> bool |
|
20 val cmp: rat * rat -> order |
|
21 val le: rat -> rat -> bool |
|
22 val lt: rat -> rat -> bool |
|
23 val cmp_zero: rat -> order |
|
24 val add: rat -> rat -> rat |
|
25 val mult: rat -> rat -> rat |
|
26 val neg: rat -> rat |
|
27 val inv: rat -> rat |
|
28 val roundup: rat -> rat |
|
29 val rounddown: rat -> rat |
|
30 end; |
|
31 |
|
32 structure Rat : RAT = |
|
33 struct |
|
34 |
|
35 datatype rat = Rat of bool * Intt.int * Intt.int; |
|
36 |
|
37 exception DIVZERO; |
|
38 |
|
39 val zero = Rat (true, Intt.int 0, Intt.int 1); |
|
40 val one = Rat (true, Intt.int 1, Intt.int 1); |
|
41 val two = Rat (true, Intt.int 2, Intt.int 1); |
|
42 |
|
43 fun rat_of_int i = |
|
44 if i < Intt.int 0 |
|
45 then Rat (false, ~i, Intt.int 1) |
|
46 else Rat (true, i, Intt.int 1); |
|
47 |
|
48 fun norm (a, p, q) = |
|
49 if p = Intt.int 0 then Rat (true, Intt.int 0, Intt.int 1) |
|
50 else |
|
51 let |
|
52 val absp = abs p |
|
53 val m = gcd (absp, q) |
|
54 in Rat(a = (Intt.int 0 <= p), absp div m, q div m) end; |
|
55 |
|
56 fun common (p1, q1, p2, q2) = |
|
57 let val q' = lcm (q1, q2) |
|
58 in (p1 * (q' div q1), p2 * (q' div q2), q') end |
|
59 |
|
60 fun rat_of_quotient (p, q) = |
|
61 if q = Intt.int 0 then raise DIVZERO |
|
62 else norm (Intt.int 0 <= q, p, abs q); |
|
63 |
|
64 fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~p, q); |
|
65 |
|
66 fun string_of_rat r = |
|
67 let val (p, q) = quotient_of_rat r |
|
68 in Intt.string_of_int p ^ "/" ^ Intt.string_of_int q end; |
|
69 |
|
70 fun eq (Rat (false, _, _), Rat (true, _, _)) = false |
|
71 | eq (Rat (true, _, _), Rat (false, _, _)) = false |
|
72 | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2 |
|
73 |
|
74 fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS |
|
75 | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER |
|
76 | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) = |
|
77 let val (r1, r2, _) = common (p1, q1, p2, q2) |
|
78 in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end; |
|
79 |
|
80 fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end; |
|
81 fun lt a b = cmp (a, b) = LESS; |
|
82 |
|
83 fun cmp_zero (Rat (false, _, _)) = LESS |
|
84 | cmp_zero (Rat (_, 0, _)) = EQUAL |
|
85 | cmp_zero (Rat (_, _, _)) = GREATER; |
|
86 |
|
87 fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) = |
|
88 let |
|
89 val (r1, r2, den) = common (p1, q1, p2, q2) |
|
90 val num = (if a1 then r1 else ~r1) + (if a2 then r2 else ~r2) |
|
91 in norm (true, num, den) end; |
|
92 |
|
93 fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) = |
|
94 norm (a1=a2, p1*p2, q1*q2); |
|
95 |
|
96 fun neg (r as Rat (b, p, q)) = |
|
97 if p = Intt.int 0 then r |
|
98 else Rat (not b, p, q); |
|
99 |
|
100 fun inv (Rat (a, p, q)) = |
|
101 if p = Intt.int 0 then raise DIVZERO |
|
102 else Rat (a, q, p); |
|
103 |
|
104 fun roundup (r as Rat (a, p, q)) = |
|
105 if q = Intt.int 1 then r |
|
106 else |
|
107 let |
|
108 fun round true q = Rat (true, q + Intt.int 1, Intt.int 1) |
|
109 | round false q = |
|
110 if q = Intt.int 0 |
|
111 then Rat (true, Intt.int 0, Intt.int 1) |
|
112 else Rat (false, q, Intt.int 1); |
|
113 in round a (p div q) end; |
|
114 |
|
115 fun rounddown (r as Rat (a, p, q)) = |
|
116 if q = Intt.int 1 then r |
|
117 else |
|
118 let |
|
119 fun round true q = Rat (true, q, Intt.int 1) |
|
120 | round false q = Rat (false, q + Intt.int 1, Intt.int 1) |
|
121 in round a (p div q) end; |
|
122 |
|
123 end; |
|
124 |
|
125 infix 5 +/; |
|
126 infix 5 -/; |
|
127 infix 7 */; |
|
128 infix 7 //; |
|
129 infix 4 =/ </ <=/ >/ >=/ <>/; |
|
130 |
|
131 fun a +/ b = Rat.add a b; |
|
132 fun a -/ b = a +/ Rat.neg b; |
|
133 fun a */ b = Rat.mult a b; |
|
134 fun a // b = a */ Rat.inv b; |
|
135 fun a =/ b = Rat.eq (a,b); |
|
136 fun a </ b = Rat.lt a b; |
|
137 fun a <=/ b = Rat.le a b; |
|
138 fun a >/ b = b </ a; |
|
139 fun a >=/ b = b <=/ a; |
|
140 fun a <>/ b = not (a =/ b); |
|