author | wenzelm |
Wed, 01 Jun 2016 10:55:10 +0200 | |
changeset 63202 | e77481be5c97 |
parent 63201 | f151704c08e4 |
child 63203 | c1b15830549e |
permissions | -rw-r--r-- |
63197
af562e976038
rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
wenzelm
parents:
30161
diff
changeset
|
1 |
(* Title: Pure/General/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 |
|
63201 | 14 |
val of_int: int -> rat |
15 |
val make: int * int -> rat |
|
16 |
val dest: 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 |
||
63202 | 35 |
datatype rat = Rat of int * int; (*numerator, positive (!) denominator*) |
63199
da38571dd5bd
prefer more efficient Poly/ML operations, taking care of sign;
wenzelm
parents:
63198
diff
changeset
|
36 |
|
23520 | 37 |
fun common (p1, q1) (p2, q2) = |
63199
da38571dd5bd
prefer more efficient Poly/ML operations, taking care of sign;
wenzelm
parents:
63198
diff
changeset
|
38 |
let val m = PolyML.IntInf.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 |
|
23251 | 41 |
exception DIVZERO; |
42 |
||
63201 | 43 |
fun make (p, q) = |
63200 | 44 |
let |
45 |
val m = PolyML.IntInf.gcd (p, q); |
|
46 |
val (p', q') = (p div m, q div m) handle Div => raise DIVZERO; |
|
47 |
in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end |
|
23520 | 48 |
|
63201 | 49 |
fun dest (Rat r) = r; |
23520 | 50 |
|
63201 | 51 |
fun of_int i = Rat (i, 1); |
23251 | 52 |
|
63201 | 53 |
val zero = of_int 0; |
54 |
val one = of_int 1; |
|
55 |
val two = 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)) = |
63202 | 63 |
(case (Integer.sign p1, Integer.sign p2) of |
64 |
(LESS, EQUAL) => LESS |
|
23520 | 65 |
| (LESS, GREATER) => LESS |
66 |
| (EQUAL, LESS) => GREATER |
|
67 |
| (EQUAL, EQUAL) => EQUAL |
|
68 |
| (EQUAL, GREATER) => LESS |
|
69 |
| (GREATER, LESS) => GREATER |
|
70 |
| (GREATER, EQUAL) => GREATER |
|
63202 | 71 |
| _ => int_ord (fst (common (p1, q1) (p2, q2)))); |
23251 | 72 |
|
23520 | 73 |
fun le a b = not (ord (a, b) = GREATER); |
63202 | 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)) = |
63202 | 81 |
let val ((m1, m2), n) = common (p1, q1) (p2, q2) |
63201 | 82 |
in make (m1 + m2, n) end; |
23251 | 83 |
|
63202 | 84 |
fun mult (Rat (p1, q1)) (Rat (p2, q2)) = make (p1 * p2, q1 * q2); |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
85 |
|
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
86 |
fun neg (Rat (p, q)) = Rat (~ p, q); |
23251 | 87 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
88 |
fun inv (Rat (p, q)) = |
63202 | 89 |
(case Integer.sign p of |
90 |
LESS => Rat (~ q, ~ p) |
|
24522 | 91 |
| EQUAL => raise DIVZERO |
63202 | 92 |
| GREATER => Rat (q, p)); |
23251 | 93 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
94 |
fun rounddown (Rat (p, q)) = Rat (p div q, 1); |
23520 | 95 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
96 |
fun roundup (Rat (p, q)) = |
63202 | 97 |
(case Integer.div_mod p q of |
98 |
(m, 0) => Rat (m, 1) |
|
99 |
| (m, _) => Rat (m + 1, 1)); |
|
23251 | 100 |
|
101 |
end; |
|
102 |
||
63198
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
103 |
ML_system_overload (uncurry Rat.add) "+"; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
104 |
ML_system_overload (fn (a, b) => Rat.add a (Rat.neg b)) "-"; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
105 |
ML_system_overload (uncurry Rat.mult) "*"; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
106 |
ML_system_overload (fn (a, b) => Rat.mult a (Rat.inv b)) "/"; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
107 |
ML_system_overload Rat.eq "="; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
108 |
ML_system_overload (uncurry Rat.lt) "<"; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
109 |
ML_system_overload (uncurry Rat.le) "<="; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
110 |
ML_system_overload (fn (a, b) => Rat.lt b a) ">"; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
111 |
ML_system_overload (fn (a, b) => Rat.le b a) ">="; |
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63197
diff
changeset
|
112 |
ML_system_overload (not o Rat.eq) "<>"; |