Re: [isabelle] Target language bindings for rat



Dear Jose,

On 18/12/15 13:56, Jose DivasÃn wrote:
    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".
Rat.normalise only divides by divisors, so the remainder is always 0 and the problem should not occur in this case.

Best,
Andreas




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