Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 19 2022 at 12:48):

From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
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
"Data.Array.IArray.Array"
(http://cvs.haskell.org/Hugs/pages/libraries/base/Data-Array-IArray.html)
(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,

Jesus
IArray_Addenda.thy
IArray_Haskell_RC3.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 12:54):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jesus,

In the upcoming release, target language numerals like IntInf.int 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 IntInf.int, now
Code_Target_Numeral implements both as type copies of IntInf.int 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 =
Option.map (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

Last updated: Apr 25 2024 at 20:15 UTC