[Agda] Size limit on generated code?

[Andreas Abel]

Hi Roly,

I am not aware of any size limit of the MAlonzo compiler.  Please submit 
an issue report with a reproducible test case (can also be a link to a 
commit on github or so) to

   https://code.google.com/p/agda/issues
.
Cheers,
Andreas

On 26.09.2014 05:01, Roly Perera wrote:
> Hi,
>
> I've been working on an Agda development for some time and would now
> like to run some test code. (Outré, I know.) So I'm compiling to a
> binary using C-c C-x C-c in Emacs.
>
> Everything is hunky dory until GHC reaches the .hs file for the test
> code itself, which appears to be truncated at line 32653. I assume
> this is some kind of limit on the size of the generated code.
>
> I build a test value which represents a pi calculus expression
> containing several variables. It looks like each occurrence of a de
> Bruijn index in the pi calculus program is expanding into a rather
> large amount of Haskell, along these sorts of lines:
>
>     (MAlonzo.Code.Data.Fin.d135
>        (MAlonzo.RTE.mazCoerce
>           (MAlonzo.Code.Data.Nat.C5
>              (MAlonzo.RTE.mazCoerce
>                 (MAlonzo.Code.Data.Nat.mazIntegerToNat
>                    (8 ::
>                       Integer)))))
>        (MAlonzo.RTE.mazCoerce
>           (MAlonzo.Code.Data.Fin.d135
>              (MAlonzo.RTE.mazCoerce
>                 (MAlonzo.Code.Data.Nat.C5
>                    (MAlonzo.RTE.mazCoerce
>                       (MAlonzo.Code.Data.Nat.mazIntegerToNat
>                          (8 ::
>                             Integer)))))
>
> The generated file is truncated in the middle of a token:
>
>          (MAlonzo.Code.Dat
>
> Is there any way around the limit, if that's indeed what I'm running
> into, or tips for avoiding this sort of problem?
>
> thanks
> Roly
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/