[Agda] gcd, toDecimal performance

[Sergei Meshveliani]

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