src/Pure/General/integer.ML
author wenzelm
Tue Nov 14 20:12:47 2017 +0100 (20 months ago)
changeset 67074 5da20135f560
parent 67033 2288cc39b038
child 68028 1f9f973eed2a
permissions -rw-r--r--
slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore (amending 2288cc39b038)
haftmann@28308
     1
(*  Title:      Pure/General/integer.ML
wenzelm@24633
     2
    Author:     Florian Haftmann, TU Muenchen
wenzelm@24633
     3
wenzelm@33002
     4
Auxiliary operations on (unbounded) integers.
wenzelm@24633
     5
*)
wenzelm@24633
     6
wenzelm@24633
     7
signature INTEGER =
wenzelm@24633
     8
sig
wenzelm@33029
     9
  val min: int -> int -> int
wenzelm@33029
    10
  val max: int -> int -> int
wenzelm@33002
    11
  val add: int -> int -> int
wenzelm@33002
    12
  val mult: int -> int -> int
wenzelm@33002
    13
  val sum: int list -> int
wenzelm@33002
    14
  val prod: int list -> int
wenzelm@24633
    15
  val sign: int -> order
wenzelm@24633
    16
  val div_mod: int -> int -> int * int
wenzelm@24633
    17
  val square: int -> int
wenzelm@24633
    18
  val pow: int -> int -> int (* exponent -> base -> result *)
wenzelm@24633
    19
  val gcd: int -> int -> int
wenzelm@63227
    20
  val lcm: int -> int -> int
wenzelm@24633
    21
  val gcds: int list -> int
wenzelm@24633
    22
  val lcms: int list -> int
wenzelm@24633
    23
end;
wenzelm@24633
    24
wenzelm@24633
    25
structure Integer : INTEGER =
wenzelm@24633
    26
struct
wenzelm@24633
    27
wenzelm@33029
    28
fun min x y = Int.min (x, y);
wenzelm@33029
    29
fun max x y = Int.max (x, y);
wenzelm@33029
    30
wenzelm@33002
    31
fun add x y = x + y;
wenzelm@33002
    32
fun mult x y = x * y;
wenzelm@24633
    33
wenzelm@33002
    34
fun sum xs = fold add xs 0;
wenzelm@33002
    35
fun prod xs = fold mult xs 1;
wenzelm@33002
    36
wenzelm@33002
    37
fun sign x = int_ord (x, 0);
wenzelm@24633
    38
wenzelm@24633
    39
fun div_mod x y = IntInf.divMod (x, y);
wenzelm@24633
    40
wenzelm@24633
    41
fun square x = x * x;
wenzelm@24633
    42
wenzelm@67074
    43
fun pow k l =
wenzelm@67074
    44
  let
wenzelm@67074
    45
    fun pw 0 _ = 1
wenzelm@67074
    46
      | pw 1 l = l
wenzelm@67074
    47
      | pw k l =
wenzelm@67074
    48
          let
wenzelm@67074
    49
            val (k', r) = div_mod k 2;
wenzelm@67074
    50
            val l' = pw k' (l * l);
wenzelm@67074
    51
          in if r = 0 then l' else l' * l end;
wenzelm@67074
    52
  in
wenzelm@67074
    53
    if k < 0
wenzelm@67074
    54
    then IntInf.pow (l, k)
wenzelm@67074
    55
    else pw k l
wenzelm@67074
    56
  end;
wenzelm@24633
    57
wenzelm@63227
    58
fun gcd x y = PolyML.IntInf.gcd (x, y);
wenzelm@63227
    59
fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
wenzelm@24633
    60
wenzelm@63227
    61
fun gcds [] = 0
wenzelm@63227
    62
  | gcds (x :: xs) = fold gcd xs x;
wenzelm@24633
    63
wenzelm@63227
    64
fun lcms [] = 1
wenzelm@63227
    65
  | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
wenzelm@24633
    66
wenzelm@24633
    67
end;
wenzelm@67074
    68
wenzelm@67074
    69
(*slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore*)
wenzelm@67074
    70
structure IntInf =
wenzelm@67074
    71
struct
wenzelm@67074
    72
  open IntInf;
wenzelm@67074
    73
  fun pow (i, n) = Integer.pow n i;
wenzelm@67074
    74
end;