author | haftmann |
Mon, 21 May 2007 19:11:42 +0200 | |
changeset 23063 | b4ee6ec4f9c6 |
parent 23036 | 65b4f545a76f |
child 23231 | aef7b4e5c8fe |
permissions | -rw-r--r-- |
17848 | 1 |
(* Title: Pure/General/rat.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow, TU Muenchen |
|
4 |
||
17940 | 5 |
Canonical implementation of exact rational numbers. |
17848 | 6 |
*) |
7 |
||
8 |
signature RAT = |
|
9 |
sig |
|
10 |
type rat |
|
11 |
exception DIVZERO |
|
12 |
val zero: rat |
|
19557 | 13 |
val one: rat |
22950 | 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 |
|
17848 | 18 |
val string_of_rat: rat -> string |
19 |
val eq: rat * rat -> bool |
|
22950 | 20 |
val cmp: rat * rat -> order |
21 |
val le: rat -> rat -> bool |
|
23036
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
22 |
val lt: rat -> rat -> bool |
22950 | 23 |
val cmp_zero: rat -> order |
24 |
val add: rat -> rat -> rat |
|
25 |
val mult: rat -> rat -> rat |
|
17848 | 26 |
val neg: rat -> rat |
27 |
val inv: rat -> rat |
|
17940 | 28 |
val roundup: rat -> rat |
29 |
val rounddown: rat -> rat |
|
17848 | 30 |
end; |
31 |
||
23063 | 32 |
structure Rat :> RAT = |
17848 | 33 |
struct |
34 |
||
22950 | 35 |
datatype rat = Rat of bool * Intt.int * Intt.int; |
17848 | 36 |
|
37 |
exception DIVZERO; |
|
38 |
||
22950 | 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); |
|
19557 | 42 |
|
22950 | 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); |
|
17848 | 47 |
|
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
48 |
fun norm (a, p, q) = |
22950 | 49 |
if p = Intt.int 0 then Rat (true, Intt.int 0, Intt.int 1) |
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
50 |
else |
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
51 |
let |
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
52 |
val absp = abs p |
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
53 |
val m = gcd (absp, q) |
22950 | 54 |
in Rat(a = (Intt.int 0 <= p), absp div m, q div m) end; |
17848 | 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 |
||
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
60 |
fun rat_of_quotient (p, q) = |
22950 | 61 |
if q = Intt.int 0 then raise DIVZERO |
62 |
else norm (Intt.int 0 <= q, p, abs q); |
|
17848 | 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 |
|
22950 | 68 |
in Intt.string_of_int p ^ "/" ^ Intt.string_of_int q end; |
17848 | 69 |
|
17940 | 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 |
||
22950 | 74 |
fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS |
75 |
| cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER |
|
76 |
| cmp (Rat (a, p1, q1), Rat (_, p2, q2)) = |
|
17940 | 77 |
let val (r1, r2, _) = common (p1, q1, p2, q2) |
22950 | 78 |
in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end; |
17940 | 79 |
|
23063 | 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 |
||
22950 | 83 |
fun cmp_zero (Rat (false, _, _)) = LESS |
84 |
| cmp_zero (Rat (_, 0, _)) = EQUAL |
|
85 |
| cmp_zero (Rat (_, _, _)) = GREATER; |
|
17848 | 86 |
|
22950 | 87 |
fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) = |
17848 | 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 |
||
22950 | 93 |
fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) = |
17848 | 94 |
norm (a1=a2, p1*p2, q1*q2); |
95 |
||
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
96 |
fun neg (r as Rat (b, p, q)) = |
22950 | 97 |
if p = Intt.int 0 then r |
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
98 |
else Rat (not b, p, q); |
17848 | 99 |
|
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
100 |
fun inv (Rat (a, p, q)) = |
22950 | 101 |
if p = Intt.int 0 then raise DIVZERO |
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
102 |
else Rat (a, q, p); |
17848 | 103 |
|
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
104 |
fun roundup (r as Rat (a, p, q)) = |
22950 | 105 |
if q = Intt.int 1 then r |
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
106 |
else |
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
107 |
let |
22950 | 108 |
fun round true q = Rat (true, q + Intt.int 1, Intt.int 1) |
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
109 |
| round false q = |
22950 | 110 |
if q = Intt.int 0 |
111 |
then Rat (true, Intt.int 0, Intt.int 1) |
|
112 |
else Rat (false, q, Intt.int 1); |
|
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
113 |
in round a (p div q) end; |
17940 | 114 |
|
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
115 |
fun rounddown (r as Rat (a, p, q)) = |
22950 | 116 |
if q = Intt.int 1 then r |
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
117 |
else |
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
118 |
let |
22950 | 119 |
fun round true q = Rat (true, q, Intt.int 1) |
120 |
| round false q = Rat (false, q + Intt.int 1, Intt.int 1) |
|
22574
e6c25fd3de2a
avoid overloaded integer constants (accomodate Alice);
wenzelm
parents:
22189
diff
changeset
|
121 |
in round a (p div q) end; |
17940 | 122 |
|
17848 | 123 |
end; |
23036
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
124 |
|
23063 | 125 |
infix 6 +/; (*FIXME infix 5?*) |
126 |
infix 5 -/; |
|
127 |
infix 7 */; |
|
128 |
infix 8 //; (*FIXME infix 7?*) |
|
129 |
infix 4 =/ </ <=/ >/ >=/ <>/; |
|
23036
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
130 |
|
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
131 |
fun a +/ b = Rat.add a b; |
23063 | 132 |
fun a -/ b = a +/ Rat.neg b; |
133 |
fun a */ b = Rat.mult a b; |
|
134 |
fun a // b = a */ Rat.inv b; |
|
23036
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
135 |
fun a =/ b = Rat.eq (a,b); |
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
136 |
fun a </ b = Rat.lt a b; |
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
137 |
fun a <=/ b = Rat.le a b; |
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
138 |
fun a >/ b = b </ a; |
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
139 |
fun a >=/ b = b <=/ a; |
65b4f545a76f
added lt and some other infix operation analogous to Ocaml's num library
chaieb
parents:
22950
diff
changeset
|
140 |
fun a <>/ b = not (a =/ b); |