1 (* Title: Pure/ML-Systems/proper_int.ML
4 SML basis with type int representing proper integers, not machine
8 val ml_system_fix_ints = true;
10 val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
11 val dest_int = IntInf.toInt: IntInf.int -> Int.int;
16 structure OrigInt = Int;
17 structure OrigIntInf = IntInf;
18 type int = IntInf.int;
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;
29 structure Int = IntInf;
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);
44 val length = List.length;
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;
65 (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
67 | SOME (c, d) => SOME (mk_int c, d));
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;
86 (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
88 | SOME (c, d) => SOME (mk_int c, d));
97 val maxOrd = mk_int Char.maxOrd;
98 val chr = Char.chr o dest_int;
99 val ord = mk_int o Char.ord;
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);
118 val size = String.size;
119 val substring = String.substring;
124 structure 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);
141 structure StringCvt =
144 datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option
145 fun realfmt fmt = Real.fmt
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)));
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;
171 val wordSize = mk_int Word8.wordSize;
172 val toInt = mk_int o Word8.toInt;
173 val toIntX = mk_int o Word8.toIntX;
174 val fromInt = Word8.fromInt o dest_int;
180 val wordSize = mk_int Word32.wordSize;
181 val toInt = mk_int o Word32.toInt;
182 val toIntX = mk_int o Word32.toIntX;
183 val fromInt = Word32.fromInt o dest_int;
186 structure LargeWord =
189 val wordSize = mk_int LargeWord.wordSize;
190 val toInt = mk_int o LargeWord.toInt;
191 val toIntX = mk_int o LargeWord.toIntX;
192 val fromInt = LargeWord.fromInt o dest_int;
201 val radix = mk_int Real.radix;
202 val precision = mk_int Real.precision;
203 fun sign a = mk_int (Real.sign a);
204 fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
205 fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
206 val ceil = mk_int o Real.ceil;
207 val floor = mk_int o Real.floor;
208 val real = Real.fromInt o dest_int;
209 val round = mk_int o Real.round;
210 val trunc = mk_int o Real.trunc;
211 fun toInt a b = mk_int (Real.toInt a b);
212 fun fromInt a = Real.fromInt (dest_int a);
213 val fmt = StringCvt.realfmt;
216 val ceil = Real.ceil;
217 val floor = Real.floor;
218 val real = Real.real;
219 val round = Real.round;
220 val trunc = Real.trunc;
228 fun inputN (a, b) = TextIO.inputN (a, dest_int b);
229 fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
238 fun fmt a b = Time.fmt (dest_int a) b;