Admin/proper_int.ML
author wenzelm
Tue, 24 Jul 2007 19:44:32 +0200
changeset 23961 9e7e1e309ebd
parent 23339 babddcf161ca
child 24132 dc95373bd69f
permissions -rw-r--r--
Multithreading in Poly/ML (version 5.1).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23339
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/proper_int.ML
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     4
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     5
SML basis with type int representing proper integers, not machine
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     6
words.
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     7
*)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     8
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
     9
local
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    10
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    11
val mk = IntInf.fromInt: Int.int -> IntInf.int;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    12
val dest = IntInf.toInt: IntInf.int -> Int.int;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    13
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    14
in
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    15
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    16
(* Int *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    17
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    18
structure OrigInt = Int;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    19
structure OrigIntInf = IntInf;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    20
type int = IntInf.int;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    21
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    22
structure IntInf =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    23
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    24
  open IntInf;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    25
  fun fromInt (a: int) = a;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    26
  fun toInt (a: int) = a;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    27
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    28
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    29
structure Int = IntInf;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    30
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    31
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    32
(* List *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    33
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    34
structure List =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    35
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    36
  open List;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    37
  fun length a = mk (List.length a);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    38
  fun nth (a, b) = List.nth (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    39
  fun take (a, b) = List.take (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    40
  fun drop (a, b) = List.drop (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    41
  fun tabulate (a, b) = List.tabulate (dest a, b o mk);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    42
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    43
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    44
val length = List.length;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    45
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    46
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    47
(* Array *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    48
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    49
structure Array =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    50
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    51
  open Array;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    52
  val maxLen = mk Array.maxLen;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    53
  fun array (a, b) = Array.array (dest a, b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    54
  fun tabulate (a, b) = Array.tabulate (dest a, b o mk);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    55
  fun length a = mk (Array.length a);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    56
  fun sub (a, b) = Array.sub (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    57
  fun update (a, b, c) = Array.update (a, dest b, c);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    58
  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest di};
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    59
  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest di};
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    60
  fun appi a b = Array.appi (fn (x, y) => a (mk x, y)) b;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    61
  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk x, y)) b;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    62
  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    63
  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    64
  fun findi a b =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    65
    (case Array.findi (fn (x, y) => a (mk x, y)) b of
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    66
      NONE => NONE
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    67
    | SOME (c, d) => SOME (mk c, d));
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    68
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    69
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    70
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    71
(* Vector *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    72
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    73
structure Vector =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    74
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    75
  open Vector;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    76
  val maxLen = mk Vector.maxLen;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    77
  fun tabulate (a, b) = Vector.tabulate (dest a, b o mk);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    78
  fun length a = mk (Vector.length a);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    79
  fun sub (a, b) = Vector.sub (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    80
  fun update (a, b, c) = Vector.update (a, dest b, c);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    81
  fun appi a b = Vector.appi (fn (x, y) => a (mk x, y)) b;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    82
  fun mapi a b = Vector.mapi (fn (x, y) => a (mk x, y)) b;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    83
  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    84
  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    85
  fun findi a b =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    86
    (case Vector.findi (fn (x, y) => a (mk x, y)) b of
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    87
      NONE => NONE
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    88
    | SOME (c, d) => SOME (mk c, d));
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    89
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    90
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    91
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    92
(* Char *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    93
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    94
structure Char =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    95
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    96
  open Char;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    97
  val maxOrd = mk Char.maxOrd;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    98
  val chr = Char.chr o dest;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
    99
  val ord = mk o Char.ord;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   100
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   101
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   102
val chr = Char.chr;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   103
val ord = Char.ord;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   104
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   105
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   106
(* String *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   107
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   108
structure String =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   109
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   110
  open String;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   111
  val maxSize = mk String.maxSize;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   112
  val size = mk o String.size;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   113
  fun sub (a, b) = String.sub (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   114
  fun extract (a, b, c) = String.extract (a, dest b, Option.map dest c);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   115
  fun substring (a, b, c) = String.substring (a, dest b, dest c);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   116
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   117
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   118
val size = String.size;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   119
val substring = String.substring;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   120
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   121
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   122
(* Substring *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   123
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   124
structure Substring =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   125
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   126
  open Substring;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   127
  fun sub (a, b) = Substring.sub (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   128
  val size = mk o Substring.size;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   129
  fun base a = let val (b, c, d) = Substring.base a in (b, mk c, mk d) end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   130
  fun extract (a, b, c) = Substring.extract (a, dest b, Option.map dest c);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   131
  fun substring (a, b, c) = Substring.substring (a, dest b, dest c);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   132
  fun triml a b = Substring.triml (dest a) b;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   133
  fun trimr a b = Substring.trimr (dest a) b;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   134
  fun slice (a, b, c) = Substring.slice (a, dest b, Option.map dest c);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   135
  fun splitAt (a, b) = Substring.splitAt (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   136
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   137
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   138
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   139
(* Word *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   140
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   141
structure Word =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   142
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   143
  open Word;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   144
  val wordSize = mk Word.wordSize;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   145
  val toInt = mk o Word.toInt;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   146
  val toIntX = mk o Word.toIntX;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   147
  val fromInt = Word.fromInt o dest;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   148
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   149
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   150
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   151
(* Real *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   152
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   153
structure Real =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   154
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   155
  open Real;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   156
  val radix = mk Real.radix;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   157
  val precision = mk Real.precision;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   158
  fun sign a = mk (Real.sign a);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   159
  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk exp} end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   160
  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest exp};
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   161
  val ceil = mk o Real.ceil;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   162
  val floor = mk o Real.floor;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   163
  val real = Real.fromInt o dest;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   164
  val round = mk o Real.round;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   165
  val trunc = mk o Real.trunc;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   166
  fun toInt a b = mk (Real.toInt a b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   167
  fun fromInt a = Real.fromInt (dest a);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   168
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   169
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   170
val ceil = Real.ceil;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   171
val floor = Real.floor;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   172
val real = Real.real;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   173
val round = Real.round;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   174
val trunc = Real.trunc;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   175
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   176
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   177
(* TextIO *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   178
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   179
structure TextIO =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   180
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   181
  open TextIO;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   182
  fun inputN (a, b) = TextIO.inputN (a, dest b);
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   183
  fun canInput (a, b) = Option.map mk (TextIO.canInput (a, dest b));
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   184
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   185
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   186
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   187
(* Time *)
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   188
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   189
structure Time =
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   190
struct
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   191
  open Time;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   192
  fun fmt a b = Time.fmt (dest a) b;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   193
end;
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   194
babddcf161ca SML basis with type int representing proper integers, not machine words.
wenzelm
parents:
diff changeset
   195
end;