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