Re: [isabelle] Target language bindings for rat
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
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:
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 inf.ethz.ch
<mailto:andreas.lochbihler at inf.ethz.ch>>:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and