[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