Re: [isabelle] Target language bindings for rat
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>:
> 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