[Agda] evaluation in compilation

[Serge D. Mechveliani]

On Mon, Oct 01, 2012 at 07:30:41PM +0200, Nils Anders Danielsson wrote:
[..]
>> It follows then that there is no simple way to sort in practice in Agda
>> a given list of naturals of length about 64000
>> (?)
>
> As I wrote elsewhere: You can work around this problem by reading (parts
> of) the input from a file. Furthermore I suspect that your problem is
> not related to normalisation but rather to the representation of natural
> numbers.


1. In practice, a large expression (not only a number) more often appears 
   not from a file but as  a result of a function,  a result of 
   intermediate computation.

2. A binary counter for the value of  b = 2^18  : Bin  has a small 
   representation. But the compiler still tries to evaluate at the 
compilation time the corresponding concatenation of 2^18 small lists 
built by a function in my example.
By the way, if this  b  is read from a file, will this prevent this 
long compilation effect in this example?

Regards,

------
Sergei