made mk_int/dest_int pervasive;

--- a/Admin/proper_int.ML	Thu Aug 02 18:13:42 2007 +0200
+++ b/Admin/proper_int.ML	Thu Aug 02 21:43:55 2007 +0200
@@ -6,12 +6,9 @@
 words.
 *)
 
-local
+val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
+val dest_int = IntInf.toInt: IntInf.int -> Int.int;
 
-val mk = IntInf.fromInt: Int.int -> IntInf.int;
-val dest = IntInf.toInt: IntInf.int -> Int.int;
-
-in
 
 (* Int *)
 
@@ -24,6 +21,8 @@
   open IntInf;
   fun fromInt (a: int) = a;
   fun toInt (a: int) = a;
+  val log2 = mk_int o IntInf.log2;
+  val sign = mk_int o IntInf.sign;
 end;
 
 structure Int = IntInf;
@@ -34,11 +33,11 @@
 structure List =
 struct
   open List;
-  fun length a = mk (List.length a);
-  fun nth (a, b) = List.nth (a, dest b);
-  fun take (a, b) = List.take (a, dest b);
-  fun drop (a, b) = List.drop (a, dest b);
-  fun tabulate (a, b) = List.tabulate (dest a, b o mk);
+  fun length a = mk_int (List.length a);
+  fun nth (a, b) = List.nth (a, dest_int b);
+  fun take (a, b) = List.take (a, dest_int b);
+  fun drop (a, b) = List.drop (a, dest_int b);
+  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
 end;
 
 val length = List.length;
@@ -49,22 +48,22 @@
 structure Array =
 struct
   open Array;
-  val maxLen = mk Array.maxLen;
-  fun array (a, b) = Array.array (dest a, b);
-  fun tabulate (a, b) = Array.tabulate (dest a, b o mk);
-  fun length a = mk (Array.length a);
-  fun sub (a, b) = Array.sub (a, dest b);
-  fun update (a, b, c) = Array.update (a, dest b, c);
-  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest di};
-  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest di};
-  fun appi a b = Array.appi (fn (x, y) => a (mk x, y)) b;
-  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk x, y)) b;
-  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
-  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
+  val maxLen = mk_int Array.maxLen;
+  fun array (a, b) = Array.array (dest_int a, b);
+  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
+  fun length a = mk_int (Array.length a);
+  fun sub (a, b) = Array.sub (a, dest_int b);
+  fun update (a, b, c) = Array.update (a, dest_int b, c);
+  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
+  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
+  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
+  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
+  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
+  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   fun findi a b =
-    (case Array.findi (fn (x, y) => a (mk x, y)) b of
+    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
       NONE => NONE
-    | SOME (c, d) => SOME (mk c, d));
+    | SOME (c, d) => SOME (mk_int c, d));
 end;
 
 
@@ -73,19 +72,19 @@
 structure Vector =
 struct
   open Vector;
-  val maxLen = mk Vector.maxLen;
-  fun tabulate (a, b) = Vector.tabulate (dest a, b o mk);
-  fun length a = mk (Vector.length a);
-  fun sub (a, b) = Vector.sub (a, dest b);
-  fun update (a, b, c) = Vector.update (a, dest b, c);
-  fun appi a b = Vector.appi (fn (x, y) => a (mk x, y)) b;
-  fun mapi a b = Vector.mapi (fn (x, y) => a (mk x, y)) b;
-  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
-  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
+  val maxLen = mk_int Vector.maxLen;
+  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
+  fun length a = mk_int (Vector.length a);
+  fun sub (a, b) = Vector.sub (a, dest_int b);
+  fun update (a, b, c) = Vector.update (a, dest_int b, c);
+  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
+  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
+  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
+  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   fun findi a b =
-    (case Vector.findi (fn (x, y) => a (mk x, y)) b of
+    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
       NONE => NONE
-    | SOME (c, d) => SOME (mk c, d));
+    | SOME (c, d) => SOME (mk_int c, d));
 end;
 
 
@@ -94,9 +93,9 @@
 structure Char =
 struct
   open Char;
