[isabelle] Haskell code-generation
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Haskell code-generation
- From: Christian Sternagel <christian.sternagel at uibk.ac.at>
- Date: Thu, 31 Mar 2011 09:17:36 +0200
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:220.127.116.11) Gecko/20110307 Fedora/3.1.9-0.39.b3pre.fc14 Lightning/1.0b2 Thunderbird/3.1.9
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
A minor comment: the code-generator setup for Haskell (in HOL.thy)
declares "&&" and "||" as infixl, whereas in Haskell's Prelude they are
This archive was generated by a fusion of
Pipermail (Mailman edition) and