[Agda] interactive Bin arith performance

[Sergei Meshveliani]

On Thu, 2019-01-31 at 18:40 +0300, Sergei Meshveliani wrote:

> 
> And in my example of  test0 = remainder (divRem 520 10),  
> proofs are not evaluated in the compiled program.
> 
> Now, return to Agda interpreter.
> [..]


Consider a more clear example of test1:


-- of Binary-4.2 ---------------------------------------------------
open import Binary using (Bin; 0#; 1#; 2#; 3#; 4#; 5#; _+_; 
                                               DivMod; divMod; rem)
10' : Bin
10' = 5# + 5#

-- test0 = let b = stringToBin "1000001000" in rem b 10' (λ())

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 ?

Then,
      C-c C-n  (test1 "1000001000")

takes 20 seconds, which is 10.000 times longer than for the compiled
program.
So that, probably, proofs were evaluated here.

Why it is so?
Am I missing something?

Thanks,

------
Sergei