[Agda] interactive Bin arith performance

[Sergei Meshveliani]

People,

I see a strangely slow evaluation of the Bin arithmetic in the
interactive type checking under emacs:

  test1 :  let b = stringToBin "1000001000" in  rem b 10' (λ()) ≡ 0#
  test1 =  refl

This is actually proving the equality   520 modulo 10 ≡ 0,  

where the data are represented in the binary system.

stringToBin  is evaluated fast,  and all the rest takes  28 sec.

And when it is compiled, and  "1000001000"  is input from file,
and the result (rem b 10' (λ())) is printed out, 
this input + evaluation + output  takes  
                                        0.002 sec.

This makes it  14000  times speed up.

rem  is a part of  divMod  for binary naturals.
I use my own Bin library, the representation is similar as the one that
Martin Escardo introduced.

This is going to be Binary-4.2. There I try to change the definition for
_<_ and implementation for _<-cmp_ for Bin.
This may lead to some adventures in performance, it needs investigation.

But why the same method is 14000 times faster when compiled?
Can this slow down be natural, or there is something strange in the type
checker?

This is on Development Agda of January 2, 2019.

I cannot reproduce the example in Standard Bin, because it has not
divMod.


Regards,

------
Sergei