Re: [isabelle] Target language bindings for rat



Dear all,

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.

http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Improved_Code_Equations.html

Cheers,
RenÃ

> 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
>> 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.