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