Re: [isabelle] Target language bindings for rat

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.