[Agda] timing for agda-prelude gcd

[Sergei Meshveliani]

On Thu, 2017-06-22 at 07:44 +0200, Ulf Norell wrote:
> 
> 
> On Wed, Jun 21, 2017 at 10:20 PM, Sergei Meshveliani
> <mechvel at botik.ru> wrote:
>         Dear all,
>         
>         Earlier there was discussed in this list the performance of _
>         +_ and _*_
>         on Nat. I provided a test program.
>         And as I recall, the performance is high: as in the Haskell
>         program for
>         ghc-7.10.2.
>         
>         Now I need fast  divMod and gcd  for Nat.
>         Standard library is very-very slow at this point.
>         
>         So I try  agda-prelude.
>         It shows considerably faster.
>         But it is still slower than  GHC.
>         gcd  is about  12 times  slower,
>         and  divMod  is about 4000 times slower (?).
> 
> 
> divMod isn't slow, the problem is that you are using ≤? from the
> standard library in
> your implementation of max. If you replace it by ≤? from agda-prelude
> the Agda code
> [..]


Thank you.  I see now that  divMod and gcd  of agda-prelude are fast
enough.

I suspected some mistake of mine of this sort in the test.

Now, I tried first to replace _≤?_. This leads to using Bool. 
Also 
     decimalDigit? c = ... (48 ≤? n) ∧ (n ≤? 57)

caused a strange report about not finding the Ord instance for
something.

So, I removed _≤?_ at all, and replaced  max  with  sum.
And now the test is indeed almost as fast as the GHC library.
 
Improving Nat performance by using both Standard library and
agda-prelude meets various technical difficulties. A headache.
Probably, Standard library needs improvement in implementation of 
_≤?_ and divMod.

Regards,

------
Sergei