author  wenzelm 
Tue, 18 Sep 2007 16:08:00 +0200  
changeset 24630  351a308ab58d 
parent 24584  01e83ffa6c54 
child 30161  c26e515f1c29 
permissions  rwrr 
24584  1 
(* Title: Tools/rat.ML 
23251  2 
ID: $Id$ 
23520  3 
Author: Tobias Nipkow, Florian Haftmann, TU Muenchen 
23251  4 

5 
Canonical implementation of exact rational numbers. 

6 
*) 

7 

8 
signature RAT = 

9 
sig 

23297  10 
eqtype rat 
23251  11 
exception DIVZERO 
12 
val zero: rat 

13 
val one: rat 

14 
val two: rat 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

15 
val rat_of_int: int > rat 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

16 
val rat_of_quotient: int * int > rat 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

17 
val quotient_of_rat: rat > int * int 
23251  18 
val string_of_rat: rat > string 
19 
val eq: rat * rat > bool 

23520  20 
val ord: rat * rat > order 
23251  21 
val le: rat > rat > bool 
22 
val lt: rat > rat > bool 

23520  23 
val sign: rat > order 
24 
val abs: rat > rat 

23251  25 
val add: rat > rat > rat 
26 
val mult: rat > rat > rat 

27 
val neg: rat > rat 

28 
val inv: rat > rat 

23520  29 
val rounddown: rat > rat 
23251  30 
val roundup: rat > rat 
31 
end; 

32 

33 
structure Rat : RAT = 

34 
struct 

35 

23520  36 
fun common (p1, q1) (p2, q2) = 
37 
let 

38 
val m = Integer.lcm q1 q2; 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

39 
in ((p1 * (m div q1), p2 * (m div q2)), m) end; 
23520  40 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

41 
datatype rat = Rat of int * int; (*nominator, denominator (positive!)*) 
23251  42 

43 
exception DIVZERO; 

44 

45 
fun rat_of_quotient (p, q) = 

23261  46 
let 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

47 
val m = Integer.gcd (Int.abs p) q 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

48 
in Rat (p div m, q div m) end handle Div => raise DIVZERO; 
23520  49 

50 
fun quotient_of_rat (Rat r) = r; 

51 

52 
fun rat_of_int i = Rat (i, 1); 

23251  53 

23520  54 
val zero = rat_of_int 0; 
55 
val one = rat_of_int 1; 

56 
val two = rat_of_int 2; 

23251  57 

23520  58 
fun string_of_rat (Rat (p, q)) = 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

59 
string_of_int p ^ "/" ^ string_of_int q; 
23520  60 

61 
fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2); 

23251  62 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

63 
fun ord (Rat (p1, q1), Rat (p2, q2)) = 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

64 
case (Integer.sign p1, Integer.sign p2) 
23520  65 
of (LESS, EQUAL) => LESS 
66 
 (LESS, GREATER) => LESS 

67 
 (EQUAL, LESS) => GREATER 

68 
 (EQUAL, EQUAL) => EQUAL 

69 
 (EQUAL, GREATER) => LESS 

70 
 (GREATER, LESS) => GREATER 

71 
 (GREATER, EQUAL) => GREATER 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

72 
 _ => int_ord (fst (common (p1, q1) (p2, q2))); 
23251  73 

23520  74 
fun le a b = not (ord (a, b) = GREATER); 
75 
fun lt a b = (ord (a, b) = LESS); 

23251  76 

23520  77 
fun sign (Rat (p, _)) = Integer.sign p; 
23251  78 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

79 
fun abs (Rat (p, q)) = Rat (Int.abs p, q); 
23251  80 

23520  81 
fun add (Rat (p1, q1)) (Rat (p2, q2)) = 
82 
let 

83 
val ((m1, m2), n) = common (p1, q1) (p2, q2); 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

84 
in rat_of_quotient (m1 + m2, n) end; 
23251  85 

23520  86 
fun mult (Rat (p1, q1)) (Rat (p2, q2)) = 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

87 
rat_of_quotient (p1 * p2, q1 * q2); 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

88 

351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

89 
fun neg (Rat (p, q)) = Rat (~ p, q); 
23251  90 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

91 
fun inv (Rat (p, q)) = 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

92 
case Integer.sign p 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

93 
of LESS => Rat (~ q, ~ p) 
24522  94 
 EQUAL => raise DIVZERO 
24521  95 
 GREATER => Rat (q, p); 
23251  96 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

97 
fun rounddown (Rat (p, q)) = Rat (p div q, 1); 
23520  98 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

99 
fun roundup (Rat (p, q)) = 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

100 
case Integer.div_mod p q 
23520  101 
of (m, 0) => Rat (m, 1) 
102 
 (m, _) => Rat (m + 1, 1); 

23251  103 

104 
end; 

105 

23261  106 
infix 7 */ //; 
23297  107 
infix 6 +/ /; 
23251  108 
infix 4 =/ </ <=/ >/ >=/ <>/; 
109 

110 
fun a +/ b = Rat.add a b; 

111 
fun a / b = a +/ Rat.neg b; 

112 
fun a */ b = Rat.mult a b; 

23297  113 
fun a // b = a */ Rat.inv b; 
23261  114 
fun a =/ b = Rat.eq (a, b); 
23251  115 
fun a </ b = Rat.lt a b; 
116 
fun a <=/ b = Rat.le a b; 

117 
fun a >/ b = b </ a; 

118 
fun a >=/ b = b <=/ a; 

119 
fun a <>/ b = not (a =/ b); 