[isabelle] Haskell code-generation



Hi all,

recently I tried to embed some generated code more deeply into the Haskell standard library (by using Prelude functions whenever possible). The initial problem (which many of you may know) is that whenever in Isabelle you are using "nat" the corresponding Haskell function would use either Int or Integer... since many Prelude functions are using Int, lets just assume that Int should replace "nat" (ignoring the fact that nat's may get arbitrarily large but Int's don't).

First HOL/Library/Efficient_Nat.thy seemed exactly to be what I needed, but unfortunately it doesn't seem to hold what is claimed in the header: "The efficiency of the generated code can be improved
drastically by implementing natural numbers by target-language
integers.  To do this, just include this theory."

I did just import Efficient_Nat.thy, is there anything else to do afterwards (maybe for Haskell Integers are used instead of Int's?).

Does anybody have experience with using Efficient_Nat for Haskell code-generation?

cheers

chris

A minor comment: the code-generator setup for Haskell (in HOL.thy) declares "&&" and "||" as infixl, whereas in Haskell's Prelude they are declared infixr.





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