src/Pure/ML-Systems/proper_int.ML
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 50801 b8ff6d1ee56c
child 52277 2bbeab01c0ea
permissions -rw-r--r--
tuned signature;
tuned comments;
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@24140
     8
val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
wenzelm@24140
     9
val dest_int = IntInf.toInt: IntInf.int -> Int.int;
wenzelm@24140
    10
wenzelm@24140
    11
wenzelm@24140
    12
(* Int *)
wenzelm@24140
    13
wenzelm@24140
    14
type int = IntInf.int;
wenzelm@24140
    15
wenzelm@24140
    16
structure IntInf =
wenzelm@24140
    17
struct
wenzelm@24140
    18
  open IntInf;
wenzelm@24140
    19
  fun fromInt (a: int) = a;
wenzelm@24140
    20
  fun toInt (a: int) = a;
wenzelm@24140
    21
  val log2 = mk_int o IntInf.log2;
wenzelm@24140
    22
  val sign = mk_int o IntInf.sign;
wenzelm@24140
    23
end;
wenzelm@24140
    24
wenzelm@24140
    25
structure Int = IntInf;
wenzelm@24140
    26
wenzelm@24140
    27
wenzelm@24140
    28
(* List *)
wenzelm@24140
    29
wenzelm@24140
    30
structure List =
wenzelm@24140
    31
struct
wenzelm@24140
    32
  open List;
wenzelm@24140
    33
  fun length a = mk_int (List.length a);
wenzelm@24140
    34
  fun nth (a, b) = List.nth (a, dest_int b);
wenzelm@24140
    35
  fun take (a, b) = List.take (a, dest_int b);
wenzelm@24140
    36
  fun drop (a, b) = List.drop (a, dest_int b);
wenzelm@24140
    37
  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
wenzelm@24140
    38
end;
wenzelm@24140
    39
wenzelm@24140
    40
val length = List.length;
wenzelm@24140
    41
wenzelm@24140
    42
wenzelm@24140
    43
(* Array *)
wenzelm@24140
    44
wenzelm@24140
    45
structure Array =
wenzelm@24140
    46
struct
wenzelm@24140
    47
  open Array;
wenzelm@24140
    48
  val maxLen = mk_int Array.maxLen;
wenzelm@24140
    49
  fun array (a, b) = Array.array (dest_int a, b);
wenzelm@24140
    50
  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
wenzelm@24140
    51
  fun length a = mk_int (Array.length a);
wenzelm@24140
    52
  fun sub (a, b) = Array.sub (a, dest_int b);
wenzelm@24140
    53
  fun update (a, b, c) = Array.update (a, dest_int b, c);
wenzelm@24140
    54
  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
wenzelm@24140
    55
  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
wenzelm@24140
    56
  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
wenzelm@24140
    57
  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
wenzelm@24140
    58
  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
wenzelm@24140
    59
  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
wenzelm@24140
    60
  fun findi a b =
wenzelm@24140
    61
    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
wenzelm@24140
    62
      NONE => NONE
wenzelm@24140
    63
    | SOME (c, d) => SOME (mk_int c, d));
wenzelm@24140
    64
end;
wenzelm@24140
    65
wenzelm@24140
    66
wenzelm@24140
    67
(* Vector *)
wenzelm@24140
    68
wenzelm@24140
    69
structure Vector =
wenzelm@24140
    70
struct
wenzelm@24140
    71
  open Vector;
wenzelm@24140
    72
  val maxLen = mk_int Vector.maxLen;
wenzelm@24140
    73
  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
wenzelm@24140
    74
  fun length a = mk_int (Vector.length a);
wenzelm@24140
    75
  fun sub (a, b) = Vector.sub (a, dest_int b);
wenzelm@24140
    76
  fun update (a, b, c) = Vector.update (a, dest_int b, c);
wenzelm@24140
    77
  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
wenzelm@24140
    78
  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
wenzelm@24140
    79
  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
wenzelm@24140
    80
  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
wenzelm@24140
    81
  fun findi a b =
wenzelm@24140
    82
    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
wenzelm@24140
    83
      NONE => NONE
wenzelm@24140
    84
    | SOME (c, d) => SOME (mk_int c, d));
wenzelm@24140
    85
end;
wenzelm@24140
    86
wenzelm@24140
    87
wenzelm@45067
    88
(* Word8VectorSlice *)
wenzelm@45067
    89
wenzelm@45067
    90
structure Word8VectorSlice =
wenzelm@45067
    91
