Re: [polyml] Fixed precision int and compatibility

2016-02-24 Thread David Matthews
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:

Re: [polyml] Fixed precision int and compatibility

2016-02-23 Thread Makarius
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:

Re: [polyml] Fixed precision int

2016-02-10 Thread David Matthews
On 10/02/2016 15:41, Anthony Fox wrote: This is significant change. Would it be possible to make this user selectable? MLton has the command line flag -default-type intinf when IntInf is preferred for Int. Perhaps there could be a switch to "configure". It's really a question of how the

Re: [polyml] Fixed precision int

2016-02-10 Thread David Matthews
Anthony, I'm copying the mailing list to my replies because this is of general interest. On 10/02/2016 16:02, Anthony Fox wrote: I just occurred to me that I could have done: structure Int :> INTEGER = IntInf if I wanted IntInf everywhere (rather than having the choice of fixed ot

Re: [polyml] Fixed precision int

2016-02-10 Thread David Matthews
On 10/02/2016 16:18, Anthony Fox wrote: Can you provide some more information and try to narrow the problem down? There certainly shouldn't be bus errors or segmentation faults anywhere. I removed the files $POLYDIR/lib/libpoly* before doing an Poly/ML install and that seemed to fix

Re: [polyml] Fixed precision int

2016-02-10 Thread Rob Arthan
> On 10 Feb 2016, at 17:01, Makarius wrote: > > On Wed, 10 Feb 2016, David Matthews wrote: > > This reminds me of the situation in SML/NJ, before I spent some efforts to > force int = IntInf.int on it. It includes a somewhat "patched" basis library > like this: >

Re: [polyml] Fixed precision int

2016-02-10 Thread Makarius
On Wed, 10 Feb 2016, Rob Arthan wrote: ProofPower takes a different approach to this: it uses the compiler's native integers except where logical soundness requires an IntInf, where it uses a type it defines called INTEGER, which has its own operations @+, @-, @* etc. implemented using the

[polyml] Fixed precision int

2016-02-10 Thread David Matthews
From the start int in Poly/ML has been arbitrary precision. After around thirty years I think it's time to make a change. The current plan is to introduce a fixed precision integer type and use that as the default int. Arbitrary precision will remain as LargeInt.int/IntInf.int. The reason