equal
deleted
inserted
replaced
1 (* Title: Pure/General/rat.ML |
1 (* Title: Pure/General/rat.ML |
2 Author: Tobias Nipkow, Florian Haftmann, TU Muenchen |
2 Author: Tobias Nipkow, Florian Haftmann, TU Muenchen |
|
3 Author: Makarius |
3 |
4 |
4 Canonical implementation of exact rational numbers. |
5 Canonical implementation of exact rational numbers. |
5 *) |
6 *) |
6 |
7 |
7 signature RAT = |
8 signature RAT = |
8 sig |
9 sig |
9 eqtype rat |
10 eqtype rat |
10 exception DIVZERO |
11 exception DIVZERO |
11 val zero: rat |
|
12 val one: rat |
|
13 val two: rat |
|
14 val of_int: int -> rat |
12 val of_int: int -> rat |
15 val make: int * int -> rat |
13 val make: int * int -> rat |
16 val dest: rat -> int * int |
14 val dest: rat -> int * int |
17 val string_of_rat: rat -> string |
15 val string_of_rat: rat -> string |
18 val eq: rat * rat -> bool |
16 val eq: rat * rat -> bool |
47 in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end |
45 in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end |
48 |
46 |
49 fun dest (Rat r) = r; |
47 fun dest (Rat r) = r; |
50 |
48 |
51 fun of_int i = Rat (i, 1); |
49 fun of_int i = Rat (i, 1); |
52 |
|
53 val zero = of_int 0; |
|
54 val one = of_int 1; |
|
55 val two = of_int 2; |
|
56 |
50 |
57 fun string_of_rat (Rat (p, q)) = |
51 fun string_of_rat (Rat (p, q)) = |
58 string_of_int p ^ "/" ^ string_of_int q; |
52 string_of_int p ^ "/" ^ string_of_int q; |
59 |
53 |
60 fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2); |
54 fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2); |