Thanks for the various comments on fixed precision integer. I've now implemented two different mechanisms for compatibility with arbitrary precision int.
There is a configure option --enable-intinf-as-int. This causes polyimport to build the basis library with int as arbitrary precision integer rather than fixed precision.
The second mechanism is to build a module. Calling PolyML.loadModule "IntAsIntInf"; loads a module that sets the compiler's default overloading to arbitrary precision and loads replacements for most of the basis library. I added modules to Poly/ML 5.6 as a way of providing extensions to the existing basis library and this is the first example. Note that this assumes that "poly" has been installed using "make install" and the module has been copied to its installation location. If you're testing it within the build tree you need PolyML.loadModule "modules/IntAsIntInf/IntAsIntInf";
There are a few cases that aren't covered but they are only likely to affect a few people. Specifically, when installing pretty printers the "depth" argument is always FixedInt.int. There may be a few other case where functions are tightly integrated into the compiler. The IntAsIntInf module covers most of the basis library but currently excludes socket IO and a few other cases. It can probably be extended as necessary.
David
On Mon, 22 Feb 2016, David Matthews wrote:
There is a configure option --enable-intinf-as-int. This causes polyimport to build the basis library with int as arbitrary precision integer rather than fixed precision.
I have adapted to this change here: http://isabelle.in.tum.de/repos/isabelle/rev/ad3eb2889f9a
It works fine. I am rather glad that only some ML pretty printing required a different (approximative) int type.
Makarius
On 23/02/2016 19:05, Makarius wrote:
On Mon, 22 Feb 2016, David Matthews wrote:
There is a configure option --enable-intinf-as-int. This causes polyimport to build the basis library with int as arbitrary precision integer rather than fixed precision.
I have adapted to this change here: http://isabelle.in.tum.de/repos/isabelle/rev/ad3eb2889f9a
It works fine. I am rather glad that only some ML pretty printing required a different (approximative) int type.
I'm glad it's not too painful. I need to check more carefully that there aren't any other cases that really need to be fixed-precision but I think that's probably all.
One of the things I want to do as a result of removing arbitrary precision emulation is improve the way that long-form arbitrary precision values are handled. With emulation there is a sort of "cliff edge" where short-form values are handled very efficiently but long-form values that actually require emulating are considerably slower. Removing emulation should ultimately allow calls to C functions, such as the GMP library, to be speeded up.
David
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net