23251

1 
(* Title: Pure/General/rat.ML


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

23261

15 
val rat_of_int: integer > rat


16 
val rat_of_quotient: integer * integer > rat


17 
val quotient_of_rat: rat > integer * integer

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 signabs: rat > order * rat


24 
val sign: rat > order


25 
val abs: rat > rat

23251

26 
val add: rat > rat > rat


27 
val mult: rat > rat > rat


28 
val neg: rat > rat


29 
val inv: rat > rat

23520

30 
val rounddown: rat > rat

23251

31 
val roundup: rat > rat


32 
end;


33 


34 
structure Rat : RAT =


35 
struct


36 

23520

37 
fun common (p1, q1) (p2, q2) =


38 
let


39 
val m = Integer.lcm q1 q2;


40 
in ((Integer.mult p1 (Integer.div m q1), Integer.mult p2 (Integer.div m q2)), m) end;


41 


42 
datatype rat = Rat of integer * integer; (* nominator, denominator (positive!) *)

23251

43 


44 
exception DIVZERO;


45 


46 
fun rat_of_quotient (p, q) =

23261

47 
let

23520

48 
val m = Integer.gcd (Integer.abs p) q


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


50 


51 
fun quotient_of_rat (Rat r) = r;


52 


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

23251

54 

23520

55 
val zero = rat_of_int 0;


56 
val one = rat_of_int 1;


57 
val two = rat_of_int 2;

23251

58 

23520

59 
fun string_of_rat (Rat (p, q)) =


60 
Integer.string_of_int p ^ "/" ^ Integer.string_of_int q;


61 


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

23251

63 

23520

64 
fun ord (Rat (p1, q1), Rat (p2, q2)) = case (Integer.sign p1, Integer.sign p2)


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


72 
 _ => Integer.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 

23520

79 
fun abs (Rat (p, q)) = Rat (Integer.abs p, q);

23251

80 

23520

81 
fun signabs (Rat (p, q)) =

23251

82 
let

23520

83 
val (s, p') = Integer.signabs p;


84 
in (s, Rat (p', q)) end;

23251

85 

23520

86 
fun add (Rat (p1, q1)) (Rat (p2, q2)) =


87 
let


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


89 
in rat_of_quotient (Integer.add m1 m2, n) end;

23251

90 

23520

91 
fun mult (Rat (p1, q1)) (Rat (p2, q2)) =


92 
rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2);

23251

93 

23520

94 
fun neg (Rat (p, q)) = Rat (Integer.neg p, q);


95 

24521

96 
fun inv (Rat (p, q)) = case Integer.sign p


97 
of LESS => Rat (Integer.neg q, Integer.neg p)

24522

98 
 EQUAL => raise DIVZERO

24521

99 
 GREATER => Rat (q, p);

23251

100 

23520

101 
fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1);


102 


103 
fun roundup (Rat (p, q)) = case Integer.divmod p q


104 
of (m, 0) => Rat (m, 1)


105 
 (m, _) => Rat (m + 1, 1);

23251

106 


107 
end;


108 

23261

109 
infix 7 */ //;

23297

110 
infix 6 +/ /;

23251

111 
infix 4 =/ </ <=/ >/ >=/ <>/;


112 


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


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


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

23297

116 
fun a // b = a */ Rat.inv b;

23261

117 
fun a =/ b = Rat.eq (a, b);

23251

118 
fun a </ b = Rat.lt a b;


119 
fun a <=/ b = Rat.le a b;


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


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


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