[Agda] interactive Bin arith performance

[Sergei Meshveliani]

On Thu, 2019-01-31 at 18:14 +0100, Ulf Norell wrote:

> [..]

>         test1 : String → Bin
>         test1 str =
>                   let b = stringToBin str in  rem b 10' (λ())
>         -------------------------------------------------------------
>         
>         
>         First,  C-c C-l  is applied.
>         rem  is here  remainder (divRem b 10' _).
>         
>         test1  is type-checked, together with all functions needed for
>         divRem.
>         
>         Is it known after this that no proofs need to be evaluated for
>         evaluation of  test1 ?
> 
> 
> No, why would you think that? Also it's not clear what you mean by
> "evaluation of test1".
> Do you mean using the compile-time evaluator, running the compiled
> code, or some hypothetical ideal evaluator.
> 

Sorry, I need to understand this feature.
Earlier I ignored it, because I considered the performance of the
compiled code.
    
Can anybody, please, explain what is happening in the below simple and
self-contained example? 

-----------------------------------------------------------------
f : (m : ℕ) → ∃ (\n → n ≤ m)

f 0       =  (0 , ≤-refl)
f (suc m) =  let (n , n≤m) = f m
             in
             case suc n ≤? m of \
                             { (yes _) → (n , ≤-step n≤m)
                             ; (no _ ) → (suc n , s≤s n≤m) }

g = proj₁ ∘ f
-----------------------------------------------------------------

emacs,   C-c C-l 
             g 22

is evaluated in  25 sec.

   C-c C-l  g 25

takes very long, I have interrupted it.

Is it due to the proof part evaluation?

If the module (Foo.agda) is complied, and  m  is read from the file
data.txt, then
               ./Foo 

evaluates about 10.000 times faster than the interpreted g.

Still the evaluation cost of the compiled code looks as quadratic.
I think, this is because  k ≤? l  is solved  m  times for  k  having  k
`suc' constructors for  k = 0, ..., m. 

Does the compiled  g  evaluate proofs?
If not, then who has removed the  proof evaluation part (PEP)
from the code?

Type checking produces  Foo.agdai  which has PEP,
MAlonzo takes Foo.agdai, compiles to Haskell with removing the PEP, 
and  Foo.hs  does not have PEP
-- is this so?

I attach the module that also includes the `main' function.
The code for  g  is small, and all the rest is for parsing of a String
to Nat
(is such parsing somewhere in standard library?).

Thanks,

------
Sergei

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

open import Function         using (_∘_; case_of_)
open import Relation.Nullary using (yes; no)
open import Relation.Unary   using (Decidable)
open import Relation.Binary.PropositionalEquality using
                                              (_≡_; sym; subst)
open import Data.Product using (_×_; _,_; _,′_; proj₁; proj₂; ∃)
open import Data.Nat     using (ℕ; suc; _+_; _∸_; _*_; _≤_; z≤n;
                                                  s≤s; _≤?_)  
open import Data.Nat.Properties using
     (≤-refl; ≤-step; +-mono-≤; *-distribˡ-+; module ≤-Reasoning)
open ≤-Reasoning
open import Data.List using (List; []; _∷_; reverse; map; filter)
open import Data.Char as Char using (Char)
import Data.Nat.Show as NatShow



-------------------------------------------------------------------
-- This is for reading from String to ℕ.
-- Has standard something for this?

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')
                                   ; (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

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

-------------------------------------------------------------------
f : (m : ℕ) → ∃ (\n → n ≤ m)
 
f 0       =  (0 , ≤-refl) 
f (suc m) =  let (n , n≤m) = f m
             in
             case suc n ≤? m of \
                             { (yes _) → (n , ≤-step n≤m)
                             ; (no _ ) → (suc n , s≤s n≤m) }

g = proj₁ ∘ f

-- g 22   |  25 sec.

 
main = (readFiniteFile "data.txt") >>= putStrLn ∘ toCostring ∘ h
       where
       h : String → String
       h = NatShow.show ∘ g ∘ stringToNat ∘ filterStr decimalDigit?