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