Email Gateway (Aug 18 2022 at 14:32): Email Gateway (Aug 18 2022 at 14:32):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
Is there any code-generator setup to generate 32/(64) bit integers with
modulo-arithmetic, mapped on the corresponding SML type (Word32) ?
In the logic, the type Word.word has the intended behaviour, but how to
get,e.g., "32 word", mapped to SML's "Word32" ?
Best,
Peter
Email Gateway (Aug 18 2022 at 14:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
there is, as far as I remember, a default setup for code generation for
type 'a word, but no mapping to any target-language-specific types. If
this is desired, it would be required to wrap up type expressions like
e.g. "64 word" into a dedicated type, say, "word64", to have dedicated
types for all the different 'a word instances. This wrapping is simple
but cumbersome to do.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:32):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Peter,
This topic is of interest to me. At the isabelle users workshop in
Munich last year I had a long discussion with Florian about precisely
this. The answer seemed to be "not with the current code generator", and
his argument felt convincing enough for me to leave that approach alone.
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.
That or trying to write your own code generator, which might be...
interesting.
Sincerely,
Rafal Kolanski.
Peter Lammich wrote:
Email Gateway (Aug 18 2022 at 14:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
to be more precise, what we would need is a tool which inside the logic
lifts operations on type "64 word" to a dedicated type "word64". What
could already provide helpful assistance is the "transfer" tool by Amine
Chaieb and Jeremy Avigad, whose basic usage can be followed in
src/HOL/Nat_Transfer.thy.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:44):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 14:46):From: Michael Norrish <Michael.Norrish@nicta.com.au>
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.
Email Gateway (Aug 18 2022 at 14:47):From: Makarius <makarius@sketis.net>
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
values.
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 ...
Makarius
Last updated: Apr 23 2024 at 04:18 UTC