[Agda] interactive Bin arith performance

[Sergei Meshveliani]

On Wed, 2019-01-30 at 15:55 +0300, Sergei Meshveliani wrote:
> 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.


Now I set a more precise test:

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

and evaluate  test0  in interpreter by  C-c C n.
This takes 20 sec.
So that the performance ratio is  10.000.

The matter is in equational provers.  There are possible provers basing
on certain computations with polynomials over rational numbers, and
such. And such a computation happens during the type check. With this
10.000 slow down, such a prover is greatly restricted in its
application.  

--
SM


> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda