1(* Title: Pure/General/rat.ML 2 Author: Tobias Nipkow, Florian Haftmann, TU Muenchen 3 Author: Makarius 4 5Canonical implementation of exact rational numbers. 6*) 7 8signature RAT = 9sig 10 eqtype rat 11 val of_int: int -> rat 12 val make: int * int -> rat 13 val dest: rat -> int * int 14 val string_of_rat: rat -> string 15 val signed_string_of_rat: rat -> string 16 val ord: rat ord 17 val le: rat -> rat -> bool 18 val lt: rat -> rat -> bool 19 val sign: rat -> order 20 val abs: rat -> rat 21 val add: rat -> rat -> rat 22 val mult: rat -> rat -> rat 23 val neg: rat -> rat 24 val inv: rat -> rat 25 val floor: rat -> int 26 val ceil: rat -> int 27end; 28 29structure Rat : RAT = 30struct 31 32datatype rat = Rat of int * int; (*numerator, positive (!) denominator*) 33 34fun of_int i = Rat (i, 1); 35 36fun common (p1, q1) (p2, q2) = 37 let val m = Integer.lcm q1 q2 38 in ((p1 * (m div q1), p2 * (m div q2)), m) end; 39 40fun make (_, 0) = raise Div 41 | make (p, q) = 42 let 43 val m = Integer.gcd p q; 44 val (p', q') = (p div m, q div m); 45 in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end 46 47fun dest (Rat r) = r; 48 49fun string_of_rat (Rat (p, 1)) = string_of_int p 50 | string_of_rat (Rat (p, q)) = string_of_int p ^ "/" ^ string_of_int q; 51 52fun signed_string_of_rat (Rat (p, 1)) = signed_string_of_int p 53 | signed_string_of_rat (Rat (p, q)) = signed_string_of_int p ^ "/" ^ string_of_int q; 54 55fun ord (Rat (p1, q1), Rat (p2, q2)) = 56 (case (Integer.sign p1, Integer.sign p2) of 57 (LESS, EQUAL) => LESS 58 | (LESS, GREATER) => LESS 59 | (EQUAL, LESS) => GREATER 60 | (EQUAL, EQUAL) => EQUAL 61 | (EQUAL, GREATER) => LESS 62 | (GREATER, LESS) => GREATER 63 | (GREATER, EQUAL) => GREATER 64 | _ => int_ord (fst (common (p1, q1) (p2, q2)))); 65 66fun le a b = ord (a, b) <> GREATER; 67fun lt a b = ord (a, b) = LESS; 68 69fun sign (Rat (p, _)) = Integer.sign p; 70 71fun abs (r as Rat (p, q)) = if p < 0 then Rat (~ p, q) else r; 72 73fun add (Rat r1) (Rat r2) = 74 let val ((m1, m2), n) = common r1 r2 75 in make (m1 + m2, n) end; 76 77fun mult (Rat (p1, q1)) (Rat (p2, q2)) = make (p1 * p2, q1 * q2); 78 79fun neg (Rat (p, q)) = Rat (~ p, q); 80 81fun inv (Rat (p, q)) = 82 (case Integer.sign p of 83 LESS => Rat (~ q, ~ p) 84 | EQUAL => raise Div 85 | GREATER => Rat (q, p)); 86 87fun floor (Rat (p, q)) = p div q; 88 89fun ceil (Rat (p, q)) = 90 (case Integer.div_mod p q of 91 (m, 0) => m 92 | (m, _) => m + 1); 93 94end; 95 96ML_system_overload (uncurry Rat.add) "+"; 97ML_system_overload (fn (a, b) => Rat.add a (Rat.neg b)) "-"; 98ML_system_overload (uncurry Rat.mult) "*"; 99ML_system_overload (fn (a, b) => Rat.mult a (Rat.inv b)) "/"; 100ML_system_overload (uncurry Rat.lt) "<"; 101ML_system_overload (uncurry Rat.le) "<="; 102ML_system_overload (fn (a, b) => Rat.lt b a) ">"; 103ML_system_overload (fn (a, b) => Rat.le b a) ">="; 104ML_system_overload Rat.neg "~"; 105ML_system_overload Rat.abs "abs"; 106 107ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x))); 108