[Agda] constant evaluation

Serge D. Mechveliani mechvel at botik.ru
Sun Sep 23 18:31:36 CEST 2012


Please, 
how to prevent evaluation of a given constant at the compile time?

(in Agda-2.3.0.1, MAlonzo, lib-0.6).

My  `main'  
  defines   ys = f n xs  which 
            concatenates  n : Bin  times the list  xs : List Nat,
  puts  n = 2^12,  xs = 1 :: 2 :: 3 :: nil   in  ys = f n xs,
  finds  zs = merge ys ys
  prints the first and last elements in  zs.

The compiler hungs for a long time. I think, it is because it starts to 
evaluate the constant  ys  (and may be also  zs)  at the compile time.
For a small  n,  it finishes fast enough.

On the other hand, for a certain counting in Bin from 0 to 2^12,
it does not evaluate the constant at the compile time, even though
forming this constant is simpler than forming the above list  ys.

Thank you in advance for explanation,

------
Sergei


More information about the Agda mailing list