Re: [isabelle] Haskell code-generation



Hi Christian,

> 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.

thanks for pointing that out, this seems to have been wrong from the
very beginning.  Fixed in the hg repository (rev b992c8e6394b).

> 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?).

Well, for Haskell indeed Integers are used for consistency.  But if your
code involves massive computation on considerably large nats,
Efficient_Nat should bring a considerable speedup.  Maybe the bottleneck
is somewhere else?  A clear statement requires an inspection of the
corresponding code.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



Attachment: signature.asc
Description: OpenPGP digital signature



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