[Agda] constant evaluation

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

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

(in Agda-, 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,


More information about the Agda mailing list