[Agda] timing for agda-prelude gcd

[Sergei Meshveliani]

Dear all,

Earlier there was discussed in this list the performance of _+_ and _*_
on Nat. I provided a test program.
And as I recall, the performance is high: as in the Haskell program for
ghc-7.10.2. 

Now I need fast  divMod and gcd  for Nat.
Standard library is very-very slow at this point.

So I try  agda-prelude.
It shows considerably faster.
But it is still slower than  GHC.
gcd  is about  12 times  slower, 
and  divMod  is about 4000 times slower (?).

I wonder: what makes this difference with the performance of _+_ and
_*_ ?
(mainly for divMod).

On practice, I need to find  d = gcd m n  and then to  divide m and n by
d. And both need to be fast.  
gcd looks reasonable (if I do not mistake),
but division is via  dimMod,  it its slows down everything.


The code  (for  Agda-2.5.2 -like  and for  Haskell)  is attached in
GCDTest.agda
It is small.

`main' of Agda     reads  n  from file.
`main' of Haskell  sets   n  in the program (I hope it would not compute
much at compile-time -- ?).
As the loops are long, I hope this does not make a real difference in
time.

The Haskell code is `made' by  
                           ghc -O --make

The Agda code includes auxiliary functions that read  n  and convert to
Nat  (may be, Standard needs to provide such functions?). 

After the Agda code, there follows the timing table,
then it follows the Haskell code.

There is produced a long list  rs  of results for divMod (for gcd),
and it is printed  (maximum rs).
`maximum' is applied in order to avoid printing large values.

Can people, please, try this code and tell, may be I am missing
something? 
The thing needs consideration and verification.

Thanks,

------
Sergei
-------------- next part --------------
module GCDTest where

open import Foreign.Haskell
open import IO.Primitive
open import Data.String as Str using (String; toCostring; _++_)

open import Function                   using (_$_; _∘_; flip; case_of_)
open import Relation.Nullary           using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Unary             using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≢_) 
open import Data.Product      using (_×_; _,_; _,′_; proj₁; proj₂) 
open import Data.Char as Char using (Char)
open import Data.List using (List; []; _∷_; map; foldr; reverse; filter)
import Data.Fin as Fin
open import Data.Nat      using (ℕ; suc; pred; _+_; _*_; _∸_; _≤_; _≤?_)
open import Data.Nat.Show using () renaming (show to showNat) 

-- of UNPrelude --
open import Prelude.String 
open import Prelude.Nat    
open import Numeric.Nat.DivMod using (rem) renaming (divMod to uDivMod)
open import Numeric.Nat.GCD    using (gcd!)



--****************************************************************************
concatStr : List String → String
concatStr = foldr _++_ ""

filterStr :  {P : Char → Set} → Decidable P → String → String
filterStr P? =  Str.fromList ∘ filter (⌊_⌋ ∘ P?) ∘ Str.toList

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

decimalDigit? : Decidable isDecimalDigit
decimalDigit? c =
                let n = Char.toNat c
                in
                case ((48 ≤? n) ,′ (n ≤? 57)) of \
                                   { (yes le ,  yes le') → yes (le , le')
                                   ; (no 48≰n , _      ) → no (48≰n ∘ proj₁)
                                   ; (_ ,       no n≰57) → no (n≰57 ∘ 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

max : ℕ → List ℕ → ℕ 
max x []       =  x
max x (y ∷ xs) =  case x ≤? y of \ { (yes _) → max y xs 
                                   ; (no _)  → max x xs }

natSegment :  ℕ → ℕ → List ℕ
natSegment m n =                    -- [k | m ≤ k ≤ n]   
               segm m (n ∸ m)
               where
               segm : ℕ → ℕ → List ℕ
               segm m 0         =  m ∷ []
               segm m (suc cnt) =  m ∷ (segm (suc m) cnt)

------------------------------------------------------------------
remBySuc : ℕ → ℕ → ℕ 
remBySuc m n =  rem (uDivMod (suc n) m)

testRem : ℕ → ℕ 
testRem n =  max 0 (map (remBySuc n) (natSegment 0 (n ∸ 2)))
             
testGCD : ℕ → ℕ 
testGCD n =  max 0 (map (gcd! n) (natSegment 1 (pred n)))

main : IO Unit
main = (readFiniteFile "data.txt") >>= putStrLn ∘ toCostring ∘ g
  where
  -- n  is first read from file  data.txt
  g : String -> String
  g str = 
    concatStr 
    ("n = "               ∷  showNat n             ∷ ",   " ∷
     "testRem = "         ∷  showNat (testRem n)      -- chhose 
     -- "testGCD n = "       ∷  showNat (testGCD n)   -- here
     ∷ []               
    )
    where
    n = stringToNat $ filterStr decimalDigit? str




{- ------------------------------------------   
Timing   for  Agda 2.5.2,  3 GHz machine.  

 n       |   Time [sec]                    
         |
------- testRem -----------------------------
         |                       |
         | Agda 2.5.2            | ghc-7.10.2
---------------------------------------------
 20000   |   3  (value =  9999)  |  0.000
 30000   |   9  (value = 14999)  |  0.004
 40000   |  17  (value = 19999)  |  0.004
         |                       |
500000   |                       |  0.3


------- testGCD ---------------------
         |
         |  Agda 2.5.2 | ghc-7.10.2
-------------------------------------    
  500000 |   0.8       |   
 1000000 |   1.7       |   
 5000000 |  10.7       |   0.8

20000000 |             |   3.1
-}



-- Haskell code ******************************************************

max' :: Integer -> [Integer] -> Integer   -- maximum (x: xs)
max' x []      =  x
max' x (y: xs) =  if x < y then  max' y xs
                  else           max' x xs

modTest :: Integer -> Integer
modTest n =
          max' 0 (map (\ k -> mod n (succ k))
                                    ([0 .. (n - 2)] :: [Integer])
                 )

gcdTest :: Integer -> Integer
gcdTest n =
          max' 0 (map (gcd n) [1 .. (pred n)])

n = 20000000  :: Integer      -- edit this 

main :: IO ()
main = putStrLn (show (modTest n))
                      -- gcdTest    edit this