[Agda] gcd, toDecimal performance

[Sergei Meshveliani]

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





-------------- next part --------------
open import Foreign.Haskell
open import IO.Primitive
open import Codata.Musical.Costring using (toCostring)

open import Function                   using (_∘_; case_of_)
open import Algebra.FunctionProperties using (Op₂)
open import Relation.Nullary           using (yes; no)
open import Relation.Unary             using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Product using (_×_; _,_; _,′_; proj₁; proj₂)
open import Data.List using (List; []; _∷_; [_]; reverse; map; foldr; filter)
open import Data.Char as Char  using (Char)
open import Data.String as Str using (String) renaming (_++_ to _++s_)
open import Data.Nat           using (ℕ; suc; _+_; _∸_; _*_; _≤_; _≤?_) 
open import Data.Nat.Show      using (show)
open import Data.Nat.GCD       using (gcd)
open import Data.Nat.DivMod    using (_div_; _%_) 


-- Begin-Prelude -------------------------------------------------------------

concatStr : List String → String
concatStr = foldr Str._++_ ""

filterStr :  ∀ {p} {P : Char → Set p} → Decidable P → String → String 
filterStr P? =  Str.fromList ∘ filter P? ∘ Str.toList 

-- stringToNat; decimalDigit?

showNats :  List ℕ → String
showNats =  concatStr ∘ map (\n → "," ++s (show n))

isDecimapDigit : Char → Set
isDecimapDigit c =  48 ≤ n × n ≤ 57  where 
                                     n = Char.toNat c

decimalDigit? : Decidable isDecimapDigit
decimalDigit? c =
                let n = Char.toNat c
                in
                case ((48 ≤? n) ,′ (n ≤? 57)) of \ 
                                  { (yes le ,  yes le') → yes (le , le')
                                  ; (yes _ ,   no n≰57) → no (n≰57 ∘ proj₂)
                                  ; (no 48≰n , _      ) → no (48≰n ∘ proj₁) 
                                  } 

charToDecDigitNat : Char → ℕ
charToDecDigitNat c = (Char.toNat c) ∸ 48

readNat : List Char → ℕ                   -- convert from decimal digit chars
readNat =  toN ∘ map charToDecDigitNat ∘ reverse 
           where
           toN : List ℕ → ℕ
           toN []        = 0
           toN (j ∷ js) = j + (10 * (toN js))

stringToNat : String → ℕ
stringToNat = readNat ∘ Str.toList

-- End-Prelude ----------------------------------------------------------------



factorials : ℕ → List ℕ           -- [factorial i | i <- [n .. 0]]
factorials 0       = [ 1 ]
factorials (suc n) = case factorials n of \
                                 { (p ∷ fs) → ((suc n) * p) ∷ p ∷ fs
                                 ; []        → []   -- unaccessible
                                 }
-- test : factorials 4 ≡ 24 ∷ 6 ∷ 2 ∷ 1 ∷ 1 ∷ []
-- test = refl

gcd! : Op₂ ℕ
gcd! n = proj₁ ∘ gcd n

gcds : ℕ → List ℕ
gcds n =
       map (gcd! n) (factorials n)



test : ℕ → String   
test n =
  concatStr
  ("n = "                    ∷ show n
   ∷ "\nrems =\n "          ∷ showNats rems
   ∷ "\nqRems =\n "         ∷ showNats qRems
   -- ∷ "\nfactorials n =\n "  ∷ showNats fs
   -- ∷ "\ngcds n =\n "     ∷ showNats gs
   ∷ []
  )
  where
  fs    = factorials n
  rems  = map (\x → x % (suc n))   fs
  quots = map (\x → x div (suc n)) fs
  qRems = map (\x → x % (suc n))   quots
  gs    = gcds n
  
main = (readFiniteFile "data.txt") >>= putStrLn ∘ toCostring ∘ g
       where
       g : String -> String
       g str = test n
               where
               n = stringToNat (filterStr decimalDigit? str)

-- Put to  data.txt  n =
--                     9, 10, 11, 12, ...
--
-- and run  > time ./NatGCDTest