src/Tools/integer.ML
author haftmann
Tue, 05 Jun 2007 15:17:02 +0200
changeset 23251 471b576aad25
child 23298 404988d8b1e0
permissions -rw-r--r--
moved generic algebra modules
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/General/int.ML
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     2
    ID:         $Id$
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     4
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     5
Unbounded integers.
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     6
*)
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     7
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     8
signature INTEGER =
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     9
sig
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    10
  type int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    11
  val zero: int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    12
  val one: int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    13
  val two: int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    14
  val int: Int.int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    15
  val machine_int: int -> Int.int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    16
  val string_of_int: int -> string
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    17
  val int_of_string: string -> int option
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    18
  val eq: int * int -> bool
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    19
  val cmp: int * int -> order
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    20
  val le: int -> int -> bool
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    21
  val lt: int -> int -> bool
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    22
  val cmp_zero: int -> order
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    23
  val min: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    24
  val max: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    25
  val inc: int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    26
  val add: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    27
  val sub: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    28
  val mult: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    29
  val divmod: int -> int -> int * int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    30
  val div: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    31
  val mod: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    32
  val neg: int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    33
  val signabs: int -> bool * int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    34
  val exp: int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    35
  val log: int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    36
  val pow: int -> int -> int (* exponent -> base -> result *)
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    37
  val gcd: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    38
  val lcm: int -> int -> int
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    39
end;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    40
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    41
structure Integer : INTEGER =
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    42
struct
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    43
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    44
open IntInf;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    45
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    46
val int = fromInt;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    47
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    48
val zero = int 0;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    49
val one = int 1;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    50
val two = int 2;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    51
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    52
val machine_int = toInt;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    53
val string_of_int = toString;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    54
val int_of_string = fromString;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    55
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    56
val eq = op = : int * int -> bool;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    57
val cmp = compare;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    58
val le = curry (op <=);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    59
val lt = curry (op <);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    60
fun cmp_zero k = cmp (k, zero);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    61
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    62
val min = curry min;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    63
val max = curry max;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    64
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    65
val inc = curry (op +) one;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    66
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    67
val add = curry (op +);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    68
val sub = curry (op -);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    69
val mult = curry ( op * );
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    70
val divmod = curry divMod;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    71
nonfix div val div = curry div;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    72
nonfix mod val mod = curry mod;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    73
val neg = ~;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    74
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    75
fun signabs k = if cmp_zero k = LESS then (false, neg k) else (true, k);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    76
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    77
fun pow k l =
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    78
  let
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    79
    fun pw 0 = 1
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    80
      | pw k = mult l (pw (sub k 1));
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    81
  in if k < zero
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    82
    then error "pow: negative exponent"
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    83
    else pw k
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    84
  end;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    85
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    86
fun exp k = pow k two;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    87
val log = int o log2;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    88
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    89
fun gcd x y =
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    90
  let
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    91
    fun gxd x y = if y = zero then x else gxd y (mod x y)
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    92
  in if lt x y then gxd y x else gxd x y end;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    93
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    94
fun lcm x y = div (mult x y) (gcd x y);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    95
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    96
end;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    97
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    98
type integer = Integer.int;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    99
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   100
infix 7 *%;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   101
infix 6 +% -%; 
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   102
infix 4 =% <% <=% >% >=% <>%;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   103
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   104
fun a +% b = Integer.add a b;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   105
fun a -% b = a +% Integer.neg b;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   106
fun a *% b = Integer.mult a b;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   107
fun a =% b = Integer.eq (a, b);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   108
fun a <% b = Integer.lt a b;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   109
fun a <=% b = Integer.le a b;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   110
fun a >% b = b <% a;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   111
fun a >=% b = b <=% a;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   112
fun a <>% b = not (a =% b);
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   113
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   114
structure Intt = Integer; (*FIXME*)
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   115
val gcd = uncurry Integer.gcd; (*FIXME*)
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
   116
val lcm = uncurry Integer.lcm; (*FIXME*)