moved generic algebra modules
authorhaftmann
Tue Jun 05 15:17:02 2007 +0200 (2007-06-05)
changeset 23251471b576aad25
parent 23250 9886802cbbd6
child 23252 67268bb40b21
moved generic algebra modules
NEWS
src/HOL/Real/Float.thy
src/Pure/General/float.ML
src/Pure/General/int.ML
src/Pure/General/rat.ML
src/Pure/library.ML
src/Tools/float.ML
src/Tools/integer.ML
src/Tools/rat.ML
     1.1 --- a/NEWS	Tue Jun 05 15:16:11 2007 +0200
     1.2 +++ b/NEWS	Tue Jun 05 15:17:02 2007 +0200
     1.3 @@ -738,8 +738,7 @@
     1.4  * Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one".
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -* Added theory Code_Generator providing class 'eq', allowing for code
     1.8 -generation with polymorphic equality.
     1.9 +* Added class "HOL.eq", allowing for code generation with polymorphic equality.
    1.10  
    1.11  * Numeral syntax: type 'bin' which was a mere type copy of 'int' has
    1.12  been abandoned in favour of plain 'int'. INCOMPATIBILITY --
    1.13 @@ -952,6 +951,8 @@
    1.14  
    1.15  *** ML ***
    1.16  
    1.17 +* Generic arithmetic modules: Tools/integer.ML, Tools/rat.ML, Tools/float.ML
    1.18 +
    1.19  * Context data interfaces (Theory/Proof/GenericDataFun): removed
    1.20  name/print, uninitialized data defaults to ad-hoc copy of empty value,
    1.21  init only required for impure data.  INCOMPATIBILITY: empty really
     2.1 --- a/src/HOL/Real/Float.thy	Tue Jun 05 15:16:11 2007 +0200
     2.2 +++ b/src/HOL/Real/Float.thy	Tue Jun 05 15:17:02 2007 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  theory Float
     2.6  imports Real Parity
     2.7 -uses "~~/src/Pure/General/float.ML" ("float_arith.ML")
     2.8 +uses "~~/src/Tools/float.ML" ("float_arith.ML")
     2.9  begin
    2.10  
    2.11  definition
     3.1 --- a/src/Pure/General/float.ML	Tue Jun 05 15:16:11 2007 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,60 +0,0 @@
     3.4 -(*  Title:      Pure/General/float.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Steven Obua, Florian Haftmann, TU Muenchen
     3.7 -
     3.8 -Implementation of real numbers as mantisse-exponent pairs.
     3.9 -*)
    3.10 -
    3.11 -signature FLOAT =
    3.12 -sig
    3.13 -  type float = Intt.int * Intt.int
    3.14 -  val zero: float
    3.15 -  val eq: float * float -> bool
    3.16 -  val cmp: float * float -> order
    3.17 -  val cmp_zero: float -> order
    3.18 -  val min: float -> float -> float
    3.19 -  val max: float -> float -> float
    3.20 -  val add: float -> float -> float
    3.21 -  val sub: float -> float -> float
    3.22 -  val neg: float -> float
    3.23 -  val mult: float -> float -> float
    3.24 -  val positive_part: float -> float
    3.25 -  val negative_part: float -> float
    3.26 -end;
    3.27 -
    3.28 -structure Float : FLOAT =
    3.29 -struct
    3.30 -
    3.31 -type float = Intt.int * Intt.int;
    3.32 -
    3.33 -val zero = (Intt.zero, Intt.zero);
    3.34 -
    3.35 -fun add (a1, b1) (a2, b2) =
    3.36 -  if Intt.cmp (b1, b2) = LESS then
    3.37 -    (Intt.add a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
    3.38 -  else
    3.39 -    (Intt.add (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
    3.40 -
    3.41 -fun sub (a1, b1) (a2, b2) =
    3.42 -  if Intt.cmp (b1, b2) = LESS then
    3.43 -    (Intt.sub a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
    3.44 -  else
    3.45 -    (Intt.sub (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
    3.46 -
    3.47 -fun neg (a, b) = (Intt.neg a, b);
    3.48 -
    3.49 -fun mult (a1, b1) (a2, b2) = (Intt.mult a1 a2, Intt.add b1 b2);
    3.50 -
    3.51 -fun cmp_zero (a, b) = Intt.cmp_zero a;
    3.52 -
    3.53 -fun cmp (r, s) = cmp_zero (sub r s);
    3.54 -
    3.55 -fun eq (r, s) = cmp (r, s) = EQUAL;
    3.56 -
    3.57 -fun min r s = case cmp (r, s) of LESS => r | _ => s;
    3.58 -fun max r s = case cmp (r, s) of LESS => s | _ => r;
    3.59 -
    3.60 -fun positive_part (a, b) = (Intt.max Intt.zero a, b);
    3.61 -fun negative_part (a, b) = (Intt.min Intt.zero a, b);
    3.62 -
    3.63 -end;
     4.1 --- a/src/Pure/General/int.ML	Tue Jun 05 15:16:11 2007 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,82 +0,0 @@
     4.4 -(*  Title:      Pure/General/int.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Florian Haftmann, TU Muenchen
     4.7 -
     4.8 -Unbounded integers.
     4.9 -*)
    4.10 -
    4.11 -signature INTT =
    4.12 -sig
    4.13 -  type int
    4.14 -  val zero: int
    4.15 -  val one: int
    4.16 -  val two: int
    4.17 -  val int: Int.int -> int
    4.18 -  val machine_int: int -> Int.int
    4.19 -  val string_of_int: int -> string
    4.20 -  val int_of_string: string -> int option
    4.21 -  val eq: int * int -> bool
    4.22 -  val cmp: int * int -> order
    4.23 -  val le: int -> int -> bool
    4.24 -  val cmp_zero: int -> order
    4.25 -  val min: int -> int -> int
    4.26 -  val max: int -> int -> int
    4.27 -  val inc: int -> int
    4.28 -  val add: int -> int -> int
    4.29 -  val sub: int -> int -> int
    4.30 -  val mult: int -> int -> int
    4.31 -  val divmod: int -> int -> int * int
    4.32 -  val div: int -> int -> int
    4.33 -  val mod: int -> int -> int
    4.34 -  val neg: int -> int
    4.35 -  val exp: int -> int
    4.36 -  val log: int -> int
    4.37 -  val pow: int -> int -> int (* exponent -> base -> result *)
    4.38 -end;
    4.39 -
    4.40 -structure Intt: INTT =
    4.41 -struct
    4.42 -
    4.43 -open IntInf;
    4.44 -
    4.45 -val int = fromInt;
    4.46 -
    4.47 -val zero = int 0;
    4.48 -val one = int 1;
    4.49 -val two = int 2;
    4.50 -
    4.51 -val machine_int = toInt;
    4.52 -val string_of_int = toString;
    4.53 -val int_of_string = fromString;
    4.54 -
    4.55 -val eq = op = : int * int -> bool;
    4.56 -val cmp = compare;
    4.57 -val le = curry (op <=);
    4.58 -val cmp_zero = curry cmp zero;
    4.59 -
    4.60 -val min = curry min;
    4.61 -val max = curry max;
    4.62 -
    4.63 -val inc = curry (op +) one;
    4.64 -
    4.65 -val add = curry (op +);
    4.66 -val sub = curry (op -);
    4.67 -val mult = curry ( op * );
    4.68 -val divmod = curry divMod;
    4.69 -nonfix div val div = curry div;
    4.70 -nonfix mod val mod = curry mod;
    4.71 -val neg = ~;
    4.72 -
    4.73 -fun pow k l =
    4.74 -  let
    4.75 -    fun pw 0 = 1
    4.76 -      | pw k = mult l (pw (sub k 1));
    4.77 -  in if k < zero
    4.78 -    then error "pow: negative exponent"
    4.79 -    else pw k
    4.80 -  end;
    4.81 -
    4.82 -fun exp k = pow k two;
    4.83 -val log = int o log2;
    4.84 -
    4.85 -end;
     5.1 --- a/src/Pure/General/rat.ML	Tue Jun 05 15:16:11 2007 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,140 +0,0 @@
     5.4 -(*  Title:      Pure/General/rat.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tobias Nipkow, TU Muenchen
     5.7 -
     5.8 -Canonical implementation of exact rational numbers.
     5.9 -*)
    5.10 -
    5.11 -signature RAT =
    5.12 -sig
    5.13 -  type rat
    5.14 -  exception DIVZERO
    5.15 -  val zero: rat
    5.16 -  val one: rat
    5.17 -  val two: rat
    5.18 -  val rat_of_int: Intt.int -> rat
    5.19 -  val rat_of_quotient: Intt.int * Intt.int -> rat
    5.20 -  val quotient_of_rat: rat -> Intt.int * Intt.int
    5.21 -  val string_of_rat: rat -> string
    5.22 -  val eq: rat * rat -> bool
    5.23 -  val cmp: rat * rat -> order
    5.24 -  val le: rat -> rat -> bool
    5.25 -  val lt: rat -> rat -> bool
    5.26 -  val cmp_zero: rat -> order
    5.27 -  val add: rat -> rat -> rat
    5.28 -  val mult: rat -> rat -> rat
    5.29 -  val neg: rat -> rat
    5.30 -  val inv: rat -> rat
    5.31 -  val roundup: rat -> rat
    5.32 -  val rounddown: rat -> rat
    5.33 -end;
    5.34 -
    5.35 -structure Rat : RAT =
    5.36 -struct
    5.37 -
    5.38 -datatype rat = Rat of bool * Intt.int * Intt.int;
    5.39 -
    5.40 -exception DIVZERO;
    5.41 -
    5.42 -val zero = Rat (true, Intt.int 0, Intt.int 1);
    5.43 -val one = Rat (true, Intt.int 1, Intt.int 1);
    5.44 -val two = Rat (true, Intt.int 2, Intt.int 1);
    5.45 -
    5.46 -fun rat_of_int i =
    5.47 -  if i < Intt.int 0
    5.48 -  then Rat (false, ~i, Intt.int 1)
    5.49 -  else Rat (true, i, Intt.int 1);
    5.50 -
    5.51 -fun norm (a, p, q) =
    5.52 -  if p = Intt.int 0 then Rat (true, Intt.int 0, Intt.int 1)
    5.53 -  else
    5.54 -    let
    5.55 -      val absp = abs p
    5.56 -      val m = gcd (absp, q)
    5.57 -    in Rat(a = (Intt.int 0 <= p), absp div m, q div m) end;
    5.58 -
    5.59 -fun common (p1, q1, p2, q2) =
    5.60 -  let val q' = lcm (q1, q2)
    5.61 -  in (p1 * (q' div q1), p2 * (q' div q2), q') end
    5.62 -
    5.63 -fun rat_of_quotient (p, q) =
    5.64 -  if q = Intt.int 0 then raise DIVZERO
    5.65 -  else norm (Intt.int 0 <= q, p, abs q);
    5.66 -
    5.67 -fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~p, q);
    5.68 -
    5.69 -fun string_of_rat r =
    5.70 -  let val (p, q) = quotient_of_rat r
    5.71 -  in Intt.string_of_int p ^ "/" ^ Intt.string_of_int q end;
    5.72 -
    5.73 -fun eq (Rat (false, _, _), Rat (true, _, _)) = false
    5.74 -  | eq (Rat (true, _, _), Rat (false, _, _)) = false
    5.75 -  | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2
    5.76 -
    5.77 -fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
    5.78 -  | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
    5.79 -  | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) =
    5.80 -      let val (r1, r2, _) = common (p1, q1, p2, q2)
    5.81 -      in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end;
    5.82 -
    5.83 -fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end;
    5.84 -fun lt a b = cmp (a, b) = LESS;
    5.85 -
    5.86 -fun cmp_zero (Rat (false, _, _)) = LESS
    5.87 -  | cmp_zero (Rat (_, 0, _)) = EQUAL
    5.88 -  | cmp_zero (Rat (_, _, _)) = GREATER;
    5.89 -
    5.90 -fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
    5.91 -  let
    5.92 -    val (r1, r2, den) = common (p1, q1, p2, q2)
    5.93 -    val num = (if a1 then r1 else ~r1) + (if a2 then r2 else ~r2)
    5.94 -  in norm (true, num, den) end;
    5.95 -
    5.96 -fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
    5.97 -  norm (a1=a2, p1*p2, q1*q2);
    5.98 -
    5.99 -fun neg (r as Rat (b, p, q)) =
   5.100 -  if p = Intt.int 0 then r
   5.101 -  else Rat (not b, p, q);
   5.102 -
   5.103 -fun inv (Rat (a, p, q)) =
   5.104 -  if p = Intt.int 0 then raise DIVZERO
   5.105 -  else Rat (a, q, p);
   5.106 -
   5.107 -fun roundup (r as Rat (a, p, q)) =
   5.108 -  if q = Intt.int 1 then r
   5.109 -  else
   5.110 -    let
   5.111 -      fun round true q = Rat (true, q + Intt.int 1, Intt.int 1)
   5.112 -        | round false q =
   5.113 -            if q = Intt.int 0
   5.114 -            then Rat (true, Intt.int 0, Intt.int 1)
   5.115 -            else Rat (false, q, Intt.int 1);
   5.116 -    in round a (p div q) end;
   5.117 -
   5.118 -fun rounddown (r as Rat (a, p, q)) =
   5.119 -  if q = Intt.int 1 then r
   5.120 -  else
   5.121 -    let
   5.122 -      fun round true q = Rat (true, q, Intt.int 1)
   5.123 -        | round false q = Rat (false, q + Intt.int 1, Intt.int 1)
   5.124 -    in round a (p div q) end;
   5.125 -
   5.126 -end;
   5.127 -
   5.128 -infix 5 +/; 
   5.129 -infix 5 -/;
   5.130 -infix 7 */;
   5.131 -infix 7 //; 
   5.132 -infix 4 =/ </ <=/ >/ >=/ <>/;
   5.133 -
   5.134 -fun a +/ b = Rat.add a b;
   5.135 -fun a -/ b = a +/ Rat.neg b;
   5.136 -fun a */ b = Rat.mult a b;
   5.137 -fun a // b = a */ Rat.inv b; 
   5.138 -fun a =/ b = Rat.eq (a,b);
   5.139 -fun a </ b = Rat.lt a b;
   5.140 -fun a <=/ b = Rat.le a b;
   5.141 -fun a >/ b = b </ a;
   5.142 -fun a >=/ b = b <=/ a;
   5.143 -fun a <>/ b = not (a =/ b);
     6.1 --- a/src/Pure/library.ML	Tue Jun 05 15:16:11 2007 +0200
     6.2 +++ b/src/Pure/library.ML	Tue Jun 05 15:17:02 2007 +0200
     6.3 @@ -124,8 +124,6 @@
     6.4    val suffixes: 'a list -> 'a list list
     6.5  
     6.6    (*integers*)
     6.7 -  val gcd: IntInf.int * IntInf.int -> IntInf.int
     6.8 -  val lcm: IntInf.int * IntInf.int -> IntInf.int
     6.9    val inc: int ref -> int
    6.10    val dec: int ref -> int
    6.11    val upto: int * int -> int list
    6.12 @@ -639,13 +637,6 @@
    6.13  
    6.14  (** integers **)
    6.15  
    6.16 -fun gcd (x, y) =
    6.17 -  let fun gxd x y : IntInf.int =
    6.18 -    if y = IntInf.fromInt 0 then x else gxd y (x mod y)
    6.19 -  in if x < y then gxd y x else gxd x y end;
    6.20 -
    6.21 -fun lcm (x, y) = (x * y) div gcd (x, y);
    6.22 -
    6.23  fun inc i = (i := ! i + 1; ! i);
    6.24  fun dec i = (i := ! i - 1; ! i);
    6.25  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/float.ML	Tue Jun 05 15:17:02 2007 +0200
     7.3 @@ -0,0 +1,60 @@
     7.4 +(*  Title:      Pure/General/float.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Steven Obua, Florian Haftmann, TU Muenchen
     7.7 +
     7.8 +Implementation of real numbers as mantisse-exponent pairs.
     7.9 +*)
    7.10 +
    7.11 +signature FLOAT =
    7.12 +sig
    7.13 +  type float = Intt.int * Intt.int
    7.14 +  val zero: float
    7.15 +  val eq: float * float -> bool
    7.16 +  val cmp: float * float -> order
    7.17 +  val cmp_zero: float -> order
    7.18 +  val min: float -> float -> float
    7.19 +  val max: float -> float -> float
    7.20 +  val add: float -> float -> float
    7.21 +  val sub: float -> float -> float
    7.22 +  val neg: float -> float
    7.23 +  val mult: float -> float -> float
    7.24 +  val positive_part: float -> float
    7.25 +  val negative_part: float -> float
    7.26 +end;
    7.27 +
    7.28 +structure Float : FLOAT =
    7.29 +struct
    7.30 +
    7.31 +type float = Intt.int * Intt.int;
    7.32 +
    7.33 +val zero = (Intt.zero, Intt.zero);
    7.34 +
    7.35 +fun add (a1, b1) (a2, b2) =
    7.36 +  if Intt.cmp (b1, b2) = LESS then
    7.37 +    (Intt.add a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
    7.38 +  else
    7.39 +    (Intt.add (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
    7.40 +
    7.41 +fun sub (a1, b1) (a2, b2) =
    7.42 +  if Intt.cmp (b1, b2) = LESS then
    7.43 +    (Intt.sub a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
    7.44 +  else
    7.45 +    (Intt.sub (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
    7.46 +
    7.47 +fun neg (a, b) = (Intt.neg a, b);
    7.48 +
    7.49 +fun mult (a1, b1) (a2, b2) = (Intt.mult a1 a2, Intt.add b1 b2);
    7.50 +
    7.51 +fun cmp_zero (a, b) = Intt.cmp_zero a;
    7.52 +
    7.53 +fun cmp (r, s) = cmp_zero (sub r s);
    7.54 +
    7.55 +fun eq (r, s) = cmp (r, s) = EQUAL;
    7.56 +
    7.57 +fun min r s = case cmp (r, s) of LESS => r | _ => s;
    7.58 +fun max r s = case cmp (r, s) of LESS => s | _ => r;
    7.59 +
    7.60 +fun positive_part (a, b) = (Intt.max Intt.zero a, b);
    7.61 +fun negative_part (a, b) = (Intt.min Intt.zero a, b);
    7.62 +
    7.63 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/integer.ML	Tue Jun 05 15:17:02 2007 +0200
     8.3 @@ -0,0 +1,116 @@
     8.4 +(*  Title:      Pure/General/int.ML
     8.5 +    ID:         $Id$
     8.6 +    Author:     Florian Haftmann, TU Muenchen
     8.7 +
     8.8 +Unbounded integers.
     8.9 +*)
    8.10 +
    8.11 +signature INTEGER =
    8.12 +sig
    8.13 +  type int
    8.14 +  val zero: int
    8.15 +  val one: int
    8.16 +  val two: int
    8.17 +  val int: Int.int -> int
    8.18 +  val machine_int: int -> Int.int
    8.19 +  val string_of_int: int -> string
    8.20 +  val int_of_string: string -> int option
    8.21 +  val eq: int * int -> bool
    8.22 +  val cmp: int * int -> order
    8.23 +  val le: int -> int -> bool
    8.24 +  val lt: int -> int -> bool
    8.25 +  val cmp_zero: int -> order
    8.26 +  val min: int -> int -> int
    8.27 +  val max: int -> int -> int
    8.28 +  val inc: int -> int
    8.29 +  val add: int -> int -> int
    8.30 +  val sub: int -> int -> int
    8.31 +  val mult: int -> int -> int
    8.32 +  val divmod: int -> int -> int * int
    8.33 +  val div: int -> int -> int
    8.34 +  val mod: int -> int -> int
    8.35 +  val neg: int -> int
    8.36 +  val signabs: int -> bool * int
    8.37 +  val exp: int -> int
    8.38 +  val log: int -> int
    8.39 +  val pow: int -> int -> int (* exponent -> base -> result *)
    8.40 +  val gcd: int -> int -> int
    8.41 +  val lcm: int -> int -> int
    8.42 +end;
    8.43 +
    8.44 +structure Integer : INTEGER =
    8.45 +struct
    8.46 +
    8.47 +open IntInf;
    8.48 +
    8.49 +val int = fromInt;
    8.50 +
    8.51 +val zero = int 0;
    8.52 +val one = int 1;
    8.53 +val two = int 2;
    8.54 +
    8.55 +val machine_int = toInt;
    8.56 +val string_of_int = toString;
    8.57 +val int_of_string = fromString;
    8.58 +
    8.59 +val eq = op = : int * int -> bool;
    8.60 +val cmp = compare;
    8.61 +val le = curry (op <=);
    8.62 +val lt = curry (op <);
    8.63 +fun cmp_zero k = cmp (k, zero);
    8.64 +
    8.65 +val min = curry min;
    8.66 +val max = curry max;
    8.67 +
    8.68 +val inc = curry (op +) one;
    8.69 +
    8.70 +val add = curry (op +);
    8.71 +val sub = curry (op -);
    8.72 +val mult = curry ( op * );
    8.73 +val divmod = curry divMod;
    8.74 +nonfix div val div = curry div;
    8.75 +nonfix mod val mod = curry mod;
    8.76 +val neg = ~;
    8.77 +
    8.78 +fun signabs k = if cmp_zero k = LESS then (false, neg k) else (true, k);
    8.79 +
    8.80 +fun pow k l =
    8.81 +  let
    8.82 +    fun pw 0 = 1
    8.83 +      | pw k = mult l (pw (sub k 1));
    8.84 +  in if k < zero
    8.85 +    then error "pow: negative exponent"
    8.86 +    else pw k
    8.87 +  end;
    8.88 +
    8.89 +fun exp k = pow k two;
    8.90 +val log = int o log2;
    8.91 +
    8.92 +fun gcd x y =
    8.93 +  let
    8.94 +    fun gxd x y = if y = zero then x else gxd y (mod x y)
    8.95 +  in if lt x y then gxd y x else gxd x y end;
    8.96 +
    8.97 +fun lcm x y = div (mult x y) (gcd x y);
    8.98 +
    8.99 +end;
   8.100 +
   8.101 +type integer = Integer.int;
   8.102 +
   8.103 +infix 7 *%;
   8.104 +infix 6 +% -%; 
   8.105 +infix 4 =% <% <=% >% >=% <>%;
   8.106 +
   8.107 +fun a +% b = Integer.add a b;
   8.108 +fun a -% b = a +% Integer.neg b;
   8.109 +fun a *% b = Integer.mult a b;
   8.110 +fun a =% b = Integer.eq (a, b);
   8.111 +fun a <% b = Integer.lt a b;
   8.112 +fun a <=% b = Integer.le a b;
   8.113 +fun a >% b = b <% a;
   8.114 +fun a >=% b = b <=% a;
   8.115 +fun a <>% b = not (a =% b);
   8.116 +
   8.117 +structure Intt = Integer; (*FIXME*)
   8.118 +val gcd = uncurry Integer.gcd; (*FIXME*)
   8.119 +val lcm = uncurry Integer.lcm; (*FIXME*)
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/rat.ML	Tue Jun 05 15:17:02 2007 +0200
     9.3 @@ -0,0 +1,140 @@
     9.4 +(*  Title:      Pure/General/rat.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Tobias Nipkow, TU Muenchen
     9.7 +
     9.8 +Canonical implementation of exact rational numbers.
     9.9 +*)
    9.10 +
    9.11 +signature RAT =
    9.12 +sig
    9.13 +  type rat
    9.14 +  exception DIVZERO
    9.15 +  val zero: rat
    9.16 +  val one: rat
    9.17 +  val two: rat
    9.18 +  val rat_of_int: Intt.int -> rat
    9.19 +  val rat_of_quotient: Intt.int * Intt.int -> rat
    9.20 +  val quotient_of_rat: rat -> Intt.int * Intt.int
    9.21 +  val string_of_rat: rat -> string
    9.22 +  val eq: rat * rat -> bool
    9.23 +  val cmp: rat * rat -> order
    9.24 +  val le: rat -> rat -> bool
    9.25 +  val lt: rat -> rat -> bool
    9.26 +  val cmp_zero: rat -> order
    9.27 +  val add: rat -> rat -> rat
    9.28 +  val mult: rat -> rat -> rat
    9.29 +  val neg: rat -> rat
    9.30 +  val inv: rat -> rat
    9.31 +  val roundup: rat -> rat
    9.32 +  val rounddown: rat -> rat
    9.33 +end;
    9.34 +
    9.35 +structure Rat : RAT =
    9.36 +struct
    9.37 +
    9.38 +datatype rat = Rat of bool * Intt.int * Intt.int;
    9.39 +
    9.40 +exception DIVZERO;
    9.41 +
    9.42 +val zero = Rat (true, Intt.int 0, Intt.int 1);
    9.43 +val one = Rat (true, Intt.int 1, Intt.int 1);
    9.44 +val two = Rat (true, Intt.int 2, Intt.int 1);
    9.45 +
    9.46 +fun rat_of_int i =
    9.47 +  if i < Intt.int 0
    9.48 +  then Rat (false, ~i, Intt.int 1)
    9.49 +  else Rat (true, i, Intt.int 1);
    9.50 +
    9.51 +fun norm (a, p, q) =
    9.52 +  if p = Intt.int 0 then Rat (true, Intt.int 0, Intt.int 1)
    9.53 +  else
    9.54 +    let
    9.55 +      val absp = abs p
    9.56 +      val m = gcd (absp, q)
    9.57 +    in Rat(a = (Intt.int 0 <= p), absp div m, q div m) end;
    9.58 +
    9.59 +fun common (p1, q1, p2, q2) =
    9.60 +  let val q' = lcm (q1, q2)
    9.61 +  in (p1 * (q' div q1), p2 * (q' div q2), q') end
    9.62 +
    9.63 +fun rat_of_quotient (p, q) =
    9.64 +  if q = Intt.int 0 then raise DIVZERO
    9.65 +  else norm (Intt.int 0 <= q, p, abs q);
    9.66 +
    9.67 +fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~p, q);
    9.68 +
    9.69 +fun string_of_rat r =
    9.70 +  let val (p, q) = quotient_of_rat r
    9.71 +  in Intt.string_of_int p ^ "/" ^ Intt.string_of_int q end;
    9.72 +
    9.73 +fun eq (Rat (false, _, _), Rat (true, _, _)) = false
    9.74 +  | eq (Rat (true, _, _), Rat (false, _, _)) = false
    9.75 +  | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2
    9.76 +
    9.77 +fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
    9.78 +  | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
    9.79 +  | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) =
    9.80 +      let val (r1, r2, _) = common (p1, q1, p2, q2)
    9.81 +      in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end;
    9.82 +
    9.83 +fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end;
    9.84 +fun lt a b = cmp (a, b) = LESS;
    9.85 +
    9.86 +fun cmp_zero (Rat (false, _, _)) = LESS
    9.87 +  | cmp_zero (Rat (_, 0, _)) = EQUAL
    9.88 +  | cmp_zero (Rat (_, _, _)) = GREATER;
    9.89 +
    9.90 +fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
    9.91 +  let
    9.92 +    val (r1, r2, den) = common (p1, q1, p2, q2)
    9.93 +    val num = (if a1 then r1 else ~r1) + (if a2 then r2 else ~r2)
    9.94 +  in norm (true, num, den) end;
    9.95 +
    9.96 +fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
    9.97 +  norm (a1=a2, p1*p2, q1*q2);
    9.98 +
    9.99 +fun neg (r as Rat (b, p, q)) =
   9.100 +  if p = Intt.int 0 then r
   9.101 +  else Rat (not b, p, q);
   9.102 +
   9.103 +fun inv (Rat (a, p, q)) =
   9.104 +  if p = Intt.int 0 then raise DIVZERO
   9.105 +  else Rat (a, q, p);
   9.106 +
   9.107 +fun roundup (r as Rat (a, p, q)) =
   9.108 +  if q = Intt.int 1 then r
   9.109 +  else
   9.110 +    let
   9.111 +      fun round true q = Rat (true, q + Intt.int 1, Intt.int 1)
   9.112 +        | round false q =
   9.113 +            if q = Intt.int 0
   9.114 +            then Rat (true, Intt.int 0, Intt.int 1)
   9.115 +            else Rat (false, q, Intt.int 1);
   9.116 +    in round a (p div q) end;
   9.117 +
   9.118 +fun rounddown (r as Rat (a, p, q)) =
   9.119 +  if q = Intt.int 1 then r
   9.120 +  else
   9.121 +    let
   9.122 +      fun round true q = Rat (true, q, Intt.int 1)
   9.123 +        | round false q = Rat (false, q + Intt.int 1, Intt.int 1)
   9.124 +    in round a (p div q) end;
   9.125 +
   9.126 +end;
   9.127 +
   9.128 +infix 5 +/; 
   9.129 +infix 5 -/;
   9.130 +infix 7 */;
   9.131 +infix 7 //; 
   9.132 +infix 4 =/ </ <=/ >/ >=/ <>/;
   9.133 +
   9.134 +fun a +/ b = Rat.add a b;
   9.135 +fun a -/ b = a +/ Rat.neg b;
   9.136 +fun a */ b = Rat.mult a b;
   9.137 +fun a // b = a */ Rat.inv b; 
   9.138 +fun a =/ b = Rat.eq (a,b);
   9.139 +fun a </ b = Rat.lt a b;
   9.140 +fun a <=/ b = Rat.le a b;
   9.141 +fun a >/ b = b </ a;
   9.142 +fun a >=/ b = b <=/ a;
   9.143 +fun a <>/ b = not (a =/ b);