Re: [isabelle] Word32/64 ?
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] Word32/64 ?
- From: Makarius <makarius at sketis.net>
- Date: Thu, 4 Feb 2010 22:40:12 +0100 (CET)
- In-reply-to: <4B5EF5B9.firstname.lastname@example.org>
- References: <4B5EF263.email@example.com> <4B5EF5B9.firstname.lastname@example.org>
- User-agent: Alpine 1.10 (LNX 962 2008-03-14)
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and