Re: [isabelle] Target language bindings for rat
On 18/12/15 13:56, Jose DivasÃn wrote:
Rat.normalise only divides by divisors, so the remainder is always 0 and the problem
should not occur in this case.
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
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and