-  val maxOrd = mk Char.maxOrd;
-  val chr = Char.chr o dest;
-  val ord = mk o Char.ord;
+  val maxOrd = mk_int Char.maxOrd;
+  val chr = Char.chr o dest_int;
+  val ord = mk_int o Char.ord;
 end;
 
 val chr = Char.chr;
@@ -108,11 +107,11 @@
 structure String =
 struct
   open String;
-  val maxSize = mk String.maxSize;
-  val size = mk o String.size;
-  fun sub (a, b) = String.sub (a, dest b);
-  fun extract (a, b, c) = String.extract (a, dest b, Option.map dest c);
-  fun substring (a, b, c) = String.substring (a, dest b, dest c);
+  val maxSize = mk_int String.maxSize;
+  val size = mk_int o String.size;
+  fun sub (a, b) = String.sub (a, dest_int b);
+  fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
+  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
 end;
 
 val size = String.size;
@@ -124,15 +123,15 @@
 structure Substring =
 struct
   open Substring;
-  fun sub (a, b) = Substring.sub (a, dest b);
-  val size = mk o Substring.size;
-  fun base a = let val (b, c, d) = Substring.base a in (b, mk c, mk d) end;
-  fun extract (a, b, c) = Substring.extract (a, dest b, Option.map dest c);
-  fun substring (a, b, c) = Substring.substring (a, dest b, dest c);
-  fun triml a b = Substring.triml (dest a) b;
-  fun trimr a b = Substring.trimr (dest a) b;
-  fun slice (a, b, c) = Substring.slice (a, dest b, Option.map dest c);
-  fun splitAt (a, b) = Substring.splitAt (a, dest b);
+  fun sub (a, b) = Substring.sub (a, dest_int b);
+  val size = mk_int o Substring.size;
+  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
+  fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
+  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
+  fun triml a b = Substring.triml (dest_int a) b;
+  fun trimr a b = Substring.trimr (dest_int a) b;
+  fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
+  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
 end;
 
 
@@ -141,10 +140,10 @@
 structure Word =
 struct
   open Word;
-  val wordSize = mk Word.wordSize;
-  val toInt = mk o Word.toInt;
-  val toIntX = mk o Word.toIntX;
-  val fromInt = Word.fromInt o dest;
+  val wordSize = mk_int Word.wordSize;
+  val toInt = mk_int o Word.toInt;
+  val toIntX = mk_int o Word.toIntX;
+  val fromInt = Word.fromInt o dest_int;
 end;
 
 
@@ -153,18 +152,18 @@
 structure Real =
 struct
   open Real;
-  val radix = mk Real.radix;
-  val precision = mk Real.precision;
-  fun sign a = mk (Real.sign a);
-  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk exp} end;
-  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest exp};
-  val ceil = mk o Real.ceil;
-  val floor = mk o Real.floor;
-  val real = Real.fromInt o dest;
-  val round = mk o Real.round;
-  val trunc = mk o Real.trunc;
-  fun toInt a b = mk (Real.toInt a b);
-  fun fromInt a = Real.fromInt (dest a);
+  val radix = mk_int Real.radix;
+  val precision = mk_int Real.precision;
+  fun sign a = mk_int (Real.sign a);
+  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
+  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
+  val ceil = mk_int o Real.ceil;
+  val floor = mk_int o Real.floor;
+  val real = Real.fromInt o dest_int;
+  val round = mk_int o Real.round;
+  val trunc = mk_int o Real.trunc;
+  fun toInt a b = mk_int (Real.toInt a b);
+  fun fromInt a = Real.fromInt (dest_int a);
 end;
 
 val ceil = Real.ceil;
@@ -179,8 +178,8 @@
 structure TextIO =
 struct
   open TextIO;
-  fun inputN (a, b) = TextIO.inputN (a, dest b);
-  fun canInput (a, b) = Option.map mk (TextIO.canInput (a, dest b));
+  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
+  fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
 end;
 
 
@@ -189,7 +188,5 @@
 structure Time =
 struct
   open Time;
-  fun fmt a b = Time.fmt (dest a) b;
+  fun fmt a b = Time.fmt (dest_int a) b;
 end;
-
-end;