author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 30161  c26e515f1c29 
permissions  rwrr 
24584  1 
(* Title: Tools/rat.ML 
23520  2 
Author: Tobias Nipkow, Florian Haftmann, TU Muenchen 
23251  3 

4 
Canonical implementation of exact rational numbers. 

5 
*) 

6 

7 
signature RAT = 

8 
sig 

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

12 
val one: rat 

13 
val two: rat 

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

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

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

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

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

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

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

26 
val neg: rat > rat 

27 
val inv: rat > rat 

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

31 

32 
structure Rat : RAT = 

33 
struct 

34 

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

37 
val m = Integer.lcm q1 q2; 

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

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

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

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

42 
exception DIVZERO; 

43 

44 
fun rat_of_quotient (p, q) = 

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

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

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

49 
fun quotient_of_rat (Rat r) = r; 

50 

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

23251  52 

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

55 
val two = rat_of_int 2; 

23251  56 

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

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

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

23251  61 

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

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

63 
case (Integer.sign p1, Integer.sign p2) 
23520  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 

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

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

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

23251  75 

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

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

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

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

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

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

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

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

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

87 

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

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

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

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

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

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

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

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

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

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

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

23251  102 

103 
end; 

104 

23261  105 
infix 7 */ //; 
23297  106 
infix 6 +/ /; 
23251  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; 

23297  112 
fun a // b = a */ Rat.inv b; 
23261  113 
fun a =/ b = Rat.eq (a, b); 
23251  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); 