Re: Integers in SMLNJ

It seems to me that the root of this problem is that the Isabelle code
is not being written in a portable way.  Code that assumes that  
Int.int = IntInf.int
is not going to be portable; anymore than code that assumes Int.int =  
Int31.int.
With some care, it is possible to write code that avoids these  
assumptions.

As far as changing the default int type to IntInf goes, I'm surprised  
that
other stuff doesn't break.  For example, array bounds checking code  
would
not normally work with IntInf.int indices.

	- John

On Aug 10, 2007, at 8:21 AM, Amine Chaieb wrote:

> 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 <[email protected]>
> To:  <[email protected]>
> 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
>
>
> ---------------------------------------------------------------------- 
> ---
> This SF.net email is sponsored by: Splunk Inc.
> Still grepping through log files to find problems?  Stop.
> Now Search log events and configuration files using AJAX and a  
> browser.
> Download your FREE copy of Splunk now >>  http://get.splunk.com/
> _______________________________________________
> Smlnj-list mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/smlnj-list
>


-------------------------------------------------------------------------
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems?  Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >>  http://get.splunk.com/