1(* 2 Title: Standard Basis Library: LargeInt and FixedInt structures 3 Copyright David C.J. Matthews 1999, 2016 4 5 This library is free software; you can redistribute it and/or 6 modify it under the terms of the GNU Lesser General Public 7 License version 2.1 as published by the Free Software Foundation. 8 9 This library is distributed in the hope that it will be useful, 10 but WITHOUT ANY WARRANTY; without even the implied warranty of 11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 12 Lesser General Public License for more details. 13 14 You should have received a copy of the GNU Lesser General Public 15 License along with this library; if not, write to the Free Software 16 Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA 17*) 18 19 20(* LargeInt is defined in INITIALISE. *) 21 22signature INTEGER = 23sig 24 eqtype int 25 val toLarge : int -> LargeInt.int 26 val fromLarge : LargeInt.int -> int 27 val toInt : int -> Int.int 28 val fromInt : Int.int -> int 29 val precision : Int.int option 30 31 val minInt : int option 32 val maxInt : int option 33 34 val ~ : int -> int 35 val * : (int * int) -> int 36 val div : (int * int) -> int 37 val mod : (int * int) -> int 38 val quot : (int * int) -> int 39 val rem : (int * int) -> int 40 val + : (int * int) -> int 41 val - : (int * int) -> int 42 val compare : (int * int) -> General.order 43 44 val > : (int * int) -> bool 45 val >= : (int * int) -> bool 46 val < : (int * int) -> bool 47 val <= : (int * int) -> bool 48 49 val abs : int -> int 50 val min : (int * int) -> int 51 val max : (int * int) -> int 52 val sign : int -> Int.int 53 val sameSign : (int * int) -> bool 54 val fmt : StringCvt.radix -> int -> string 55 val toString : int -> string 56 val fromString : string -> int option 57 val scan : StringCvt.radix -> (char, 'a) StringCvt.reader -> (int, 'a) StringCvt.reader 58end; 59 60structure LargeInt: INTEGER = 61struct 62 (* Arbitrary precision int. *) 63 type int = LargeInt.int 64 65 fun toLarge i = i and fromLarge i = i 66 67 (* Whether int is short or long we can just cast it here. *) 68 val fromInt: Int.int -> int = RunCall.unsafeCast (* Just a cast. *) 69 70 (* If int is fixed precision we have to check that the value will fit. *) 71 fun toInt(i: int): Int.int = 72 if Bootstrap.intIsArbitraryPrecision orelse LibrarySupport.largeIntIsSmall i 73 then RunCall.unsafeCast i 74 else raise Overflow 75 76 val precision = NONE (* Arbitrary precision. *) 77 and minInt = NONE 78 and maxInt = NONE 79 80 val zero = fromInt 0 (* Avoids repeated use of fromInt. *) 81 82 fun abs (i: int): int = if i >= zero then i else ~ i 83 84 fun compare (i, j) = 85 if i < j then General.LESS 86 else if i > j then General.GREATER else General.EQUAL 87 88 fun min (i, j) = if i < j then i else j 89 and max (i, j) = if i > j then i else j 90 91 fun sign i : Int.int = if i = zero then 0 else if i < zero then ~1 else 1 92 93 fun sameSign(i, j) = 94 if i = zero then j = zero 95 else if i < zero then j < zero 96 else (* i > 0 *) j > zero 97 98 local 99 val fixedIntAsWord: FixedInt.int -> word = RunCall.unsafeCast 100 101 (* To reduce the need for arbitrary precision arithmetic we can try to 102 process values in groups. *) 103 (* Return the largest short value and the number of digits. *) 104 fun maxShort(n, radix, acc) = 105 if LibrarySupport.largeIntIsSmall(acc * radix) 106 then maxShort(n+1, radix, acc*radix) 107 else (acc, fixedIntAsWord n) 108 val (maxB, lenB) = maxShort(0, fromInt 2, fromInt 1) 109 and (maxO, lenO) = maxShort(0, fromInt 8, fromInt 1) 110 and (maxD, lenD) = maxShort(0, fromInt 10, fromInt 1) 111 and (maxH, lenH) = maxShort(0, fromInt 16, fromInt 1) 112 in 113 (* Local function *) 114 fun baseOf StringCvt.BIN = (2, maxB, lenB) 115 | baseOf StringCvt.OCT = (8, maxO, lenO) 116 | baseOf StringCvt.DEC = (10, maxD, lenD) 117 | baseOf StringCvt.HEX = (16, maxH, lenH) 118 end 119 120 local 121 open LibrarySupport 122 123 (* Int.toChars turned out to be a major allocation hot-spot in some Isabelle 124 examples. The old code created a list of the characters and then concatenated 125 them. This cost 3 words for each character before the actual string was 126 created. This version avoids that problem. This has also now been 127 modified to reduce the arbitrary precision arithmetic required when the 128 value is long. Instead of reducing it by the radix each time we take off 129 chunks of up to the maximum value that can be represented as a short precision 130 value. *) 131 132 fun toChar (digit: Int.int): char = 133 if digit < 10 then Char.chr(Char.ord(#"0") + digit) 134 else (* Hex *) Char.chr(Char.ord(#"A") + digit - 10) 135 in 136 fun fmt radix i = 137 let 138 val (base, maxShort, shortChars) = baseOf radix 139 val negative = i < zero 140 141 fun toChars(0, chars, continuation, pad) = 142 (* Finished the group. *) 143 if continuation = zero 144 then 145 ( 146 (* Really finished. Allocate the string. *) 147 if negative 148 then 149 let 150 val res = allocString(chars+0w1) 151 in 152 RunCall.storeByte(res, wordSize, #"~"); 153 (res, wordSize+0w1) 154 end 155 else (* Positive *) (allocString chars, wordSize) 156 ) 157 else (* Finished this group but have at least one more group. *) 158 let 159 val (result, pos) = toCharGroup(continuation, chars + pad) 160 fun addZeros n = 161 if n = pad then () 162 else (RunCall.storeByte(result, pos+n, #"0"); addZeros(n+0w1)) 163 in 164 addZeros 0w0; 165 (result, pos+pad) 166 end 167 168 | toChars(i, chars, continuation, pad) = 169 (* More to do in this group. *) 170 let 171 (* TODO: We haven't defined Int.quot and Int.rem yet although they 172 would be faster since we know this is short. *) 173 val ch = toChar (i mod base) 174 (* Get the string. *) 175 val (result, pos) = 176 toChars(i div base, chars+0w1, continuation, pad-0w1) 177 in 178 RunCall.storeByte(result, pos, ch); 179 (result, pos+0w1) 180 end 181 182 (* Process a group of characters that will fit in a short 183 precision number. *) 184 and toCharGroup(i, chars) = 185 if LibrarySupport.largeIntIsSmall i 186 then toChars(toInt i, chars, zero, 0w0) 187 else 188 let 189 val (q, r) = quotRem(i, maxShort) 190 in 191 toChars(toInt r, chars, q, shortChars) 192 end 193 in 194 if i = zero 195 then "0" (* This is the only case where we print a leading zero. *) 196 else 197 let 198 val (result, _) = toCharGroup(abs i, 0w0) 199 in 200 RunCall.clearMutableBit result; 201 result 202 end 203 end 204 end 205 206 val toString = fmt StringCvt.DEC 207 208 fun scan radix getc src = 209 let 210 val (base, _, _) = baseOf radix 211 val baseAsLarge = fromInt base 212 val sixteen = fromInt 16 213 214 (* Read the digits, accumulating the result in acc. isOk is true 215 once we have read a valid digit. *) 216 fun read_digits src acc isOk = 217 case getc src of 218 NONE => if isOk then SOME(acc, src) else NONE 219 | SOME(ch, src') => 220 if Char.ord ch >= Char.ord #"0" 221 andalso Char.ord ch < (Char.ord #"0" + base) 222 then read_digits src' 223 (acc*baseAsLarge + fromInt(Char.ord ch - Char.ord #"0")) true 224 else (* Invalid character - either end of number or bad no. *) 225 if isOk then SOME(acc, src) else NONE 226 227 fun read_hex_digits src acc isOk = 228 case getc src of 229 NONE => if isOk then SOME(acc, src) else NONE 230 | SOME(ch, src') => 231 if Char.ord ch >= Char.ord #"0" 232 andalso Char.ord ch <= Char.ord #"9" 233 then read_hex_digits src' 234 (acc*sixteen + fromInt(Char.ord ch - Char.ord #"0")) true 235 else if Char.ord ch >= Char.ord #"A" 236 andalso Char.ord ch <= Char.ord #"F" 237 then read_hex_digits src' 238 (acc*sixteen + fromInt(Char.ord ch - Char.ord #"A" + 10)) true 239 else if Char.ord ch >= Char.ord #"a" 240 andalso Char.ord ch <= Char.ord #"f" 241 then read_hex_digits src' 242 (acc*sixteen + fromInt(Char.ord ch - Char.ord #"a" + 10)) true 243 else (* Invalid character - either end of number or bad no. *) 244 if isOk then SOME(acc, src) else NONE 245 246 (* 247 There is a special case with hex numbers. A hex number MAY begin 248 with 0x or 0X e.g. 0x1f0 but need not. So "0x " and "0xg" are 249 both valid and represent the value 0 with "x " and "xg" as the 250 continuations of the input. 251 *) 252 fun read_number src = 253 if base = 16 254 then (* Hex. *) 255 ( 256 case getc src of 257 NONE => NONE 258 | SOME(ch, src') => 259 if ch <> #"0" 260 then read_hex_digits src zero false 261 else 262 ( 263 case getc src' of 264 NONE => SOME(zero, src') (* Accept the 0 *) 265 | SOME(ch, src'') => 266 if ch = #"x" orelse ch = #"X" 267 then 268 ( 269 (* 270 See if the characters after the 0x 271 form a valid hex number. If so return 272 that, if not return the 0 and treat 273 the rest of the string as starting 274 with the x. 275 *) 276 case read_hex_digits src'' zero false of 277 NONE => SOME(zero, src') (* Accept the 0 *) 278 | res => res 279 ) 280 else (* Start from the 0. *) 281 read_hex_digits src zero false 282 ) 283 ) 284 else (* Binary, octal and decimal *) read_digits src zero false 285 in 286 case getc src of 287 NONE => NONE 288 | SOME(ch, src') => 289 if Char.isSpace ch (* Skip white space. *) 290 then scan radix getc src' (* Recurse *) 291 else if ch = #"+" (* Remove the + sign *) 292 then read_number src' 293 else if ch = #"-" orelse ch = #"~" 294 then 295 ( 296 case read_number src' of 297 NONE => NONE 298 | SOME(i, r) => SOME(~i, r) 299 ) 300 else (* See if it's a valid digit. *) 301 read_number src 302 end 303 304 (* TODO: Implement this directly? *) 305 val fromString = StringCvt.scanString (scan StringCvt.DEC) 306 307 (* Converter to LargeInt values. *) 308 local 309 (* The string may be either decimal or hex. *) 310 fun convInt s = 311 let 312 val radix = 313 if String.size s >= 3 andalso String.substring(s, 0, 2) = "0x" 314 orelse String.size s >= 4 andalso String.substring(s, 0, 3) = "~0x" 315 then StringCvt.HEX else StringCvt.DEC 316 in 317 case StringCvt.scanString (scan radix) s of 318 NONE => raise RunCall.Conversion "Invalid integer constant" 319 | SOME res => res 320 end 321 in 322 (* Add a conversion function. *) 323 val () = RunCall.addOverload convInt "convInt" 324 end 325 326 open LargeInt (* Everything else. *) 327end; 328 329structure FixedInt: INTEGER = 330struct 331 (* This is now a fixed precision int. Currently it is the same as the short 332 form of an arbitrary precision int i.e. 31 bits on 32-bit machines and 333 63 bits on 63-bits. *) 334 type int = FixedInt.int (* Defined in the basis *) 335 336 (* Whether int is fixed or arbitrary precision we can just cast it here. *) 337 val toInt: int -> Int.int = RunCall.unsafeCast (* Just a cast. *) 338 339 (* If int is arbitrary precision we have to check that the value will fit. *) 340 fun fromInt(i: Int.int): int = 341 if LibrarySupport.isShortInt i 342 then RunCall.unsafeCast i 343 else raise Overflow 344 345 (* Conversion from fixed int to large is just a cast. It will always fit. *) 346 val toLarge: int -> LargeInt.int = RunCall.unsafeCast 347 348 (* When converting from arbitrary precision we have to check. *) 349 fun fromLarge(i: LargeInt.int): int = 350 if LibrarySupport.largeIntIsSmall i 351 then RunCall.unsafeCast i 352 else raise Overflow 353 354 local 355 fun power2' n 0 : LargeInt.int = n 356 | power2' n i = power2' (2*n) (i-1) 357 val power2 = power2' 1 358 val bitsInWord: int = (RunCall.unsafeCast LibrarySupport.wordSize) * 8 359 val wordSize = bitsInWord - 1 (* 31 or 63 bits *) 360 val maxIntP1 = power2(wordSize-1) 361 in 362 val precision = SOME(toInt wordSize) 363 val maxInt = SOME(fromLarge(maxIntP1-1)) 364 val smallestInt = fromLarge(~ maxIntP1) 365 val minInt = SOME smallestInt 366 end 367 368 fun scan radix rdr src = 369 case LargeInt.scan radix rdr src of 370 NONE => NONE 371 | SOME(i, c) => SOME(fromLarge i, c) 372 373 (* Converter to int values. This replaces the basic conversion 374 function for ints installed in the bootstrap process. In 375 particular this converter can handle hexadecimal. *) 376 local 377 fun convInt s = 378 let 379 val radix = 380 if String.size s >= 3 andalso String.substring(s, 0, 2) = "0x" 381 orelse String.size s >= 4 andalso String.substring(s, 0, 3) = "~0x" 382 then StringCvt.HEX else StringCvt.DEC 383 in 384 case StringCvt.scanString (scan radix) s of 385 NONE => raise RunCall.Conversion "Invalid integer constant" 386 | SOME res => res 387 end 388 in 389 val () = RunCall.addOverload convInt "convInt" 390 end 391 392 (* Can now open FixedInt. *) 393 open FixedInt 394 395 (* TODO: We should implement div and mod as built-ins because then they 396 can access the remainder and quotient directly. 397 Also, division by a power of two can be implemented as an 398 arithmetic shift because this rounds towards negative infinity 399 which is what we want. *) 400 401 fun compare (i, j) = 402 if i < j then General.LESS 403 else if i > j then General.GREATER else General.EQUAL 404 405 (*fun abs i = if i >= 0 then i else ~ i*) 406 407 fun min (i, j) = if i < j then i else j 408 and max (i, j) = if i > j then i else j 409 410 fun sign i = if i = 0 then 0 else if i < 0 then ~1 else 1 411 412 (* It might be possible to do something clever by xor-ing the 413 words together when both values are short. *) 414 fun sameSign(i, j) = 415 if i = 0 then j = 0 416 else if i < 0 then j < 0 417 else (* i > 0 *) j > 0 418 419 fun fmt r n = LargeInt.fmt r (toLarge n) 420 421 val fromString = StringCvt.scanString (scan StringCvt.DEC) 422 and toString = LargeInt.toString o toLarge 423 424 (* These are overloaded functions and are treated specially. *) 425(* val ~ : int->int = ~ 426 and op * : int*int->int = op * 427 and op + : int*int->int = op + 428 and op - : int*int->int = op - 429 430 val op < : int*int->bool = op < 431 and op > : int*int->bool = op > 432 and op <= : int*int->bool = op <= 433 and op >= : int*int->bool = op >=*) 434end; 435 436val () = RunCall.addOverload FixedInt.div "div" 437and () = RunCall.addOverload FixedInt.mod "mod"; 438 439(* Add extra overloadings for arbitrary precision. *) 440val () = RunCall.addOverload LargeInt.abs "abs" 441and () = RunCall.addOverload LargeInt.div "div" 442and () = RunCall.addOverload LargeInt.mod "mod"; 443 444local 445 (* Install the pretty printer for int *) 446 fun prettyFixed _ _ x = PolyML.PrettyString(FixedInt.toString x) 447 fun prettyLarge _ _ x = PolyML.PrettyString(LargeInt.toString x) 448in 449 val () = PolyML.addPrettyPrinter prettyFixed 450 and () = PolyML.addPrettyPrinter prettyLarge 451end; 452 453(* For the moment use arbitrary precision here. *) 454structure Position = LargeInt; 455 456(* The actual Int structure is defined depending on what int is. *) 457 458