Re: [isabelle] Haskell code-generation



On 03/31/2011 10:56 AM, Christian Sternagel wrote:
Thanks for all your fast answers,

just for clarification, I want to use Haskell's Int in order to be able to map many functions to Prelude functions (like mapping List.length :: 'a list => nat to length :: [a] -> Int). I'm aware that this might lead to inconsistencies (as Lukas already pointed out) -- not only because of potential overflows but also since you cannot be sure that the Prelude implementation is correct -- but for the time being I just wanted to be able to do it anyway :)

In the end I'm thinking of a "safe" version of the generated code and a "fast" version (using Int's and Prelude functions wherever possible).

It seems as if what Lukas has developed is exactly what I was searching for. But first I will thoroughly read through the code-generation manual (again) ;)


If this is of general interest, I am happy to move this development into a separate theory and incorporate your contributions. But I think we should discuss all the gory details offline.


Lukas
cheers

chris

On 03/31/2011 10:36 AM, Lukas Bulwahn wrote:
Hello Christian,


we also provide the type code_numeral for Integers (Haskell Integer) for
code generation, cf. src/HOL/Code_Numeral.thy

Currently, in development, I added a type code_int that I map to bounded
Integers (Haskell int), cf. src/HOL/Library/Quickcheck_Narrowing.thy
But I developed the necessary theory about code_int only as far as I
needed it for my purpose.
I am aware that the code generation setup for code_int could be
potentially unsound, if you exploit overflows in some tricky way.

By this replacement, I have measured an overall 50% speed-up by
replacing Integer by Int in my setting, the speed-up in the replaced
parts must be even larger.

But from my experience, foreseeing or estimating possible performance
increases in Isabelle's generated code is a difficult task.
E.g., it is still unclear to me, if the resulting non-overlapping code
equations from overlapping sequential function definitions make a
measurable performance difference in the runtime of the generated code.

Of course, these dedicated types code_numeral and code_int are for some
very special purposes, evaluation by code generation, with ML, nbe and
quickcheck, in the system.
They do not provide much theorems to reason about them, and should be
chosen with care.


Hope this helps.


Lukas


On 03/31/2011 09:48 AM, Andreas Lochbihler wrote:
Dear Christian,

Efficient_Nat does implement nat in terms of Haskell Integer, so the
comment is not wrong - provided you import Efficient_Nat as the *last*
theory in your import list in the theory where you invoke the Haskell
code generator. Even if you have imported Efficient_Nat in some
ancestor theory, reimport it.

However, nat is not literally translated to Integer, but wraps Integer
in a type Nat (cf. the generated Nat.hs). This seems necessary to do
because otherwise type class instantiations could not be
Isabelle-specific, e.g., division by 0 is defined in Isabelle whereas
not on Haskell integers. See also the comment in Efficient_Nat on this.

The easiest way to use the Haskell standard library is probably to
unpack Nat to Integer via toInteger and to wrap it back via
fromInteger whenever this is needed in your custom translations.

If you wish to replace Integer by Int, you will have to rewrite
Efficent_Nat.thy to use Int in all Haskell translations.

Possibly, Florian can tell you more on that topic.

Andreas









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