Re: [isabelle] Haskell code-generation

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.


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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