[Agda] is divMod slow?

[Ulf Norell]

The divMod implementation of the standard library is indeed horribly slow.
If you need fast certified divMod (and gcd) you can check out the
implementation in the agda-prelude library [1].

/ Ulf

[1] https://github.com/UlfNorell/agda-prelude/tree/master/src/Numeric/Nat

On Mon, Jun 19, 2017 at 9:24 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Dear Standard library developers,
>
> I test
>        (suc n) mod (suc (suc n))
>        where
>        mod = Data.Nat.DivMod.mod
>
> for  n = 123456789.
>
> The result is correct (and trivial), but it takes   ** 6 seconds **
> on a 3 GHz machine.
> It is written in  Data.Nat.DivMod that _mod_ is implemented via
> Agda.Builtin.Nat.mod-helper.
>
> Probably, this means that it relies on something like `mod' of Haskell
> standard library implemented in GHC.
> But `mod' of GHC computes this in less than 0.0001 sec
> (somewhat one machine command for division of two macrodigits).
>
> Currently the Nat arithmetic in Agda Standard library is fast because it
> is via built-ins. But divMod is also of important arithmetic.
> What about  divMod ?
> For example, arithmetic of rational numbers rely on gcd for Nat, and gcd
> relies on mod (divMod).
>
> What is happening there?
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170619/ac6f0811/attachment.html>