Admin/proper_int.ML
author haftmann
Tue Jul 10 17:30:50 2007 +0200 (2007-07-10)
changeset 23709 fd31da8f752a
parent 23339 babddcf161ca
child 24132 dc95373bd69f
permissions -rw-r--r--
moved lfp_induct2 here
     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 local
    10 
    11 val mk = IntInf.fromInt: Int.int -> IntInf.int;
    12 val dest = IntInf.toInt: IntInf.int -> Int.int;
    13 
    14 in
    15 
    16 (* Int *)
    17 
    18 structure OrigInt = Int;
    19 structure OrigIntInf = IntInf;
    20 type int = IntInf.int;
    21 
    22 structure IntInf =
    23 struct
    24   open IntInf;
    25   fun fromInt (a: int) = a;
    26   fun toInt (a: int) = a;
    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 (List.length a);
    38   fun nth (a, b) = List.nth (a, dest b);
    39   fun take (a, b) = List.take (a, dest b);
    40   fun drop (a, b) = List.drop (a, dest b);
    41   fun tabulate (a, b) = List.tabulate (dest a, b o mk);
    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 Array.maxLen;
    53   fun array (a, b) = Array.array (dest a, b);
    54   fun tabulate (a, b) = Array.tabulate (dest a, b o mk);
    55   fun length a = mk (Array.length a);
    56   fun sub (a, b) = Array.sub (a, dest b);
    57   fun update (a, b, c) = Array.update (a, dest b, c);
    58   fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest di};
    59   fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest di};
    60   fun appi a b = Array.appi (fn (x, y) => a (mk x, y)) b;
    61   fun modifyi a b = Array.modifyi (fn (x, y) => a (mk x, y)) b;
    62   fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
    63   fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
    64   fun findi a b =
    65     (case Array.findi (fn (x, y) => a (mk x, y)) b of
    66       NONE => NONE
    67     | SOME (c, d) => SOME (mk c, d));
    68 end;
    69 
    70 
    71 (* Vector *)
    72 
    73 structure Vector =
    74 struct
    75   open Vector;
    76   val maxLen = mk Vector.maxLen;
    77   fun tabulate (a, b) = Vector.tabulate (dest a, b o mk);
    78   fun length a = mk (Vector.length a);
    79   fun sub (a, b) = Vector.sub (a, dest b);
    80   fun update (a, b, c) = Vector.update (a, dest b, c);
    81   fun appi a b = Vector.appi (fn (x, y) => a (mk x, y)) b;
    82   fun mapi a b = Vector.mapi (fn (x, y) => a (mk x, y)) b;
    83   fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
    84   fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
    85   fun findi a b =
    86     (case Vector.findi (fn (x, y) => a (mk x, y)) b of
    87       NONE => NONE
    88     | SOME (c, d) => SOME (mk c, d));
    89 end;
    90 
    91 
    92 (* Char *)
    93 
    94 structure Char =
    95 struct
    96   open Char;
    97   val maxOrd = mk Char.maxOrd;
    98   val chr = Char.chr o dest;
    99   val ord = mk 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 String.maxSize;
   112   val size = mk o String.size;
   113   fun sub (a, b) = String.sub (a, dest b);
   114   fun extract (a, b, c) = String.extract (a, dest b, Option.map dest c);
   115   fun substring (a, b, c) = String.substring (a, dest b, dest 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 b);
   128   val size = mk o Substring.size;
   129   fun base a = let val (b, c, d) = Substring.base a in (b, mk c, mk d) end;
   130   fun extract (a, b, c) = Substring.extract (a, dest b, Option.map dest c);
   131   fun substring (a, b, c) = Substring.substring (a, dest b, dest c);
   132   fun triml a b = Substring.triml (dest a) b;
   133   fun trimr a b = Substring.trimr (dest a) b;
   134   fun slice (a, b, c) = Substring.slice (a, dest b, Option.map dest c);
   135   fun splitAt (a, b) = Substring.splitAt (a, dest b);
   136 end;
   137 
   138 
   139 (* Word *)
   140 
   141 structure Word =
   142 struct
   143   open Word;
   144   val wordSize = mk Word.wordSize;
   145   val toInt = mk o Word.toInt;
   146   val toIntX = mk o Word.toIntX;
   147   val fromInt = Word.fromInt o dest;
   148 end;
   149 
   150 
   151 (* Real *)
   152 
   153 structure Real =
   154 struct
   155   open Real;
   156   val radix = mk Real.radix;
   157   val precision = mk Real.precision;
   158   fun sign a = mk (Real.sign a);
   159   fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk exp} end;
   160   fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest exp};
   161   val ceil = mk o Real.ceil;
   162   val floor = mk o Real.floor;
   163   val real = Real.fromInt o dest;
   164   val round = mk o Real.round;
   165   val trunc = mk o Real.trunc;
   166   fun toInt a b = mk (Real.toInt a b);
   167   fun fromInt a = Real.fromInt (dest a);
   168 end;
   169 
   170 val ceil = Real.ceil;
   171 val floor = Real.floor;
   172 val real = Real.real;
   173 val round = Real.round;
   174 val trunc = Real.trunc;
   175 
   176 
   177 (* TextIO *)
   178 
   179 structure TextIO =
   180 struct
   181   open TextIO;
   182   fun inputN (a, b) = TextIO.inputN (a, dest b);
   183   fun canInput (a, b) = Option.map mk (TextIO.canInput (a, dest b));
   184 end;
   185 
   186 
   187 (* Time *)
   188 
   189 structure Time =
   190 struct
   191   open Time;
   192   fun fmt a b = Time.fmt (dest a) b;
   193 end;
   194 
   195 end;