Re: [isabelle] Target language bindings for rat



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:
http://afp.sourceforge.net/browser_info/current/AFP/Gauss_Jordan/Code_Rational.html

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
http://afp.sourceforge.net/browser_info/current/AFP/Gauss_Jordan/Code_Generation_IArrays_SML.html.
Without such GCD serialisations, i.e. only using Code_Target_Int, times
were 20 times slower in my case.

Best,
Jose

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.
>
> Thanks,
> Andreas
>
>



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