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 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).
We used to have separate Int vs. IntInf over a few years (2004-2007), but
it was so awkward in mixed tool implementations that people knocked at my
door and were asking for more uniformity. So I made some tricks to get
int = IntInf.int in SML/NJ.
Now I've started to think about separate int types again, but it would
probably be a big upheaval in parts of the system that don't have active
maintainers.
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 :-).
The reason for thinking about discontinuation of SML/NJ is not its
constant annoyance wrt. type errors, but more profane: many Isabelle
sessions run out of memory, even basic things like HOL-Library. So the
question needs to be revisted seriously in a few weeks on isabelle-dev
mailing list -- it will have far-reaching consequences to have just one ML
platform.
Makarius
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
