src/Pure/ML-Systems/proper_int.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32566 e6b66a59bed6
child 35627 6cec06ef67a7
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
wenzelm@24140
     1
(*  Title:      Pure/ML-Systems/proper_int.ML
wenzelm@24140
     2
    Author:     Makarius
wenzelm@24140
     3
wenzelm@24140
     4
SML basis with type int representing proper integers, not machine
wenzelm@24140
     5
words.
wenzelm@24140
     6
*)
wenzelm@24140
     7
wenzelm@24597
     8
val ml_system_fix_ints = true;
wenzelm@24597
     9
wenzelm@24140
    10
val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
wenzelm@24140
    11
val dest_int = IntInf.toInt: IntInf.int -> Int.int;
wenzelm@24140
    12
wenzelm@24140
    13
wenzelm@24140
    14
(* Int *)
wenzelm@24140
    15
wenzelm@24140
    16
structure OrigInt = Int;
wenzelm@24140
    17
structure OrigIntInf = IntInf;
wenzelm@24140
    18
type int = IntInf.int;
wenzelm@24140
    19
wenzelm@24140
    20
structure IntInf =
wenzelm@24140
    21
struct
wenzelm@24140
    22
  open IntInf;
wenzelm@24140
    23
  fun fromInt (a: int) = a;
wenzelm@24140
    24
  fun toInt (a: int) = a;
wenzelm@24140
    25
  val log2 = mk_int o IntInf.log2;
wenzelm@24140
    26
  val sign = mk_int o IntInf.sign;
wenzelm@24140
    27
end;
wenzelm@24140
    28
wenzelm@24140
    29
structure Int = IntInf;
wenzelm@24140
    30
wenzelm@24140
    31
wenzelm@24140
    32
(* List *)
wenzelm@24140
    33
wenzelm@24140
    34
structure List =
wenzelm@24140
    35
struct
wenzelm@24140
    36
  open List;
wenzelm@24140
    37
  fun length a = mk_int (List.length a);
wenzelm@24140
    38
  fun nth (a, b) = List.nth (a, dest_int b);
wenzelm@24140
    39
  fun take (a, b) = List.take (a, dest_int b);
wenzelm@24140
    40
  fun drop (a, b) = List.drop (a, dest_int b);
wenzelm@24140
    41
  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
wenzelm@24140
    42
end;
wenzelm@24140
    43
wenzelm@24140
    44
val length = List.length;
wenzelm@24140
    45
wenzelm@24140
    46
wenzelm@24140
    47
(* Array *)
wenzelm@24140
    48
wenzelm@24140
    49
structure Array =
wenzelm@24140
    50
struct
wenzelm@24140
    51
  open Array;
wenzelm@24140
    52
  val maxLen = mk_int Array.maxLen;
wenzelm@24140
    53
  fun array (a, b) = Array.array (dest_int a, b);
wenzelm@24140
    54
  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
wenzelm@24140
    55
  fun length a = mk_int (Array.length a);
wenzelm@24140
    56
  fun sub (a, b) = Array.sub (a, dest_int b);
wenzelm@24140
    57
  fun update (a, b, c) = Array.update (a, dest_int b, c);
wenzelm@24140
    58
  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
wenzelm@24140
    59
  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
wenzelm@24140
    60
  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
wenzelm@24140
    61
  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
wenzelm@24140
    62
  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
wenzelm@24140
    63
  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
wenzelm@24140
    64
  fun findi a b =
wenzelm@24140
    65
    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
wenzelm@24140
    66
      NONE => NONE
wenzelm@24140
    67
    | SOME (c, d) => SOME (mk_int c, d));
wenzelm@24140
    68
end;
wenzelm@24140
    69
wenzelm@24140
    70
wenzelm@24140
    71
(* Vector *)
wenzelm@24140
    72
wenzelm@24140
    73
structure Vector =
wenzelm@24140
    74
struct
wenzelm@24140
    75
  open Vector;
wenzelm@24140
    76
  val maxLen = mk_int Vector.maxLen;
wenzelm@24140
    77
  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
wenzelm@24140
    78
  fun length a = mk_int (Vector.length a);
wenzelm@24140
    79
  fun sub (a, b) = Vector.sub (a, dest_int b);
wenzelm@24140
    80
  fun update (a, b, c) = Vector.update (a, dest_int b, c);
wenzelm@24140
    81
  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
wenzelm@24140
    82
  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
wenzelm@24140
    83
  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
wenzelm@24140
    84
  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
wenzelm@24140
    85
  fun findi a b =
wenzelm@24140
    86
    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
wenzelm@24140
    87
      NONE => NONE
wenzelm@24140
    88
    | SOME (c, d) => SOME (mk_int c, d));
wenzelm@24140
    89
end;
wenzelm@24140
    90
wenzelm@24140
    91
wenzelm@24140
    92
(* Char *)
wenzelm@24140
    93
wenzelm@24140
    94
structure Char =
wenzelm@24140
    95
struct
wenzelm@24140
    96
  open Char;
wenzelm@24140
    97
  val maxOrd = mk_int Char.maxOrd;
wenzelm@24140
    98
  val chr = Char.chr o dest_int;
wenzelm@24140
    99
  val ord = mk_int o Char.ord;
wenzelm@24140
   100
end;
wenzelm@24140
   101
wenzelm@24140
   102
val chr = Char.chr;
wenzelm@24140
   103
val ord = Char.ord;
wenzelm@24140
   104
wenzelm@24140
   105
