[Agda] is divMod slow?

[Sergei Meshveliani]

On Mon, 2017-06-19 at 22:27 +0200, Ulf Norell wrote:
> 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



1. What is a _regular_ way to download it? to use? 

Is  divMod  programmed there as built-in, or as an Agda program loop? 


2. Another point.
As I understand, the current Standard library implements  _+_ and _*_ on
Nat simply as built-in, with postulating certain main properties
(may be, like this:  ∀ n -> suc-built-in n ≡ suc n).
Right?

Is it difficult to apply the same approach to  divMod ?
So that  divMod m (suc n) --> (q , r),
where 
q and r are computed as built-in (say, as in GHC, or as in the gmp
library),
and the properties of  q * (suc n) + r ≡ m,   r < m
are postulated
?

Can people, please, tell me, how to arrange this?

Thanks,

------
Sergei



> 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
> 
>