[Smlnj-list] Integers in SMLNJ

[Amine C. <ch...@in...>]

Dear all,

Here is a serious request about integers in SML-NJ which has been sent 
by Makarius Wenzel. If this is not the appropriate place, please tell us 
where to post it.

Otherwise, the Message: (Note that there are two messages: the request 
to the developpers at the end, and a first from an internal discussion 
already gives the solution).


----- Messages by Makarius --------

Please observe the message below, which I've sent to smlnj-dev recently
without ever getting a response.  Maybe you have better connections to
some of the core developers ...


Due to the confusion of Int vs. IntInf in SML/NJ we have presently
dactivated new arithmetic tools by Amine when running under smlnj.  He
convinced me that it is better to invest time to solve the problem once
and for all, rather than adapt individual tools. (Other users also got
enthusiastic about the prospect, even though it was never announced widely
so far.)

Last week I've actually managed to get proper ints in SML/NJ by just
changing a single line in the compiler sources:

diff -r 110.62/base/compiler/Elaborator/types/overloadlit.sml 
110.62-test/base/compiler/Elaborator/types/overloadlit.sml
39c39
<   fun default T.INT = BT.intTy
---
 >   fun default T.INT = BT.intinfTy

The rest happens in our compatibility files for smlnj.  All of Isabelle
compiled successfully with this, but there is a runtime penalty of
something like 20-40% in real applications.  (NJ's IntInf implementation
is *very* naive -- they even admit this their sources.)

Ideally, the SML/NJ people would provide a compiler option for future
working versions of their system for the above.  Then we get the
flexibility to compile Isabelle with smlnj either with partial Int or full
(but slower) Int = IntInf.  In any case the distinction in the sources
would disappear, thus reducing our worries significantly.


	Makarius

---------- Forwarded message ----------
Date: Tue, 12 Jun 2007 11:45:42 +0200 (CEST)
From: Makarius <mak...@sk...>
To:  <sml...@li...>
Subject: IntInf.int as default?

Dear SML/NJ developers,

after adding some advanced arithmetic proof procedures to the Isabelle
system we have run into a serious maintenance problem wrt. the SML/NJ
platform (most of our developers use Poly/ML by default).

The problem is caused by type Int.int vs. IntInf.int, which are different
in SML/NJ, but coincide in Poly/ML.  Occasionally, people have tried to
use IntInf explicitly, but this has only complicated the sources (due to
extra variety of int types) without really solving the problem.  Even
worse, some code generation facilities for Isabelle (HOL -> SML) include
certain choices of int representation which are hard to change by users
later on.


Is there an easy way to make IntInf.int the default int type in SML/NJ?
Ideally it would be something analogous to ``perl -Mbigint'', although I
reckon it's not that simple.

We have experimented with something like ``type int = IntInf.int'' before
compiling Isabelle, and using wrappers around the usual basis library
modules to use that type uniformly.  The remaining problem is the default
for overloaded literals and +, -, * etc.  Maybe one could just modify
compiler/Elaborator/types/overloadlit.sml accordingly, cf. the following
existing source:

   (* eventually, these may be defined elsewhere, perhaps via some
      compiler configuration mechanism *)
   val intTypes = [BT.intTy, BT.int32Ty, BT.int64Ty, BT.intinfTy]

   ...

   fun default T.INT = BT.intTy 

     ...

I wonder if it could be as simple as making the ``default'' function
depend on a global compiler flag, to use BT.intinfTy instead of BT.intTy.

What do you think?


	Makarius