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