Re: [isabelle] Target language bindings for rat



> I was also a bit surprised by your comparison of serialisation options for
> divmod_integer in Code_Generation_IArrays_SML. In SML, quotRem and divMod
> behave differently when it comes to negative numbers. In that respect,
> quotRem is the wrong choice. For example,
> quotRem (~10, 6) evaluates to (~4, ~6) and divMod (~10, 6) to (~2, 2). In
> Isabelle/HOL,
> value [nbe] "divmod_integer (-10, 6)" gives (-2, 2). So the generated code
> may actually return a different result than what you have proved. (I do not
> know whether such negative numbers can occur in your application).
>


I think it works for my concrete case (integer numbers are only used for
representing rational numbers), however for a general integer manipulation
this is not a correct serialisation.

In my exported code, quot is only used when nomalising rational numbers (by
means of the Rat.normalise definition). If I am not wrong, for such a
function it is the same using "div" as using "quot".

So, "-20 div 6" would return different results (as expected), but normalize
(-20,6) the same:

code_printing
constant "op div :: integer => _ => _" â (SML) "(IntInf.div ((_), (_)))"
| constant "op mod :: integer => _ => _" â (SML) "(IntInf.mod ((_), (_)))"

value[code] "-20 div 6::int" (*Result: - 4*)
value[code] "Rat.normalize (-20,6)" (*Result: (-10,3) :: "int à int"*)


code_printing
constant "op div :: integer => _ => _" â (SML) "(IntInf.quot ((_), (_)))"
| constant "op mod :: integer => _ => _" â (SML) "(IntInf.rem ((_), (_)))"

value[code] "-20 div 6::int" (*Result: - 3 :: "int"*)
value[code] "Rat.normalize (-20,6)" (*Result: (-10,3) :: "int à int"*)

Then, I took advantage of it and decided to use quot, since it is supposed
to be faster. Nevertheless, I have to study it carefully again because
maybe I am wrong.

Best,
Jose



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