tuned arithmetic modules
authorhaftmann
Fri Jun 29 21:23:05 2007 +0200 (2007-06-29)
changeset 23520483fe92f00c1
parent 23519 a4ffa756d8eb
child 23521 195fe3fe2831
tuned arithmetic modules
src/HOL/Matrix/cplex/fspmlp.ML
src/HOL/Tools/Qelim/cooper.ML
src/Provers/Arith/fast_lin_arith.ML
src/Tools/float.ML
src/Tools/integer.ML
src/Tools/rat.ML
     1.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML	Fri Jun 29 18:21:25 2007 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML	Fri Jun 29 21:23:05 2007 +0200
     1.3 @@ -125,13 +125,13 @@
     1.4          fun calc_sure_bound_from_sources g (key as (_, btype)) =
     1.5              let
     1.6                  fun mult_upper x (lower, upper) =
     1.7 -                    if Float.cmp_zero x = LESS then
     1.8 +                    if Float.sign x = LESS then
     1.9                          Float.mult x lower
    1.10                      else
    1.11                          Float.mult x upper
    1.12  
    1.13                  fun mult_lower x (lower, upper) =
    1.14 -                    if Float.cmp_zero x = LESS then
    1.15 +                    if Float.sign x = LESS then
    1.16                          Float.mult x upper
    1.17                      else
    1.18                          Float.mult x lower
    1.19 @@ -240,7 +240,7 @@
    1.20                                                              UPPER => (Float.neg src_upper, Float.neg src_lower)
    1.21                                                            | LOWER => src_value
    1.22                                          in
    1.23 -                                            if Float.cmp_zero src_lower = LESS then
    1.24 +                                            if Float.sign src_lower = LESS then
    1.25                                                  add_edge g (src_index, UPPER) dest_key row_index coeff
    1.26                                              else
    1.27                                                  add_edge g (src_index, LOWER) dest_key row_index coeff
     2.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Jun 29 18:21:25 2007 +0200
     2.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Jun 29 21:23:05 2007 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  struct
     2.5  open Conv;
     2.6  open Normalizer;
     2.7 -structure Integertab = TableFun(type key = integer val ord = Integer.cmp);
     2.8 +structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord);
     2.9  exception COOPER of string * exn;
    2.10  val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
    2.11  
     3.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 29 18:21:25 2007 +0200
     3.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 29 21:23:05 2007 +0200
     3.3 @@ -185,13 +185,13 @@
     3.4  *)
     3.5  
     3.6  fun ratrelmin2 (x as (r, ler), y as (s, les)) =
     3.7 -  case Rat.cmp (r, s)
     3.8 +  case Rat.ord (r, s)
     3.9     of EQUAL => (r, (not ler) andalso (not les))
    3.10      | LESS => x
    3.11      | GREATER => y;
    3.12  
    3.13  fun ratrelmax2 (x as (r, ler), y as (s, les)) =
    3.14 -  case Rat.cmp (r, s)
    3.15 +  case Rat.ord (r, s)
    3.16     of EQUAL => (r, ler andalso les)
    3.17      | LESS => y
    3.18      | GREATER => x;
    3.19 @@ -209,7 +209,7 @@
    3.20  fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two);
    3.21  
    3.22  fun choose2 d ((lb, exactl), (ub, exactu)) =
    3.23 -  let val ord = Rat.cmp_zero lb in
    3.24 +  let val ord = Rat.sign lb in
    3.25    if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu)
    3.26      then Rat.zero
    3.27      else if not d then
    3.28 @@ -237,19 +237,19 @@
    3.29    map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le,
    3.30                          nth_map v (K Rat.zero) bs));
    3.31  
    3.32 -fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs
    3.33 +fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.sign) cs
    3.34   of [x] => x =/ nth cs v
    3.35    | _ => false;
    3.36  
    3.37  (* The base case:
    3.38     all variables occur only with positive or only with negative coefficients *)
    3.39  fun pick_vars discr (ineqs,ex) =
    3.40 -  let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.cmp_zero) cs) ineqs
    3.41 +  let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.sign) cs) ineqs
    3.42    in case nz of [] => ex
    3.43       | (_,_,cs) :: _ =>
    3.44 -       let val v = find_index (not o curry (op =) EQUAL o Rat.cmp_zero) cs
    3.45 +       let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs
    3.46             val d = nth discr v;
    3.47 -           val pos = not (Rat.cmp_zero (nth cs v) = LESS);
    3.48 +           val pos = not (Rat.sign (nth cs v) = LESS);
    3.49             val sv = filter (single_var v) nz;
    3.50             val minmax =
    3.51               if pos then if d then Rat.roundup o fst o ratrelmax
     4.1 --- a/src/Tools/float.ML	Fri Jun 29 18:21:25 2007 +0200
     4.2 +++ b/src/Tools/float.ML	Fri Jun 29 21:23:05 2007 +0200
     4.3 @@ -10,8 +10,8 @@
     4.4    type float = integer * integer
     4.5    val zero: float
     4.6    val eq: float * float -> bool
     4.7 -  val cmp: float * float -> order
     4.8 -  val cmp_zero: float -> order
     4.9 +  val ord: float * float -> order
    4.10 +  val sign: float -> order
    4.11    val min: float -> float -> float
    4.12    val max: float -> float -> float
    4.13    val add: float -> float -> float
    4.14 @@ -30,13 +30,13 @@
    4.15  val zero: float = (0, 0);
    4.16  
    4.17  fun add (a1, b1) (a2, b2) =
    4.18 -  if Integer.cmp (b1, b2) = LESS then
    4.19 +  if Integer.ord (b1, b2) = LESS then
    4.20      (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
    4.21    else
    4.22      (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
    4.23  
    4.24  fun sub (a1, b1) (a2, b2) =
    4.25 -  if Integer.cmp (b1, b2) = LESS then
    4.26 +  if Integer.ord (b1, b2) = LESS then
    4.27      (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
    4.28    else
    4.29      (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
    4.30 @@ -45,14 +45,14 @@
    4.31  
    4.32  fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
    4.33  
    4.34 -fun cmp_zero (a, b) = Integer.cmp_zero a;
    4.35 +fun sign (a, b) = Integer.sign a;
    4.36  
    4.37 -fun cmp (r, s) = cmp_zero (sub r s);
    4.38 +fun ord (r, s) = sign (sub r s);
    4.39  
    4.40 -fun eq (r, s) = cmp (r, s) = EQUAL;
    4.41 +fun eq (r, s) = ord (r, s) = EQUAL;
    4.42  
    4.43 -fun min r s = case cmp (r, s) of LESS => r | _ => s;
    4.44 -fun max r s = case cmp (r, s) of LESS => s | _ => r;
    4.45 +fun min r s = case ord (r, s) of LESS => r | _ => s;
    4.46 +fun max r s = case ord (r, s) of LESS => s | _ => r;
    4.47  
    4.48  fun positive_part (a, b) = (Integer.max 0 a, b);
    4.49  fun negative_part (a, b) = (Integer.min 0 a, b);
     5.1 --- a/src/Tools/integer.ML	Fri Jun 29 18:21:25 2007 +0200
     5.2 +++ b/src/Tools/integer.ML	Fri Jun 29 21:23:05 2007 +0200
     5.3 @@ -16,10 +16,12 @@
     5.4    val string_of_int: int -> string
     5.5    val int_of_string: string -> int option
     5.6    val eq: int * int -> bool
     5.7 -  val cmp: int * int -> order
     5.8 +  val ord: int * int -> order
     5.9    val le: int -> int -> bool
    5.10    val lt: int -> int -> bool
    5.11 -  val cmp_zero: int -> order
    5.12 +  val signabs: int -> order * int
    5.13 +  val sign: int -> order
    5.14 +  val abs: int -> int
    5.15    val min: int -> int -> int
    5.16    val max: int -> int -> int
    5.17    val inc: int -> int
    5.18 @@ -30,7 +32,6 @@
    5.19    val div: int -> int -> int
    5.20    val mod: int -> int -> int
    5.21    val neg: int -> int
    5.22 -  val signabs: int -> bool * int
    5.23    val exp: int -> int
    5.24    val log: int -> int
    5.25    val pow: int -> int -> int (* exponent -> base -> result *)
    5.26 @@ -43,8 +44,6 @@
    5.27  
    5.28  open IntInf;
    5.29  
    5.30 -type integer = int;
    5.31 -
    5.32  val int = fromInt;
    5.33  
    5.34  val zero = int 0;
    5.35 @@ -56,10 +55,12 @@
    5.36  val int_of_string = fromString;
    5.37  
    5.38  val eq = op = : int * int -> bool;
    5.39 -val cmp = compare;
    5.40 +val ord = compare;
    5.41  val le = curry (op <=);
    5.42  val lt = curry (op <);
    5.43 -fun cmp_zero k = cmp (k, zero);
    5.44 +
    5.45 +fun sign k = ord (k, zero);
    5.46 +fun signabs k = (ord (k, zero), abs k);
    5.47  
    5.48  val min = curry min;
    5.49  val max = curry max;
    5.50 @@ -74,15 +75,18 @@
    5.51  nonfix mod val mod = curry mod;
    5.52  val neg = ~;
    5.53  
    5.54 -fun signabs k = if cmp_zero k = LESS then (false, neg k) else (true, k);
    5.55 -
    5.56  fun pow k l =
    5.57    let
    5.58 -    fun pw 0 = 1
    5.59 -      | pw k = mult l (pw (sub k 1));
    5.60 +    fun pw 0 _ = 1
    5.61 +      | pw 1 l = l
    5.62 +      | pw k l =
    5.63 +          let
    5.64 +            val (k', r) = divmod k 2;
    5.65 +            val l' = pw k' (mult l l);
    5.66 +          in if r = 0 then l' else mult l' l end;
    5.67    in if k < zero
    5.68      then error "pow: negative exponent"
    5.69 -    else pw k
    5.70 +    else pw k l
    5.71    end;
    5.72  
    5.73  fun exp k = pow k two;
     6.1 --- a/src/Tools/rat.ML	Fri Jun 29 18:21:25 2007 +0200
     6.2 +++ b/src/Tools/rat.ML	Fri Jun 29 21:23:05 2007 +0200
     6.3 @@ -1,6 +1,6 @@
     6.4  (*  Title:      Pure/General/rat.ML
     6.5      ID:         $Id$
     6.6 -    Author:     Tobias Nipkow, TU Muenchen
     6.7 +    Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
     6.8  
     6.9  Canonical implementation of exact rational numbers.
    6.10  *)
    6.11 @@ -17,113 +17,90 @@
    6.12    val quotient_of_rat: rat -> integer * integer
    6.13    val string_of_rat: rat -> string
    6.14    val eq: rat * rat -> bool
    6.15 -  val cmp: rat * rat -> order
    6.16 +  val ord: rat * rat -> order
    6.17    val le: rat -> rat -> bool
    6.18    val lt: rat -> rat -> bool
    6.19 -  val cmp_zero: rat -> order
    6.20 +  val signabs: rat -> order * rat
    6.21 +  val sign: rat -> order
    6.22 +  val abs: rat -> rat
    6.23    val add: rat -> rat -> rat
    6.24    val mult: rat -> rat -> rat
    6.25    val neg: rat -> rat
    6.26    val inv: rat -> rat
    6.27 +  val rounddown: rat -> rat
    6.28    val roundup: rat -> rat
    6.29 -  val rounddown: rat -> rat
    6.30  end;
    6.31  
    6.32  structure Rat : RAT =
    6.33  struct
    6.34  
    6.35 -datatype rat = Rat of bool * integer * integer;
    6.36 +fun common (p1, q1) (p2, q2) =
    6.37 +  let
    6.38 +    val m = Integer.lcm q1 q2;
    6.39 +  in ((Integer.mult p1 (Integer.div m q1), Integer.mult p2 (Integer.div m q2)), m) end;
    6.40 +
    6.41 +datatype rat = Rat of integer * integer; (* nominator, denominator (positive!) *)
    6.42  
    6.43  exception DIVZERO;
    6.44  
    6.45 -val zero = Rat (true, 0, 1);
    6.46 -val one = Rat (true, 1, 1);
    6.47 -val two = Rat (true, 2, 1);
    6.48 -
    6.49 -fun rat_of_int i =
    6.50 -  let
    6.51 -    val (a, p) = Integer.signabs i
    6.52 -  in Rat (a, p, 1) end;
    6.53 -
    6.54 -fun norm (a, p, q) =
    6.55 -  if p = 0 then Rat (true, 0, 1)
    6.56 -  else
    6.57 -    let
    6.58 -      val (b, absp) = Integer.signabs p;
    6.59 -      val m = Integer.gcd absp q;
    6.60 -    in Rat (a = b, absp div m, q div m) end;
    6.61 -
    6.62 -fun common (p1, q1, p2, q2) =
    6.63 -  let
    6.64 -    val q' = Integer.lcm q1 q2;
    6.65 -  in (p1 * (q' div q1), p2 * (q' div q2), q') end
    6.66 -
    6.67  fun rat_of_quotient (p, q) =
    6.68    let
    6.69 -    val (a, absq) = Integer.signabs q;
    6.70 -  in
    6.71 -    if absq = 0 then raise DIVZERO
    6.72 -    else norm (a, p, absq)
    6.73 -  end;
    6.74 +    val m = Integer.gcd (Integer.abs p) q
    6.75 +  in Rat (Integer.div p m, Integer.div q m) end handle Div => raise DIVZERO;
    6.76 +
    6.77 +fun quotient_of_rat (Rat r) = r;
    6.78 +
    6.79 +fun rat_of_int i = Rat (i, 1);
    6.80  
    6.81 -fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~ p, q);
    6.82 +val zero = rat_of_int 0;
    6.83 +val one = rat_of_int 1;
    6.84 +val two = rat_of_int 2;
    6.85  
    6.86 -fun string_of_rat r =
    6.87 -  let
    6.88 -    val (p, q) = quotient_of_rat r;
    6.89 -  in Integer.string_of_int p ^ "/" ^ Integer.string_of_int q end;
    6.90 +fun string_of_rat (Rat (p, q)) =
    6.91 +  Integer.string_of_int p ^ "/" ^ Integer.string_of_int q;
    6.92 +
    6.93 +fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
    6.94  
    6.95 -fun eq (Rat (false, _, _), Rat (true, _, _)) = false
    6.96 -  | eq (Rat (true, _, _), Rat (false, _, _)) = false
    6.97 -  | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2;
    6.98 +fun ord (Rat (p1, q1), Rat (p2, q2)) = case (Integer.sign p1, Integer.sign p2)
    6.99 + of (LESS, EQUAL) => LESS
   6.100 +  | (LESS, GREATER) => LESS
   6.101 +  | (EQUAL, LESS) => GREATER
   6.102 +  | (EQUAL, EQUAL) => EQUAL
   6.103 +  | (EQUAL, GREATER) => LESS
   6.104 +  | (GREATER, LESS) => GREATER
   6.105 +  | (GREATER, EQUAL) => GREATER
   6.106 +  | _ => Integer.ord (fst (common (p1, q1) (p2, q2)));
   6.107  
   6.108 -fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
   6.109 -  | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
   6.110 -  | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) =
   6.111 -      let val (r1, r2, _) = common (p1, q1, p2, q2)
   6.112 -      in if a then Integer.cmp (r1, r2) else Integer.cmp (r2, r1) end;
   6.113 +fun le a b = not (ord (a, b) = GREATER);
   6.114 +fun lt a b = (ord (a, b) = LESS);
   6.115  
   6.116 -fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end;
   6.117 -fun lt a b = (cmp (a, b) = LESS);
   6.118 +fun sign (Rat (p, _)) = Integer.sign p;
   6.119  
   6.120 -fun cmp_zero (Rat (false, _, _)) = LESS
   6.121 -  | cmp_zero (Rat (_, 0, _)) = EQUAL
   6.122 -  | cmp_zero (Rat (_, _, _)) = GREATER;
   6.123 +fun abs (Rat (p, q)) = Rat (Integer.abs p, q);
   6.124  
   6.125 -fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
   6.126 +fun signabs (Rat (p, q)) =
   6.127    let
   6.128 -    val (r1, r2, den) = common (p1, q1, p2, q2);
   6.129 -    val num = (if a1 then r1 else ~ r1)
   6.130 -      + (if a2 then r2 else ~ r2);
   6.131 -  in norm (true, num, den) end;
   6.132 -
   6.133 -fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
   6.134 -  norm (a1 = a2, p1 * p2, q1 * q2);
   6.135 +    val (s, p') = Integer.signabs p;
   6.136 +  in (s, Rat (p', q)) end;
   6.137  
   6.138 -fun neg (r as Rat (b, p, q)) =
   6.139 -  if p = 0 then r
   6.140 -  else Rat (not b, p, q);
   6.141 +fun add (Rat (p1, q1)) (Rat (p2, q2)) =
   6.142 +  let
   6.143 +    val ((m1, m2), n) = common (p1, q1) (p2, q2);
   6.144 +  in rat_of_quotient (Integer.add m1 m2, n) end;
   6.145  
   6.146 -fun inv (Rat (a, p, q)) =
   6.147 -  if q = 0 then raise DIVZERO
   6.148 -  else Rat (a, q, p);
   6.149 +fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
   6.150 +  rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2);
   6.151  
   6.152 -fun roundup (r as Rat (a, p, q)) =
   6.153 -  if q = 1 then r
   6.154 -  else
   6.155 -    let
   6.156 -      fun round true q = Rat (true, q + 1, 1)
   6.157 -        | round false q =
   6.158 -            Rat (q = 0, 0, 1);
   6.159 -    in round a (p div q) end;
   6.160 +fun neg (Rat (p, q)) = Rat (Integer.neg p, q);
   6.161 +
   6.162 +fun inv (Rat (p, 0)) = raise DIVZERO
   6.163 +  | inv (Rat (p, q)) = Rat (q, p);
   6.164  
   6.165 -fun rounddown (r as Rat (a, p, q)) =
   6.166 -  if q = 1 then r
   6.167 -  else
   6.168 -    let
   6.169 -      fun round true q = Rat (true, q, 1)
   6.170 -        | round false q = Rat (false, q + 1, 1)
   6.171 -    in round a (p div q) end;
   6.172 +fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1);
   6.173 +
   6.174 +fun roundup (Rat (p, q)) = case Integer.divmod p q
   6.175 + of (m, 0) => Rat (m, 1)
   6.176 +  | (m, _) => Rat (m + 1, 1);
   6.177  
   6.178  end;
   6.179