made mk_int/dest_int pervasive;
authorwenzelm
Thu Aug 02 21:43:55 2007 +0200 (2007-08-02)
changeset 24132dc95373bd69f
parent 24131 1099f6c73649
child 24133 75063f96618f
made mk_int/dest_int pervasive;
Admin/proper_int.ML
     1.1 --- a/Admin/proper_int.ML	Thu Aug 02 18:13:42 2007 +0200
     1.2 +++ b/Admin/proper_int.ML	Thu Aug 02 21:43:55 2007 +0200
     1.3 @@ -6,12 +6,9 @@
     1.4  words.
     1.5  *)
     1.6  
     1.7 -local
     1.8 +val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
     1.9 +val dest_int = IntInf.toInt: IntInf.int -> Int.int;
    1.10  
    1.11 -val mk = IntInf.fromInt: Int.int -> IntInf.int;
    1.12 -val dest = IntInf.toInt: IntInf.int -> Int.int;
    1.13 -
    1.14 -in
    1.15  
    1.16  (* Int *)
    1.17  
    1.18 @@ -24,6 +21,8 @@
    1.19    open IntInf;
    1.20    fun fromInt (a: int) = a;
    1.21    fun toInt (a: int) = a;
    1.22 +  val log2 = mk_int o IntInf.log2;
    1.23 +  val sign = mk_int o IntInf.sign;
    1.24  end;
    1.25  
    1.26  structure Int = IntInf;
    1.27 @@ -34,11 +33,11 @@
    1.28  structure List =
    1.29  struct
    1.30    open List;
    1.31 -  fun length a = mk (List.length a);
    1.32 -  fun nth (a, b) = List.nth (a, dest b);
    1.33 -  fun take (a, b) = List.take (a, dest b);
    1.34 -  fun drop (a, b) = List.drop (a, dest b);
    1.35 -  fun tabulate (a, b) = List.tabulate (dest a, b o mk);
    1.36 +  fun length a = mk_int (List.length a);
    1.37 +  fun nth (a, b) = List.nth (a, dest_int b);
    1.38 +  fun take (a, b) = List.take (a, dest_int b);
    1.39 +  fun drop (a, b) = List.drop (a, dest_int b);
    1.40 +  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
    1.41  end;
    1.42  
    1.43  val length = List.length;
    1.44 @@ -49,22 +48,22 @@
    1.45  structure Array =
    1.46  struct
    1.47    open Array;
    1.48 -  val maxLen = mk Array.maxLen;
    1.49 -  fun array (a, b) = Array.array (dest a, b);
    1.50 -  fun tabulate (a, b) = Array.tabulate (dest a, b o mk);
    1.51 -  fun length a = mk (Array.length a);
    1.52 -  fun sub (a, b) = Array.sub (a, dest b);
    1.53 -  fun update (a, b, c) = Array.update (a, dest b, c);
    1.54 -  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest di};
    1.55 -  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest di};
    1.56 -  fun appi a b = Array.appi (fn (x, y) => a (mk x, y)) b;
    1.57 -  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk x, y)) b;
    1.58 -  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
    1.59 -  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
    1.60 +  val maxLen = mk_int Array.maxLen;
    1.61 +  fun array (a, b) = Array.array (dest_int a, b);
    1.62 +  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
    1.63 +  fun length a = mk_int (Array.length a);
    1.64 +  fun sub (a, b) = Array.sub (a, dest_int b);
    1.65 +  fun update (a, b, c) = Array.update (a, dest_int b, c);
    1.66 +  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
    1.67 +  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
    1.68 +  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
    1.69 +  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
    1.70 +  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
    1.71 +  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
    1.72    fun findi a b =
    1.73 -    (case Array.findi (fn (x, y) => a (mk x, y)) b of
    1.74 +    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
    1.75        NONE => NONE
    1.76 -    | SOME (c, d) => SOME (mk c, d));
    1.77 +    | SOME (c, d) => SOME (mk_int c, d));
    1.78  end;
    1.79  
    1.80  
    1.81 @@ -73,19 +72,19 @@
    1.82  structure Vector =
    1.83  struct
    1.84    open Vector;
    1.85 -  val maxLen = mk Vector.maxLen;
    1.86 -  fun tabulate (a, b) = Vector.tabulate (dest a, b o mk);
    1.87 -  fun length a = mk (Vector.length a);
    1.88 -  fun sub (a, b) = Vector.sub (a, dest b);
    1.89 -  fun update (a, b, c) = Vector.update (a, dest b, c);
    1.90 -  fun appi a b = Vector.appi (fn (x, y) => a (mk x, y)) b;
    1.91 -  fun mapi a b = Vector.mapi (fn (x, y) => a (mk x, y)) b;
    1.92 -  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
    1.93 -  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
    1.94 +  val maxLen = mk_int Vector.maxLen;
    1.95 +  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
    1.96 +  fun length a = mk_int (Vector.length a);
    1.97 +  fun sub (a, b) = Vector.sub (a, dest_int b);
    1.98 +  fun update (a, b, c) = Vector.update (a, dest_int b, c);
    1.99 +  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
   1.100 +  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
   1.101 +  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
   1.102 +  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   1.103    fun findi a b =
   1.104 -    (case Vector.findi (fn (x, y) => a (mk x, y)) b of
   1.105 +    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
   1.106        NONE => NONE
   1.107 -    | SOME (c, d) => SOME (mk c, d));
   1.108 +    | SOME (c, d) => SOME (mk_int c, d));
   1.109  end;
   1.110  
   1.111  
   1.112 @@ -94,9 +93,9 @@
   1.113  structure Char =
   1.114  struct
   1.115    open Char;
   1.116 -  val maxOrd = mk Char.maxOrd;
   1.117 -  val chr = Char.chr o dest;
   1.118 -  val ord = mk o Char.ord;
   1.119 +  val maxOrd = mk_int Char.maxOrd;
   1.120 +  val chr = Char.chr o dest_int;
   1.121 +  val ord = mk_int o Char.ord;
   1.122  end;
   1.123  
   1.124  val chr = Char.chr;
   1.125 @@ -108,11 +107,11 @@
   1.126  structure String =
   1.127  struct
   1.128    open String;
   1.129 -  val maxSize = mk String.maxSize;
   1.130 -  val size = mk o String.size;
   1.131 -  fun sub (a, b) = String.sub (a, dest b);
   1.132 -  fun extract (a, b, c) = String.extract (a, dest b, Option.map dest c);
   1.133 -  fun substring (a, b, c) = String.substring (a, dest b, dest c);
   1.134 +  val maxSize = mk_int String.maxSize;
   1.135 +  val size = mk_int o String.size;
   1.136 +  fun sub (a, b) = String.sub (a, dest_int b);
   1.137 +  fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
   1.138 +  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
   1.139  end;
   1.140  
   1.141  val size = String.size;
   1.142 @@ -124,15 +123,15 @@
   1.143  structure Substring =
   1.144  struct
   1.145    open Substring;
   1.146 -  fun sub (a, b) = Substring.sub (a, dest b);
   1.147 -  val size = mk o Substring.size;
   1.148 -  fun base a = let val (b, c, d) = Substring.base a in (b, mk c, mk d) end;
   1.149 -  fun extract (a, b, c) = Substring.extract (a, dest b, Option.map dest c);
   1.150 -  fun substring (a, b, c) = Substring.substring (a, dest b, dest c);
   1.151 -  fun triml a b = Substring.triml (dest a) b;
   1.152 -  fun trimr a b = Substring.trimr (dest a) b;
   1.153 -  fun slice (a, b, c) = Substring.slice (a, dest b, Option.map dest c);
   1.154 -  fun splitAt (a, b) = Substring.splitAt (a, dest b);
   1.155 +  fun sub (a, b) = Substring.sub (a, dest_int b);
   1.156 +  val size = mk_int o Substring.size;
   1.157 +  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
   1.158 +  fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
   1.159 +  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
   1.160 +  fun triml a b = Substring.triml (dest_int a) b;
   1.161 +  fun trimr a b = Substring.trimr (dest_int a) b;
   1.162 +  fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
   1.163 +  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
   1.164  end;
   1.165  
   1.166  
   1.167 @@ -141,10 +140,10 @@
   1.168  structure Word =
   1.169  struct
   1.170    open Word;
   1.171 -  val wordSize = mk Word.wordSize;
   1.172 -  val toInt = mk o Word.toInt;
   1.173 -  val toIntX = mk o Word.toIntX;
   1.174 -  val fromInt = Word.fromInt o dest;
   1.175 +  val wordSize = mk_int Word.wordSize;
   1.176 +  val toInt = mk_int o Word.toInt;
   1.177 +  val toIntX = mk_int o Word.toIntX;
   1.178 +  val fromInt = Word.fromInt o dest_int;
   1.179  end;
   1.180  
   1.181  
   1.182 @@ -153,18 +152,18 @@
   1.183  structure Real =
   1.184  struct
   1.185    open Real;
   1.186 -  val radix = mk Real.radix;
   1.187 -  val precision = mk Real.precision;
   1.188 -  fun sign a = mk (Real.sign a);
   1.189 -  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk exp} end;
   1.190 -  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest exp};
   1.191 -  val ceil = mk o Real.ceil;
   1.192 -  val floor = mk o Real.floor;
   1.193 -  val real = Real.fromInt o dest;
   1.194 -  val round = mk o Real.round;
   1.195 -  val trunc = mk o Real.trunc;
   1.196 -  fun toInt a b = mk (Real.toInt a b);
   1.197 -  fun fromInt a = Real.fromInt (dest a);
   1.198 +  val radix = mk_int Real.radix;
   1.199 +  val precision = mk_int Real.precision;
   1.200 +  fun sign a = mk_int (Real.sign a);
   1.201 +  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
   1.202 +  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
   1.203 +  val ceil = mk_int o Real.ceil;
   1.204 +  val floor = mk_int o Real.floor;
   1.205 +  val real = Real.fromInt o dest_int;
   1.206 +  val round = mk_int o Real.round;
   1.207 +  val trunc = mk_int o Real.trunc;
   1.208 +  fun toInt a b = mk_int (Real.toInt a b);
   1.209 +  fun fromInt a = Real.fromInt (dest_int a);
   1.210  end;
   1.211  
   1.212  val ceil = Real.ceil;
   1.213 @@ -179,8 +178,8 @@
   1.214  structure TextIO =
   1.215  struct
   1.216    open TextIO;
   1.217 -  fun inputN (a, b) = TextIO.inputN (a, dest b);
   1.218 -  fun canInput (a, b) = Option.map mk (TextIO.canInput (a, dest b));
   1.219 +  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
   1.220 +  fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
   1.221  end;
   1.222  
   1.223  
   1.224 @@ -189,7 +188,5 @@
   1.225  structure Time =
   1.226  struct
   1.227    open Time;
   1.228 -  fun fmt a b = Time.fmt (dest a) b;
   1.229 +  fun fmt a b = Time.fmt (dest_int a) b;
   1.230  end;
   1.231 -
   1.232 -end;