Re: [isabelle] Target language bindings for rat

Dear Andreas,

Did you measure how much you gained from serialising rat to Haskell's
> Rational type (compared with using Code_Target_Int plus an appropriate
> setup to implement gcd on integer and int with Prelude.gcd)? In my quick
> experiment this morning, I could not see a significant speed-up.

Yes, I did. I also carried out quick experiments and noticed more or less
the same as you: Haskell's Rational type was just a little bit faster,
almost insignificant.

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

Good point, let me take a glance at it.

> Given that the generated ML code should work for all ML systems, I think
> we cannot take the serialisations of gcd into the distribution by default.

Yes, you are completely right. Each time I exported code, I had to decide
which serialisation was going to be used depending on the ML interpreter.


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