Re: [isabelle] Target language bindings for rat

Dear Jose,

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.

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

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.


On 18/12/15 11:43, Jose DivasÃn wrote:
Dear all,

in my AFP about the Gauss-Jordan algorithm I worked with rational matrices, so I
serialised the rational numbers from Isabelle to Haskell, see:

For exporting code to SML, I just used the file Code_Target_Int together with
serialisations from gcd to PolyML.IntInf.gcd and MLton.IntInf.gcd (as far as I know, there
is no gcd implementation in the standard library). I also serialised the operations div
and mod, see
Without such GCD serialisations, i.e. only using Code_Target_Int, times were 20 times
slower in my case.


2015-12-18 10:39 GMT+01:00 Andreas Lochbihler <andreas.lochbihler at
<mailto:andreas.lochbihler at>>:

    Hi Manuel,

    On 18/12/15 09:29, Manuel Eberl wrote:

        On 18/12/15 09:01, Lochbihler Andreas wrote:

            I noticed a nice speedup (ca. 3X for Haskell and 10X for OCaml) over

        the existing setup for rat with Code_Target_Int in place.

        I find that a bit surprising, considering how rats are implemented in
        Haskell. One possible explanation that I have is that perhaps the
        exported code uses Isabelle's GCD operation on natural numbers, whereas
        the Haskell version uses the GCD operation that GMP provides, and which
        is probably much faster.

    Your guess seems to be right. If I serialise the gcd operation on integer to the
    target language implementation, the differences almost vanish.

        Another possible reason is perhaps some issue with lazyness; Haskell's
        "Ratio" datatype is declared with strict fields, whereas Isabelle
        probably declares "rat" with the lazy fields. Perhaps this can cause
        large unevaluated chunks to hang around longer than they should?

        However, the fact that the difference is even more pronounced in OCaml
        seems to speak against that. I don't know the OCaml implementation, so I
        don't know if the GCD thing might also be an explanation there.

    It is.


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