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


On Mon, Nov 4, 2013 at 11:26 AM, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> wrote:
> 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
>
>
> 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 (http://www.standardml.org/Basis/vector.html) 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 "IntInf.int".
>>
>> 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 unirioja.es ; web: http://www.unirioja.es/cu/jearansa
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.