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