Re: [isabelle] Target language bindings for rat
concerning division on integers, I also observed some optimization potential, which is save in a way that
it only invokes the divmod on positive numbers. At least
in my application gave a significant speedup, cf.
> Am 18.12.2015 um 14:02 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:
> 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
>> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and