struct
wenzelm@45067
    92
  open Word8VectorSlice;
wenzelm@45067
    93
  val length = mk_int o Word8VectorSlice.length;
wenzelm@45067
    94
  fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
wenzelm@45067
    95
end;
wenzelm@45067
    96
wenzelm@45067
    97
wenzelm@24140
    98
(* Char *)
wenzelm@24140
    99
wenzelm@24140
   100
structure Char =
wenzelm@24140
   101
struct
wenzelm@24140
   102
  open Char;
wenzelm@24140
   103
  val maxOrd = mk_int Char.maxOrd;
wenzelm@24140
   104
  val chr = Char.chr o dest_int;
wenzelm@24140
   105
  val ord = mk_int o Char.ord;
wenzelm@24140
   106
end;
wenzelm@24140
   107
wenzelm@24140
   108
val chr = Char.chr;
wenzelm@24140
   109
val ord = Char.ord;
wenzelm@24140
   110
wenzelm@24140
   111
wenzelm@24140
   112
(* String *)
wenzelm@24140
   113
wenzelm@24140
   114
structure String =
wenzelm@24140
   115
struct
wenzelm@24140
   116
  open String;
wenzelm@24140
   117
  val maxSize = mk_int String.maxSize;
wenzelm@24140
   118
  val size = mk_int o String.size;
wenzelm@24140
   119
  fun sub (a, b) = String.sub (a, dest_int b);
wenzelm@24140
   120
  fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
wenzelm@24140
   121
  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
wenzelm@24140
   122
end;
wenzelm@24140
   123
wenzelm@24140
   124
val size = String.size;
wenzelm@24140
   125
val substring = String.substring;
wenzelm@24140
   126
wenzelm@24140
   127
wenzelm@24140
   128
(* Substring *)
wenzelm@24140
   129
wenzelm@24140
   130
structure Substring =
wenzelm@24140
   131
struct
wenzelm@24140
   132
  open Substring;
wenzelm@24140
   133
  fun sub (a, b) = Substring.sub (a, dest_int b);
wenzelm@24140
   134
  val size = mk_int o Substring.size;
wenzelm@24140
   135
  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
wenzelm@24140
   136
  fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
wenzelm@24140
   137
  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
wenzelm@24140
   138
  fun triml a b = Substring.triml (dest_int a) b;
wenzelm@24140
   139
  fun trimr a b = Substring.trimr (dest_int a) b;
wenzelm@24140
   140
  fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
wenzelm@24140
   141
  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
wenzelm@24140
   142
end;
wenzelm@24140
   143
wenzelm@24140
   144
wenzelm@32566
   145
(* StringCvt *)
wenzelm@32566
   146
wenzelm@32566
   147
structure StringCvt =
wenzelm@32566
   148
struct
wenzelm@32566
   149
  open StringCvt;
wenzelm@41619
   150
  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
wenzelm@32566
   151
  fun realfmt fmt = Real.fmt
