[Agda] is divMod slow?

[Sergei Meshveliani]

On Tue, 2017-06-20 at 12:04 +0200, Ulf Norell wrote:
> 
> 
> On Tue, Jun 20, 2017 at 11:42 AM, Sergei Meshveliani
> <mechvel at botik.ru> wrote:
>         
>         1. What is a _regular_ way to download it? to use?
> 

> There are separate branches of the library for the different releases
> of Agda (the master branch should work with the stable branch of
> Agda). For instance, if you are using Agda-2.5.2 you should download
> the compat-2.5.2 branch using the command
>
>   git clone -b compat-2.5.2 https://github.com/UlfNorell/agda-prelude



I use  Agda 2.6.0-207bde6,  

and I recall that, probably, 2.5.2 is not sufficient for my code.

Will  compat-2.5.2  work under  Agda 2.6.0-207bde6 ?

And I need  gcd  on Nat  nearly as fast as in GHC on Integer.
Or at least, a fast  divMod.

Thanks,

------
Sergei




> You should then add the path to agda-prelude.agda-lib to your
> ~/.agda/libraries file (and optionally add agda-prelude to the
> defaults file).
> 
> 
> If you didn't add agda-prelude to the defaults file you need to add a
> "depend" field to your project agda-lib file.
> 
> 
>         
>         Is  divMod  programmed there as built-in, or as an Agda
>         program loop?
> 
> 
> It's programmed using the div-helper and mod-helper functions from
> Agda.Builtin.Nat. These are builtins which have an Agda definition but
> are evaluated using primitive Haskell functions. See below.
>  
>         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?
> 
> 
> This is not how it works. _+_ and _*_ have Agda definitions (which you
> can find in Agda.Builtin.Nat), so all desired properties can be proven
> without postulates. However, when these functions are applied to
> closed natural numbers (like 15 or 421783423) they are evaluated using
> the corresponding primitive Haskell functions instead of the Agda
> definitions.
>  
>         Is it difficult to apply the same approach to  divMod ?
> 
> 
> This is exactly what agda-prelude does (applying the approach I
> described above, that is).
> 
> 
> / Ulf