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