wenzelm@32566
   152
    (case fmt of
wenzelm@32566
   153
      EXACT => StringCvt.EXACT
wenzelm@32566
   154
    | FIX NONE => StringCvt.FIX NONE
wenzelm@32566
   155
    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
wenzelm@32566
   156
    | GEN NONE => StringCvt.GEN NONE
wenzelm@32566
   157
    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
wenzelm@32566
   158
    | SCI NONE => StringCvt.SCI NONE
wenzelm@32566
   159
    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
wenzelm@32566
   160
end;
wenzelm@32566
   161
wenzelm@32566
   162
wenzelm@24140
   163
(* Word *)
wenzelm@24140
   164
wenzelm@24140
   165
structure Word =
wenzelm@24140
   166
struct
wenzelm@24140
   167
  open Word;
wenzelm@24140
   168
  val wordSize = mk_int Word.wordSize;
wenzelm@41619
   169
  val toInt = Word.toLargeInt;
wenzelm@41619
   170
  val toIntX = Word.toLargeIntX;
wenzelm@41619
   171
  val fromInt = Word.fromLargeInt;
wenzelm@24140
   172
end;
wenzelm@24140
   173
wenzelm@40747
   174
structure Word8 =
wenzelm@40747
   175
struct
wenzelm@40747
   176
  open Word8;
wenzelm@40747
   177
  val wordSize = mk_int Word8.wordSize;
wenzelm@41619
   178
  val toInt = Word8.toLargeInt;
wenzelm@41619
   179
  val toIntX = Word8.toLargeIntX;
wenzelm@41619
   180
  val fromInt = Word8.fromLargeInt;
wenzelm@40747
   181
end;
wenzelm@40747
   182
wenzelm@35627
   183
structure Word32 =
wenzelm@35627
   184
struct
wenzelm@35627
   185
  open Word32;
wenzelm@35627
   186
  val wordSize = mk_int Word32.wordSize;
wenzelm@41619
   187
  val toInt = Word32.toLargeInt;
wenzelm@41619
   188
  val toIntX = Word32.toLargeIntX;
wenzelm@41619
   189
  val fromInt = Word32.fromLargeInt;
wenzelm@35627
   190
end;
wenzelm@35627
   191
wenzelm@40747
   192
structure LargeWord =
wenzelm@40747
   193
struct
wenzelm@40747
   194
  open LargeWord;
wenzelm@40747
   195
  val wordSize = mk_int LargeWord.wordSize;
wenzelm@41619
   196
  val toInt = LargeWord.toLargeInt;
wenzelm@41619
   197
  val toIntX = LargeWord.toLargeIntX;
wenzelm@41619
   198
  val fromInt = LargeWord.fromLargeInt;
wenzelm@40747
   199
end;
wenzelm@40747
   200
wenzelm@24140
   201
wenzelm@24140
   202
(* Real *)
wenzelm@24140
   203
wenzelm@24140
   204
structure Real =
wenzelm@24140
   205
struct
wenzelm@24140
   206
  open Real;
wenzelm@24140
   207
  val radix = mk_int Real.radix;
wenzelm@24140
   208
  val precision = mk_int Real.precision;
wenzelm@24140
   209
  fun sign a = mk_int (Real.sign a);
wenzelm@24140
   210
  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
wenzelm@24140
   211
  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
wenzelm@24140
   212
  val ceil = mk_int o Real.ceil;
wenzelm@24140
   213
  val floor = mk_int o Real.floor;
wenzelm@24140
   214
  val real = Real.fromInt o dest_int;
wenzelm@24140
   215
  val round = mk_int o Real.round;
wenzelm@24140
   216
  val trunc = mk_int o Real.trunc;
wenzelm@24140
   217
  fun toInt a b = mk_int (Real.toInt a b);
wenzelm@24140
   218
  fun fromInt a = Real.fromInt (dest_int a);
wenzelm@32566
   219
  val fmt = StringCvt.realfmt;
wenzelm@24140
   220
end;
wenzelm@24140
   221
wenzelm@24140
   222
val ceil = Real.ceil;
wenzelm@24140
   223
val floor = Real.floor;
wenzelm@24140
   224
val real = Real.real;
wenzelm@24140
   225
val round = Real.round;
wenzelm@24140
   226
val trunc = Real.trunc;
wenzelm@24140
   227
wenzelm@24140
   228
wenzelm@24140
   229
(* TextIO *)
wenzelm@24140
   230
wenzelm@24140
   231
structure TextIO =
wenzelm@24140
   232
struct
wenzelm@24140
   233
  open TextIO;
wenzelm@24140
   234
  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
wenzelm@24140
   235
  fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
wenzelm@24140
   236
end;
wenzelm@24140
   237
wenzelm@24140
   238
wenzelm@45030
   239
(* BinIO *)
wenzelm@45030
   240
wenzelm@45030
   241
structure BinIO =
wenzelm@45030
   242
struct
wenzelm@45030
   243
  open BinIO;
wenzelm@45030
   244
  fun inputN (a, b) = BinIO.inputN (a, dest_int b);
wenzelm@45030
   245
  fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
wenzelm@45030
   246
end;
wenzelm@45030
   247
wenzelm@45030
   248
wenzelm@24140
   249
(* Time *)
wenzelm@24140
   250
wenzelm@24140
   251
structure Time =
wenzelm@24140
   252
struct
wenzelm@24140
   253
  open Time;
wenzelm@24140
   254
  fun fmt a b = Time.fmt (dest_int a) b;
wenzelm@24140
   255
end;
wenzelm@24604
   256
wenzelm@45030
   257
wenzelm@45030
   258
(* Sockets *)
wenzelm@45030
   259
wenzelm@45030
   260
structure INetSock =
wenzelm@45030
   261
struct
wenzelm@45030
   262
  open INetSock;
wenzelm@45030
   263
  fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
wenzelm@45030
   264
  fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
wenzelm@45030
   265
end;
wenzelm@45030
   266