# HG changeset patch
# User wenzelm
# Date 1510686767 -3600
# Node ID 5da20135f56018827ae18effd4b5f3f001c3c4a8
# Parent  74bd55f1206d844685999cdb9cce85c272876a39
slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore (amending 2288cc39b038)

diff -r 74bd55f1206d -r 5da20135f560 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Tue Nov 14 16:17:08 2017 +0100
+++ b/src/Pure/General/integer.ML	Tue Nov 14 20:12:47 2017 +0100
@@ -40,7 +40,20 @@
 
 fun square x = x * x;
 
-fun pow k l = IntInf.pow (l, k);
+fun pow k l =
+  let
+    fun pw 0 _ = 1
+      | pw 1 l = l
+      | pw k l =
+          let
+            val (k', r) = div_mod k 2;
+            val l' = pw k' (l * l);
+          in if r = 0 then l' else l' * l end;
+  in
+    if k < 0
+    then IntInf.pow (l, k)
+    else pw k l
+  end;
 
 fun gcd x y = PolyML.IntInf.gcd (x, y);
 fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
@@ -52,3 +65,10 @@
   | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
 
 end;
+
+(*slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore*)
+structure IntInf =
+struct
+  open IntInf;
+  fun pow (i, n) = Integer.pow n i;
+end;