--- a/src/HOL/Matrix/cplex/fspmlp.ML Fri Jun 29 18:21:25 2007 +0200
+++ b/src/HOL/Matrix/cplex/fspmlp.ML Fri Jun 29 21:23:05 2007 +0200
@@ -125,13 +125,13 @@
fun calc_sure_bound_from_sources g (key as (_, btype)) =
let
fun mult_upper x (lower, upper) =
- if Float.cmp_zero x = LESS then
+ if Float.sign x = LESS then
Float.mult x lower
else
Float.mult x upper
fun mult_lower x (lower, upper) =
- if Float.cmp_zero x = LESS then
+ if Float.sign x = LESS then
Float.mult x upper
else
Float.mult x lower
@@ -240,7 +240,7 @@
UPPER => (Float.neg src_upper, Float.neg src_lower)
| LOWER => src_value
in
- if Float.cmp_zero src_lower = LESS then
+ if Float.sign src_lower = LESS then
add_edge g (src_index, UPPER) dest_key row_index coeff
else
add_edge g (src_index, LOWER) dest_key row_index coeff
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Jun 29 18:21:25 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Jun 29 21:23:05 2007 +0200
@@ -13,7 +13,7 @@
struct
open Conv;
open Normalizer;
-structure Integertab = TableFun(type key = integer val ord = Integer.cmp);
+structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord);
exception COOPER of string * exn;
val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Jun 29 18:21:25 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Jun 29 21:23:05 2007 +0200
@@ -185,13 +185,13 @@
*)
fun ratrelmin2 (x as (r, ler), y as (s, les)) =
- case Rat.cmp (r, s)
+ case Rat.ord (r, s)
of EQUAL => (r, (not ler) andalso (not les))
| LESS => x
| GREATER => y;
fun ratrelmax2 (x as (r, ler), y as (s, les)) =
- case Rat.cmp (r, s)
+ case Rat.ord (r, s)
of EQUAL => (r, ler andalso les)
| LESS => y
| GREATER => x;
@@ -209,7 +209,7 @@
fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two);
fun choose2 d ((lb, exactl), (ub, exactu)) =
- let val ord = Rat.cmp_zero lb in
+ let val ord = Rat.sign lb in
if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu)
then Rat.zero
else if not d then
@@ -237,19 +237,19 @@
map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le,
nth_map v (K Rat.zero) bs));
-fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs
+fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.sign) cs
of [x] => x =/ nth cs v
| _ => false;
(* The base case:
all variables occur only with positive or only with negative coefficients *)
fun pick_vars discr (ineqs,ex) =
- let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.cmp_zero) cs) ineqs
+ let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.sign) cs) ineqs
in case nz of [] => ex
| (_,_,cs) :: _ =>
- let val v = find_index (not o curry (op =) EQUAL o Rat.cmp_zero) cs
+ let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs
val d = nth discr v;
- val pos = not (Rat.cmp_zero (nth cs v) = LESS);
+ val pos = not (Rat.sign (nth cs v) = LESS);
val sv = filter (single_var v) nz;
val minmax =
if pos then if d then Rat.roundup o fst o ratrelmax
--- a/src/Tools/float.ML Fri Jun 29 18:21:25 2007 +0200
+++ b/src/Tools/float.ML Fri Jun 29 21:23:05 2007 +0200
@@ -10,8 +10,8 @@
type float = integer * integer
val zero: float
val eq: float * float -> bool
- val cmp: float * float -> order
- val cmp_zero: float -> order
+ val ord: float * float -> order
+ val sign: float -> order
val min: float -> float -> float
val max: float -> float -> float
val add: float -> float -> float
@@ -30,13 +30,13 @@
val zero: float = (0, 0);
fun add (a1, b1) (a2, b2) =
- if Integer.cmp (b1, b2) = LESS then
+ if Integer.ord (b1, b2) = LESS then
(a1 +% a2 *% Integer.exp (b2 -% b1), b1)
else
(a1 *% Integer.exp (b1 -% b2) +% a2, b2);
fun sub (a1, b1) (a2, b2) =
- if Integer.cmp (b1, b2) = LESS then
+ if Integer.ord (b1, b2) = LESS then
(a1 -% a2 *% Integer.exp (b2 -% b1), b1)
else
(a1 *% Integer.exp (b1 -% b2) -% a2, b2);
@@ -45,14 +45,14 @@
fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
-fun cmp_zero (a, b) = Integer.cmp_zero a;
+fun sign (a, b) = Integer.sign a;
-fun cmp (r, s) = cmp_zero (sub r s);
+fun ord (r, s) = sign (sub r s);
-fun eq (r, s) = cmp (r, s) = EQUAL;
+fun eq (r, s) = ord (r, s) = EQUAL;
-fun min r s = case cmp (r, s) of LESS => r | _ => s;
-fun max r s = case cmp (r, s) of LESS => s | _ => r;
+fun min r s = case ord (r, s) of LESS => r | _ => s;
+fun max r s = case ord (r, s) of LESS => s | _ => r;
fun positive_part (a, b) = (Integer.max 0 a, b);
fun negative_part (a, b) = (Integer.min 0 a, b);
--- a/src/Tools/integer.ML Fri Jun 29 18:21:25 2007 +0200
+++ b/src/Tools/integer.ML Fri Jun 29 21:23:05 2007 +0200
@@ -16,10 +16,12 @@
val string_of_int: int -> string
val int_of_string: string -> int option
val eq: int * int -> bool
- val cmp: int * int -> order
+ val ord: int * int -> order
val le: int -> int -> bool
val lt: int -> int -> bool
- val cmp_zero: int -> order
+ val signabs: int -> order * int
+ val sign: int -> order
+ val abs: int -> int
val min: int -> int -> int
val max: int -> int -> int
val inc: int -> int
@@ -30,7 +32,6 @@
val div: int -> int -> int
val mod: int -> int -> int
val neg: int -> int
- val signabs: int -> bool * int
val exp: int -> int
val log: int -> int
val pow: int -> int -> int (* exponent -> base -> result *)
@@ -43,8 +44,6 @@
open IntInf;
-type integer = int;
-
val int = fromInt;
val zero = int 0;
@@ -56,10 +55,12 @@
val int_of_string = fromString;
val eq = op = : int * int -> bool;
-val cmp = compare;
+val ord = compare;
val le = curry (op <=);
val lt = curry (op <);
-fun cmp_zero k = cmp (k, zero);
+
+fun sign k = ord (k, zero);
+fun signabs k = (ord (k, zero), abs k);
val min = curry min;
val max = curry max;
@@ -74,15 +75,18 @@
nonfix mod val mod = curry mod;
val neg = ~;
-fun signabs k = if cmp_zero k = LESS then (false, neg k) else (true, k);
-
fun pow k l =
let
- fun pw 0 = 1
- | pw k = mult l (pw (sub k 1));
+ fun pw 0 _ = 1
+ | pw 1 l = l
+ | pw k l =
+ let
+ val (k', r) = divmod k 2;
+ val l' = pw k' (mult l l);
+ in if r = 0 then l' else mult l' l end;
in if k < zero
then error "pow: negative exponent"
- else pw k
+ else pw k l
end;
fun exp k = pow k two;
--- a/src/Tools/rat.ML Fri Jun 29 18:21:25 2007 +0200
+++ b/src/Tools/rat.ML Fri Jun 29 21:23:05 2007 +0200
@@ -1,6 +1,6 @@
(* Title: Pure/General/rat.ML
ID: $Id$
- Author: Tobias Nipkow, TU Muenchen
+ Author: Tobias Nipkow, Florian Haftmann, TU Muenchen
Canonical implementation of exact rational numbers.
*)
@@ -17,113 +17,90 @@
val quotient_of_rat: rat -> integer * integer
val string_of_rat: rat -> string
val eq: rat * rat -> bool
- val cmp: rat * rat -> order
+ val ord: rat * rat -> order
val le: rat -> rat -> bool
val lt: rat -> rat -> bool
- val cmp_zero: rat -> order
+ val signabs: rat -> order * rat
+ val sign: rat -> order
+ val abs: rat -> rat
val add: rat -> rat -> rat
val mult: rat -> rat -> rat
val neg: rat -> rat
val inv: rat -> rat
+ val rounddown: rat -> rat
val roundup: rat -> rat
- val rounddown: rat -> rat
end;
structure Rat : RAT =
struct
-datatype rat = Rat of bool * integer * integer;
+fun common (p1, q1) (p2, q2) =
+ let
+ val m = Integer.lcm q1 q2;
+ in ((Integer.mult p1 (Integer.div m q1), Integer.mult p2 (Integer.div m q2)), m) end;
+
+datatype rat = Rat of integer * integer; (* nominator, denominator (positive!) *)
exception DIVZERO;
-val zero = Rat (true, 0, 1);
-val one = Rat (true, 1, 1);
-val two = Rat (true, 2, 1);
-
-fun rat_of_int i =
- let
- val (a, p) = Integer.signabs i
- in Rat (a, p, 1) end;
-
-fun norm (a, p, q) =
- if p = 0 then Rat (true, 0, 1)
- else
- let
- val (b, absp) = Integer.signabs p;
- val m = Integer.gcd absp q;
- in Rat (a = b, absp div m, q div m) end;
-
-fun common (p1, q1, p2, q2) =
- let
- val q' = Integer.lcm q1 q2;
- in (p1 * (q' div q1), p2 * (q' div q2), q') end
-
fun rat_of_quotient (p, q) =
let
- val (a, absq) = Integer.signabs q;
- in
- if absq = 0 then raise DIVZERO
- else norm (a, p, absq)
- end;
+ val m = Integer.gcd (Integer.abs p) q
+ in Rat (Integer.div p m, Integer.div q m) end handle Div => raise DIVZERO;
+
+fun quotient_of_rat (Rat r) = r;
+
+fun rat_of_int i = Rat (i, 1);
-fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~ p, q);
+val zero = rat_of_int 0;
+val one = rat_of_int 1;
+val two = rat_of_int 2;
-fun string_of_rat r =
- let
- val (p, q) = quotient_of_rat r;
- in Integer.string_of_int p ^ "/" ^ Integer.string_of_int q end;
+fun string_of_rat (Rat (p, q)) =
+ Integer.string_of_int p ^ "/" ^ Integer.string_of_int q;
+
+fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
-fun eq (Rat (false, _, _), Rat (true, _, _)) = false
- | eq (Rat (true, _, _), Rat (false, _, _)) = false
- | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2;
+fun ord (Rat (p1, q1), Rat (p2, q2)) = case (Integer.sign p1, Integer.sign p2)
+ of (LESS, EQUAL) => LESS
+ | (LESS, GREATER) => LESS
+ | (EQUAL, LESS) => GREATER
+ | (EQUAL, EQUAL) => EQUAL
+ | (EQUAL, GREATER) => LESS
+ | (GREATER, LESS) => GREATER
+ | (GREATER, EQUAL) => GREATER
+ | _ => Integer.ord (fst (common (p1, q1) (p2, q2)));
-fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
- | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
- | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) =
- let val (r1, r2, _) = common (p1, q1, p2, q2)
- in if a then Integer.cmp (r1, r2) else Integer.cmp (r2, r1) end;
+fun le a b = not (ord (a, b) = GREATER);
+fun lt a b = (ord (a, b) = LESS);
-fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end;
-fun lt a b = (cmp (a, b) = LESS);
+fun sign (Rat (p, _)) = Integer.sign p;
-fun cmp_zero (Rat (false, _, _)) = LESS
- | cmp_zero (Rat (_, 0, _)) = EQUAL
- | cmp_zero (Rat (_, _, _)) = GREATER;
+fun abs (Rat (p, q)) = Rat (Integer.abs p, q);
-fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
+fun signabs (Rat (p, q)) =
let
- val (r1, r2, den) = common (p1, q1, p2, q2);
- val num = (if a1 then r1 else ~ r1)
- + (if a2 then r2 else ~ r2);
- in norm (true, num, den) end;
-
-fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
- norm (a1 = a2, p1 * p2, q1 * q2);
+ val (s, p') = Integer.signabs p;
+ in (s, Rat (p', q)) end;
-fun neg (r as Rat (b, p, q)) =
- if p = 0 then r
- else Rat (not b, p, q);
+fun add (Rat (p1, q1)) (Rat (p2, q2)) =
+ let
+ val ((m1, m2), n) = common (p1, q1) (p2, q2);
+ in rat_of_quotient (Integer.add m1 m2, n) end;
-fun inv (Rat (a, p, q)) =
- if q = 0 then raise DIVZERO
- else Rat (a, q, p);
+fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
+ rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2);
-fun roundup (r as Rat (a, p, q)) =
- if q = 1 then r
- else
- let
- fun round true q = Rat (true, q + 1, 1)
- | round false q =
- Rat (q = 0, 0, 1);
- in round a (p div q) end;
+fun neg (Rat (p, q)) = Rat (Integer.neg p, q);
+
+fun inv (Rat (p, 0)) = raise DIVZERO
+ | inv (Rat (p, q)) = Rat (q, p);
-fun rounddown (r as Rat (a, p, q)) =
- if q = 1 then r
- else
- let
- fun round true q = Rat (true, q, 1)
- | round false q = Rat (false, q + 1, 1)
- in round a (p div q) end;
+fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1);
+
+fun roundup (Rat (p, q)) = case Integer.divmod p q
+ of (m, 0) => Rat (m, 1)
+ | (m, _) => Rat (m + 1, 1);
end;