Re: [isabelle] Word32/64 ?
On Fri, 5 Feb 2010, Michael Norrish wrote:
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
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.
In the "long" form Poly/ML integers are definitely slower than anything
more modern out there (even Java BigInt which appears to be pure Java).
But the nice thing about the default int type in Poly/ML is that you get
almost full speed machine arithmetic until you degrade gracefully to the
long form. This works, because 1 or 2 bits are sacrificed for tagging of
So the reason why Word32 is slow (it needs to be boxed) is the same reason
why proper int is fast (a machine word can be either a "short" int, or a
boxed "long" one).
While this tagging business appears to be ancient LISP technology, nobody
appears to be using it in the C-derived universe (including Java). This
is one of the reasons why there is now so much opportunity to do
verification involving unsafe word arithmetic as we all know ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and