Re: [isabelle] Code generation for "int" in Isabelle 2013-1 RC3
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"
"findi_integer f arr =
Option.map (apfst integer_of_nat) (findi (f o apfst integer_of_nat) arr)"
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,
On 04/11/13 08:50, Jesus Aransay wrote:
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
Thanks in advance for any advice,
This archive was generated by a fusion of
Pipermail (Mailman edition) and