[Agda] interactive Bin arith performance

[Sergei Meshveliani]

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


Suppose that the module M1 is imported in M2.agda,
and the function f is implemented in M1.
Then M2 is loaded by C-c C-l, 
and it is evaluated in the interpreter the term  M1.f   
by the command  C-c C-n. 

Does it make difference for performance whether the module M1.agda is
previously compiled or not?  
(I have an impression that it is equally slow).

Thanks,

------
Sergei



> 
> > 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
> 
> 
>