|
1 (* Title: Pure/General/rat.ML |
|
2 Author: Tobias Nipkow, Florian Haftmann, TU Muenchen |
|
3 |
|
4 Canonical implementation of exact rational numbers. |
|
5 *) |
|
6 |
|
7 signature RAT = |
|
8 sig |
|
9 eqtype rat |
|
10 exception DIVZERO |
|
11 val zero: rat |
|
12 val one: rat |
|
13 val two: rat |
|
14 val rat_of_int: int -> rat |
|
15 val rat_of_quotient: int * int -> rat |
|
16 val quotient_of_rat: rat -> int * int |
|
17 val string_of_rat: rat -> string |
|
18 val eq: rat * rat -> bool |
|
19 val ord: rat * rat -> order |
|
20 val le: rat -> rat -> bool |
|
21 val lt: rat -> rat -> bool |
|
22 val sign: rat -> order |
|
23 val abs: rat -> rat |
|
24 val add: rat -> rat -> rat |
|
25 val mult: rat -> rat -> rat |
|
26 val neg: rat -> rat |
|
27 val inv: rat -> rat |
|
28 val rounddown: rat -> rat |
|
29 val roundup: rat -> rat |
|
30 end; |
|
31 |
|
32 structure Rat : RAT = |
|
33 struct |
|
34 |
|
35 fun common (p1, q1) (p2, q2) = |
|
36 let |
|
37 val m = Integer.lcm q1 q2; |
|
38 in ((p1 * (m div q1), p2 * (m div q2)), m) end; |
|
39 |
|
40 datatype rat = Rat of int * int; (*nominator, denominator (positive!)*) |
|
41 |
|
42 exception DIVZERO; |
|
43 |
|
44 fun rat_of_quotient (p, q) = |
|
45 let |
|
46 val m = Integer.gcd (Int.abs p) q |
|
47 in Rat (p div m, q div m) end handle Div => raise DIVZERO; |
|
48 |
|
49 fun quotient_of_rat (Rat r) = r; |
|
50 |
|
51 fun rat_of_int i = Rat (i, 1); |
|
52 |
|
53 val zero = rat_of_int 0; |
|
54 val one = rat_of_int 1; |
|
55 val two = rat_of_int 2; |
|
56 |
|
57 fun string_of_rat (Rat (p, q)) = |
|
58 string_of_int p ^ "/" ^ string_of_int q; |
|
59 |
|
60 fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2); |
|
61 |
|
62 fun ord (Rat (p1, q1), Rat (p2, q2)) = |
|
63 case (Integer.sign p1, Integer.sign p2) |
|
64 of (LESS, EQUAL) => LESS |
|
65 | (LESS, GREATER) => LESS |
|
66 | (EQUAL, LESS) => GREATER |
|
67 | (EQUAL, EQUAL) => EQUAL |
|
68 | (EQUAL, GREATER) => LESS |
|
69 | (GREATER, LESS) => GREATER |
|
70 | (GREATER, EQUAL) => GREATER |
|
71 | _ => int_ord (fst (common (p1, q1) (p2, q2))); |
|
72 |
|
73 fun le a b = not (ord (a, b) = GREATER); |
|
74 fun lt a b = (ord (a, b) = LESS); |
|
75 |
|
76 fun sign (Rat (p, _)) = Integer.sign p; |
|
77 |
|
78 fun abs (Rat (p, q)) = Rat (Int.abs p, q); |
|
79 |
|
80 fun add (Rat (p1, q1)) (Rat (p2, q2)) = |
|
81 let |
|
82 val ((m1, m2), n) = common (p1, q1) (p2, q2); |
|
83 in rat_of_quotient (m1 + m2, n) end; |
|
84 |
|
85 fun mult (Rat (p1, q1)) (Rat (p2, q2)) = |
|
86 rat_of_quotient (p1 * p2, q1 * q2); |
|
87 |
|
88 fun neg (Rat (p, q)) = Rat (~ p, q); |
|
89 |
|
90 fun inv (Rat (p, q)) = |
|
91 case Integer.sign p |
|
92 of LESS => Rat (~ q, ~ p) |
|
93 | EQUAL => raise DIVZERO |
|
94 | GREATER => Rat (q, p); |
|
95 |
|
96 fun rounddown (Rat (p, q)) = Rat (p div q, 1); |
|
97 |
|
98 fun roundup (Rat (p, q)) = |
|
99 case Integer.div_mod p q |
|
100 of (m, 0) => Rat (m, 1) |
|
101 | (m, _) => Rat (m + 1, 1); |
|
102 |
|
103 end; |
|
104 |
|
105 infix 7 */ //; |
|
106 infix 6 +/ -/; |
|
107 infix 4 =/ </ <=/ >/ >=/ <>/; |
|
108 |
|
109 fun a +/ b = Rat.add a b; |
|
110 fun a -/ b = a +/ Rat.neg b; |
|
111 fun a */ b = Rat.mult a b; |
|
112 fun a // b = a */ Rat.inv b; |
|
113 fun a =/ b = Rat.eq (a, b); |
|
114 fun a </ b = Rat.lt a b; |
|
115 fun a <=/ b = Rat.le a b; |
|
116 fun a >/ b = b </ a; |
|
117 fun a >=/ b = b <=/ a; |
|
118 fun a <>/ b = not (a =/ b); |