[Agda] gcd, toDecimal performance

[Matthew Daggitt]

Hi Sergei,
 Glad to hear that we've managed to speed up `div` and `mod` for you. Yes,
the code for GCD and LCM is quite old at this point and can probably be
made more efficient. Probably best to make an issue on the standard library
Github and then either you, or if you're lucky someone else, will get
around to doing it.
Best,
Matthew

On Tue, Mar 26, 2019 at 2:30 AM Sergei Meshveliani <mechvel at botik.ru> wrote:

> Concerning printing large Nat:
>
> the following function  show' : ℕ → String
>
> prints large numbers many times faster than  Data.Nat.Show.show,
> it is `exponentially' faster.
> So that the point III below can be fixed somewhat this way,
> and it remains the point II of gcd.
>
> ---------------------------------------------------------------
> LChar = List Char
>
> toDigitChar : (n : ℕ) → Char
> toDigitChar n =
>               Char.fromNat (n + 48)
>
> 1<10 : 1 < 10
> 1<10 = s≤s (s≤s z≤n)
>
> {-# TERMINATING #-}
> toDecimalChars : ℕ → LChar
> toDecimalChars x =  aux x []
>   where
>   aux : (n : ℕ) → LChar → LChar
>   aux 0       =  ('0' ∷_)
>   aux (suc n) =
>            let q = (suc n) div 10    -- Only avoid _divMod_
>                r = (suc n) %   10    -- of the current Standard!
>                c = toDigitChar r
>            in
>            case q ≟ 0 of \ { (yes _) → (c ∷_)
>                            ; (no _)  → aux q ∘ (c ∷_) }
>
> show' : ℕ → String
> show' = Str.fromList ∘ toDecimalChars
>
> test : show' 1090 ≡ "1090"
> test = refl
> ----------------------------------------------------------------------
>
>
> --
> SM
>
>
>
> On Mon, 2019-03-25 at 18:53 +0300, Sergei Meshveliani wrote:
> > Dear standard library developers,
> >
> > I wrote recently about the performance of divMod for Nat and rational
> > arithmetics, and Ulf issued some comments.
> >
> > But now I discover news, when look into  Dat.Nat/
> > in the
> >    experimental lib branch for Agda-2.6.0-candidate.
> >
> > There appear _≡ᵇ_, _<ᵇ_, div-mod-helper
> >
> > which use built-ins from GHC.
> > Also the attached test shows that mod (_%_) and _div_ are fast enough.
> >
> > (1) But  gcd  remains `exponentially' slow.
> > This is strange. Because  gcd  is usually found by applying divMod a few
> > times.
> > This slow  gcd  will actually break rational arithmetic.
> >
> > (2) Printing Nat (in decimal digits) is `exponentially' slow.
> > This is also strange. Because conversion from unary to decimal system
> > can be written as something like applying (\n -> divMod n 10) a few
> > times.
> > Am I missing something?
> >
> > Can you, please, fix these two features?
> > I guess this is not difficult, because standard library currently has
> > all the needed fast functions.
> >
> > Please try the  _attached test_.
> >
> > It
> >  reads  n : Nat  from  data.txt  (n = 10, 11, 12, ...);
> >
> >  computes  fs = factorials n =  [0!, 1!, ..., n!]
> >                                               (12! is not so large);
> >  computes  x % n,  (x div n) % n  for x <- fs;
> >  prints  x % n,  (x div n) % n    for x <- fs.
> >
> >  prints  gcd! x n   for x <- fs;      -- II
> >  prints  fs.                          -- III
> >
> >
> > For n = 12, all this is done in a moment - except II and III.
> > II  takes very long,
> > III takes very long.
> >
> > I guess this illustrates the conclusions (1) and (2).
> > Does it?
> >
> > Can you, please, look into the subject?
> > I have an impressions that these things can be fixed easily.
> >
> > Thanks,
> >
> > ------
> > Sergei
> >
> >
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> 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/20190326/ae3d9819/attachment.html>