> On 10 Feb 2016, at 17:01, Makarius <makar...@sketis.net> 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: > http://isabelle.in.tum.de/repos/isabelle/file/9343649abb09/src/Pure/RAW/proper_int.ML
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 operators of Int or IntInf as appropriate (selected at compile-time by using a conditional compilation feature that is built into the way ProofPower packages ML code into documents). ProofPower builds and tests fine using poly built from the FixedPrecisionInt branch after tweaking the conditionally compiled bits of code so that Poly/ML is treated just like Standard ML of New Jersey in the definition of the type INTEGER. (And tweaking a few tests that accidentally forgot that INTEGER and int are not necessarily the same.) >> I'm inclined to think that having a "configure" option would be the answer. > I think that's a good idea, but it gives me a bit of problem as my conditial compilation is based on the compiler and not how the compiler has been configured. > That would greatly simplify the Isabelle setup, because we always provide a > separately compiled version of Poly/ML. I can see why you do that, but I don't want to do it for ProofPower. So if we have a "configure" option, then it would be good for me if there some well-defined way, e.g., using "poly -v", for a build script to find out how a pre-installed Poly/ML installation has been configured. > > Since we are about to discontinue SML/NJ altogether, it would allow to remove > the above tricks, and not move them over to Poly/ML. I can unerstand why you are doing that too, but in this case I'm really glad I tried to maintain compatibility, as it meant I already had almost everything I needed to accommodate the proposed change :-). All that said, I would be surprised if the change made any significant performance improvement on any of my code, because anything that is computationally intensive in the theorem prover tends to be dealing with object language data, and, if that data is numeric, it will be arbitrary precision. Regards, Rob. _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