wenzelm@24140
   106
(* String *)
wenzelm@24140
   107
wenzelm@24140
   108
structure String =
wenzelm@24140
   109
struct
wenzelm@24140
   110
  open String;
wenzelm@24140
   111
  val maxSize = mk_int String.maxSize;
wenzelm@24140
   112
  val size = mk_int o String.size;
wenzelm@24140
   113
  fun sub (a, b) = String.sub (a, dest_int b);
wenzelm@24140
   114
  fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
wenzelm@24140
   115
  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
wenzelm@24140
   116
end;
wenzelm@24140
   117
wenzelm@24140
   118
val size = String.size;
wenzelm@24140
   119
val substring = String.substring;
wenzelm@24140
   120
wenzelm@24140
   121
wenzelm@24140
   122
(* Substring *)
wenzelm@24140
   123
wenzelm@24140
   124
structure Substring =
wenzelm@24140
   125
struct
wenzelm@24140
   126
  open Substring;
wenzelm@24140
   127
  fun sub (a, b) = Substring.sub (a, dest_int b);
wenzelm@24140
   128
  val size = mk_int o Substring.size;
wenzelm@24140
   129
  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
wenzelm@24140
   130
  fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
wenzelm@24140
   131
  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
wenzelm@24140
   132
  fun triml a b = Substring.triml (dest_int a) b;
wenzelm@24140
   133
  fun trimr a b = Substring.trimr (dest_int a) b;
wenzelm@24140
   134
  fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
wenzelm@24140
   135
  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
wenzelm@24140
   136
end;
wenzelm@24140
   137
wenzelm@24140
   138
wenzelm@32566
   139
(* StringCvt *)
wenzelm@32566
   140
wenzelm@32566
   141
structure StringCvt =
wenzelm@32566
   142
struct
wenzelm@32566
   143
  open StringCvt;
wenzelm@32566
   144
  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option
wenzelm@32566
   145
  fun realfmt fmt = Real.fmt
wenzelm@32566
   146
    (case fmt of
wenzelm@32566
   147
      EXACT => StringCvt.EXACT
wenzelm@32566
   148
    | FIX NONE => StringCvt.FIX NONE
wenzelm@32566
   149
    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
wenzelm@32566
   150
    | GEN NONE => StringCvt.GEN NONE
wenzelm@32566
   151
    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
wenzelm@32566
   152
    | SCI NONE => StringCvt.SCI NONE
wenzelm@32566
   153
    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
wenzelm@32566
   154
end;
wenzelm@32566
   155
wenzelm@32566
   156
wenzelm@24140
   157
(* Word *)
wenzelm@24140
   158
wenzelm@24140
   159
structure Word =
wenzelm@24140
   160
struct
wenzelm@24140
   161
  open Word;
wenzelm@24140
   162
  val wordSize = mk_int Word.wordSize;
wenzelm@24140
   163
  val toInt = mk_int o Word.toInt;
wenzelm@24140
   164
  val toIntX = mk_int o Word.toIntX;
wenzelm@24140
   165
  val fromInt = Word.fromInt o dest_int;
wenzelm@24140
   166
end;
wenzelm@24140
   167
wenzelm@24140
   168
wenzelm@24140
   169
(* Real *)
wenzelm@24140
   170
wenzelm@24140
   171
structure Real =
wenzelm@24140
   172
struct
wenzelm@24140
   173
  open Real;
wenzelm@24140
   174
  val radix = mk_int Real.radix;
wenzelm@24140
   175
  val precision = mk_int Real.precision;
wenzelm@24140
   176
  fun sign a = mk_int (Real.sign a);
wenzelm@24140
   177
  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
wenzelm@24140
   178
  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
wenzelm@24140
   179
  val ceil = mk_int o Real.ceil;
wenzelm@24140
   180
  val floor = mk_int o Real.floor;
wenzelm@24140
   181
  val real = Real.fromInt o dest_int;
wenzelm@24140
   182
  val round = mk_int o Real.round;
wenzelm@24140
   183
  val trunc = mk_int o Real.trunc;
wenzelm@24140
   184
  fun toInt a b = mk_int (Real.toInt a b);
wenzelm@24140
   185
  fun fromInt a = Real.fromInt (dest_int a);
wenzelm@32566
   186
  val fmt = StringCvt.realfmt;
wenzelm@24140
   187
end;
wenzelm@24140
   188
wenzelm@24140
   189
val ceil = Real.ceil;
wenzelm@24140
   190
val floor = Real.floor;
wenzelm@24140
   191
val real = Real.real;
wenzelm@24140
   192
val round = Real.round;
wenzelm@24140
   193
val trunc = Real.trunc;
wenzelm@24140
   194
wenzelm@24140
   195
wenzelm@24140
   196
(* TextIO *)
wenzelm@24140
   197
wenzelm@24140
   198
structure TextIO =
wenzelm@24140
   199
struct
wenzelm@24140
   200
  open TextIO;
wenzelm@24140
   201
  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
wenzelm@24140
   202
  fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
wenzelm@24140
   203
end;
wenzelm@24140
   204
wenzelm@24140
   205
wenzelm@24140
   206
(* Time *)
wenzelm@24140
   207
wenzelm@24140
   208
structure Time =
wenzelm@24140
   209
struct
wenzelm@24140
   210
  open Time;
wenzelm@24140
   211
  fun fmt a b = Time.fmt (dest_int a) b;
wenzelm@24140
   212
end;
wenzelm@24604
   213