23251
|
1 |
(* Title: Pure/General/rat.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow, TU Muenchen
|
|
4 |
|
|
5 |
Canonical implementation of exact rational numbers.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature RAT =
|
|
9 |
sig
|
|
10 |
type rat
|
|
11 |
exception DIVZERO
|
|
12 |
val zero: rat
|
|
13 |
val one: rat
|
|
14 |
val two: rat
|
|
15 |
val rat_of_int: Intt.int -> rat
|
|
16 |
val rat_of_quotient: Intt.int * Intt.int -> rat
|
|
17 |
val quotient_of_rat: rat -> Intt.int * Intt.int
|
|
18 |
val string_of_rat: rat -> string
|
|
19 |
val eq: rat * rat -> bool
|
|
20 |
val cmp: rat * rat -> order
|
|
21 |
val le: rat -> rat -> bool
|
|
22 |
val lt: rat -> rat -> bool
|
|
23 |
val cmp_zero: rat -> order
|
|
24 |
val add: rat -> rat -> rat
|
|
25 |
val mult: rat -> rat -> rat
|
|
26 |
val neg: rat -> rat
|
|
27 |
val inv: rat -> rat
|
|
28 |
val roundup: rat -> rat
|
|
29 |
val rounddown: rat -> rat
|
|
30 |
end;
|
|
31 |
|
|
32 |
structure Rat : RAT =
|
|
33 |
struct
|
|
34 |
|
|
35 |
datatype rat = Rat of bool * Intt.int * Intt.int;
|
|
36 |
|
|
37 |
exception DIVZERO;
|
|
38 |
|
|
39 |
val zero = Rat (true, Intt.int 0, Intt.int 1);
|
|
40 |
val one = Rat (true, Intt.int 1, Intt.int 1);
|
|
41 |
val two = Rat (true, Intt.int 2, Intt.int 1);
|
|
42 |
|
|
43 |
fun rat_of_int i =
|
|
44 |
if i < Intt.int 0
|
|
45 |
then Rat (false, ~i, Intt.int 1)
|
|
46 |
else Rat (true, i, Intt.int 1);
|
|
47 |
|
|
48 |
fun norm (a, p, q) =
|
|
49 |
if p = Intt.int 0 then Rat (true, Intt.int 0, Intt.int 1)
|
|
50 |
else
|
|
51 |
let
|
|
52 |
val absp = abs p
|
|
53 |
val m = gcd (absp, q)
|
|
54 |
in Rat(a = (Intt.int 0 <= p), absp div m, q div m) end;
|
|
55 |
|
|
56 |
fun common (p1, q1, p2, q2) =
|
|
57 |
let val q' = lcm (q1, q2)
|
|
58 |
in (p1 * (q' div q1), p2 * (q' div q2), q') end
|
|
59 |
|
|
60 |
fun rat_of_quotient (p, q) =
|
|
61 |
if q = Intt.int 0 then raise DIVZERO
|
|
62 |
else norm (Intt.int 0 <= q, p, abs q);
|
|
63 |
|
|
64 |
fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~p, q);
|
|
65 |
|
|
66 |
fun string_of_rat r =
|
|
67 |
let val (p, q) = quotient_of_rat r
|
|
68 |
in Intt.string_of_int p ^ "/" ^ Intt.string_of_int q end;
|
|
69 |
|
|
70 |
fun eq (Rat (false, _, _), Rat (true, _, _)) = false
|
|
71 |
| eq (Rat (true, _, _), Rat (false, _, _)) = false
|
|
72 |
| eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2
|
|
73 |
|
|
74 |
fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
|
|
75 |
| cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
|
|
76 |
| cmp (Rat (a, p1, q1), Rat (_, p2, q2)) =
|
|
77 |
let val (r1, r2, _) = common (p1, q1, p2, q2)
|
|
78 |
in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end;
|
|
79 |
|
|
80 |
fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end;
|
|
81 |
fun lt a b = cmp (a, b) = LESS;
|
|
82 |
|
|
83 |
fun cmp_zero (Rat (false, _, _)) = LESS
|
|
84 |
| cmp_zero (Rat (_, 0, _)) = EQUAL
|
|
85 |
| cmp_zero (Rat (_, _, _)) = GREATER;
|
|
86 |
|
|
87 |
fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
|
|
88 |
let
|
|
89 |
val (r1, r2, den) = common (p1, q1, p2, q2)
|
|
90 |
val num = (if a1 then r1 else ~r1) + (if a2 then r2 else ~r2)
|
|
91 |
in norm (true, num, den) end;
|
|
92 |
|
|
93 |
fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
|
|
94 |
norm (a1=a2, p1*p2, q1*q2);
|
|
95 |
|
|
96 |
fun neg (r as Rat (b, p, q)) =
|
|
97 |
if p = Intt.int 0 then r
|
|
98 |
else Rat (not b, p, q);
|
|
99 |
|
|
100 |
fun inv (Rat (a, p, q)) =
|
|
101 |
if p = Intt.int 0 then raise DIVZERO
|
|
102 |
else Rat (a, q, p);
|
|
103 |
|
|
104 |
fun roundup (r as Rat (a, p, q)) =
|
|
105 |
if q = Intt.int 1 then r
|
|
106 |
else
|
|
107 |
let
|
|
108 |
fun round true q = Rat (true, q + Intt.int 1, Intt.int 1)
|
|
109 |
| round false q =
|
|
110 |
if q = Intt.int 0
|
|
111 |
then Rat (true, Intt.int 0, Intt.int 1)
|
|
112 |
else Rat (false, q, Intt.int 1);
|
|
113 |
in round a (p div q) end;
|
|
114 |
|
|
115 |
fun rounddown (r as Rat (a, p, q)) =
|
|
116 |
if q = Intt.int 1 then r
|
|
117 |
else
|
|
118 |
let
|
|
119 |
fun round true q = Rat (true, q, Intt.int 1)
|
|
120 |
| round false q = Rat (false, q + Intt.int 1, Intt.int 1)
|
|
121 |
in round a (p div q) end;
|
|
122 |
|
|
123 |
end;
|
|
124 |
|
|
125 |
infix 5 +/;
|
|
126 |
infix 5 -/;
|
|
127 |
infix 7 */;
|
|
128 |
infix 7 //;
|
|
129 |
infix 4 =/ </ <=/ >/ >=/ <>/;
|
|
130 |
|
|
131 |
fun a +/ b = Rat.add a b;
|
|
132 |
fun a -/ b = a +/ Rat.neg b;
|
|
133 |
fun a */ b = Rat.mult a b;
|
|
134 |
fun a // b = a */ Rat.inv b;
|
|
135 |
fun a =/ b = Rat.eq (a,b);
|
|
136 |
fun a </ b = Rat.lt a b;
|
|
137 |
fun a <=/ b = Rat.le a b;
|
|
138 |
fun a >/ b = b </ a;
|
|
139 |
fun a >=/ b = b <=/ a;
|
|
140 |
fun a <>/ b = not (a =/ b);
|