Re: [isabelle] Word32/64 ?



On 05/02/10 08:40, Makarius wrote:
On Wed, 27 Jan 2010, Rafal Kolanski wrote:

One approach for high-performance code seems to be going in reverse,
i.e. parsing annotated SML/C/Haskell/whatever into Isabelle, where you
can pick your own translation, but have to pay by having to specify
the semantics also.

BTW, "high-performance" in SML (as implemented in Poly/ML) means to use
the default int, i.e. the proper mathematical (unbounded) integers, not
machine words. Poly/ML optimizes the representation of values for the
demands of symbolic computation, not for bare metal operations. So
proper ints, lists (cons cells), datatypes are fast, but Word32 is
really slow.

But then, if you are emitting SML, and really wanting speed, you'll probably compile with MLton; at least until you can emit code to exploit Poly/ML threads.  MLton uses the gmp library to implement its IntInf structure, so if you target that explicitly, you will get infinite integers.  Otherwise, you will get native machine integers.

Michael.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.