Re: [isabelle] Code generation for "int" in Isabelle 2013-1 RC3

Dear Andreas,

thanks for the hints, they allowed me to solve the problem; I also got
to read in the code generation manual (version in Isabelle 2013-1 RC3)
about he Isabelle types "integer" and "natural" in "Code_Numeral",
which are conceived to be used in the code generation setup as indexes
in target-language arrays.Thanks also to Florian for persuading me to
install Isabelle 2013-1 RC3 and try the new code generation setup.

Thanks to this we produced a serialisation of some additional
functions (not included in "IArray.thy") over "iarray" to SML "Vector"
functions (see the attached file "IArray_Addenda.thy"), and also a
serialisation in Haskell of Isabelle "iarray" to  the class
(see the attached file "IArray_Haskell_RC3.thy"). Maybe somebody could
find them useful.

Feel free to comment on them or suggest any improvements,

best wishes,


On Mon, Nov 4, 2013 at 11:26 AM, Andreas Lochbihler
<andreas.lochbihler at> wrote:
> Dear Jesus,
> In the upcoming release, target language numerals like are
> properly encapsulated in their own types integer and natural. Formerly, the
> adaptation theories made the SML code generator to implement the types nat
> and int directly as, now Code_Target_Numeral implements both as
> type copies of to enforce the separation. Consequently, you
> cannot exploit the former clash of types any more. You have to define an
> function that operates directly on integer rather than nat. For example:
> definition findi_integer ::
>   "(integer * 'a => bool) => 'a iarray => (integer * 'a) option"
> where
>   "findi_integer f arr =
> (apfst integer_of_nat) (findi (f o apfst integer_of_nat) arr)"
> code_printing
>     constant findi_integer => (SML) "Vector.findi"
> Of course, you also have to use findi_integer instead of findi in your code
> equations or prove a corresponding code equation for findi.
> Hope this helps,
> Andreas
> On 04/11/13 08:50, Jesus Aransay wrote:
>> Dear all,
>> the code generation snippet in the attached file worked in Isabelle
>> 2013 but fails in Isabelle 2013-1 RC3; a function resembling the SML
>> Vector.findi ( is
>> introduced in Isabelle, and then serialised to SML Vector.findi, but
>> apparently there is a clash between the Isabelle code generated
>> structure "int" and the SML "".
>> I have tried to import "Code_Target_Int" with similar result.
>> Is there an easy way to avoid such clash? (I could edit the SML code
>> by hand and fix types' declarations, but does not seem a proper
>> solution).
>> Thanks in advance for any advice,
>> Jesus

Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at ; web:
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

Attachment: IArray_Addenda.thy
Description: Binary data

Attachment: IArray_Haskell_RC3.thy
Description: Binary data

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