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



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





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