src/Tools/integer.ML
changeset 23520 483fe92f00c1
parent 23517 93d1ad7662a9
child 24584 01e83ffa6c54
--- 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;