[Agda] is divMod slow?

[Jorn van Wijk]

The divMod implementation of the standard library is also implemented using
the div-helper and mod-helper functions from Agda.Builtin.Nat.
https://agda.github.io/agda-stdlib/Data.Nat.DivMod.html#4861

This makes me wonder in what way the prelude version differs from the
standard library version.

Kind regards,
Jorn

2017-06-20 12:34 GMT+02:00 Sergei Meshveliani <mechvel at botik.ru>:

> 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
>
>
> _______________________________________________
> 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/20170620/7e5a64e7/attachment.html>