[Agda] evaluation in compilation

[Serge D. Mechveliani]

On Mon, Oct 01, 2012 at 07:12:53PM +0200, Nils Anders Danielsson wrote:
> On 2012-10-01 18:51, Serge D. Mechveliani wrote:
>> *** How to prevent this evaluation in compilation time? ***
>
> One option is to avoid hard-coded constants, and read data from a file.
>
>> n = 16000  -- 32000
>
> I think this number will be represented using 16001 constructors (plus
> lots of uses of unsafeCoerce). The Epic backend automatically detects
> that certain types can be represented using "big integers". We should
> generalise this functionality and make it available to more backends.
>
> This could be a good code sprint for someone at the Agda meeting that
> starts on Wednesday.


May be it is good to do this.
But consider the following. 

1. 16000 `suc' applications is all right -- if they appear at run time.

2. The "big integers" approach will not help in general.
   I tried the variant of 
               concatCopies : {A : Set} -> Bin└∙ -> List A -> List A 

with a  binary counter  instead of  Nat,  with applying  Bin.suc  and
\?=  for in counting from zero to  n.
In this case there are not any big integers;
and the counter has quite a few constructor applications in it.
And still the counter value 
                           fromBits (0b :: ... 0b :: 1b :: []) 
of  2^18 : Bin
leads to more than 30 minute compilation.
Probably this is because the compiler tries to evaluate these great 
number of concatenations.

Do I need to provide the code, or you can explain the effect as it is?

Thanks,

------
Sergei