Re: [isabelle] Haskell code-generation

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.


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.


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