[Agda] evaluation in compilation

Serge D. Mechveliani mechvel at botik.ru
Mon Oct 1 19:44:19 CEST 2012

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?



More information about the Agda mailing list