[Agda] how does BUILTIN work - practical programming in Agda

[Andreas Abel]

Maybe my last mail was not addressing your issue.

You want portable efficient arithmetic.

It seems that currently each compiler has its own COMPILED pragmas.  So 
maybe you just have to add a pragma for each compiler you want to support.

For instance, I find in the release notes of 2.3.0 the Syntax for 
JavaScript COMPILED pragmas:

     {-# COMPILED_JS _+_ function (x) { return function (y) {
                           return x+y; };
       } #-}

If I am not mistaken, without the _JS is the COMPILED pragma for Haskell.

Have you tried this?

Of course, on the long run, we may agree on a minimum set of primitives 
each compiler has to implement, that covers at least arithmetic.

Cheers,
Andreas

On 04.12.11 8:13 PM, Silvio Frischknecht wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Hello
>
> I've been trying to do a few standard examples I usually do when
> learning a programming language, such as calculating fibonacci numbers.
> However the type ℕ is really slow. So I used imported haskell types.
> However this is very cumbersome solution and it's not portable if you
> want to use Javascript backend.
>
> I see there is a {-# BUILTIN #-} pragma and I also found that in this file
>
> src/full/Agda/Compiler/MAlonzo/Primitives.hs
>
> in the MAlonzo backend integer functions like NATPLUS or NATTIMES are
> defined as you would expect that in haskell (+) (*) but somehow when I
> import Data.Nat from the standard library, which uses these BUILTINs
> it is still very slow, even for something like this.
>
> num = 1000 * 1000 * 1000 ∸ 1000 * 1000 * 999
>
> main = putStrLn $ toCostring $ show num
>
> 1) What does BUILTIN do if not replacing ℕ with a haskell Integer?
>
> 2) While using haskell types to compute fibonacci numbers I also
> stumbled over the lake of a seq function. Is there a portable way to
> force eager evaluation? Because I got a stack overflow when using big
> numbers. Which i fixed by also importing seq from haskell, which is
> again not portable.
>
> Also I'm not sure I used the standard library correctly
> I just checked out darcs and then
>
> 1  cabal install --user
> 2  generateEverything
> 3  cd ffi&&  cabal install --user
>
> (interestingly the 3. line is not mentioned on the wiki)
> I'm also not sure what the 2. line does. I know it generates
> darcsdir/Everything.agda but nothing else.
>
> 3) when compiling agda is it correct to specify -i darcsdir/src?
> Because that would mean that Everything.agda is outside.
>
> Silvio Frischknecht
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.11 (GNU/Linux)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
>
> iQIcBAEBAgAGBQJO28ZrAAoJEDLsP+zrbatWWQwQALXCXLykbNzedvx1zYYT+lDZ
> Yc9dXm3eZDqWJEVkIfBNTAuIe1OdlkLT9q5T+9owUudHcaXIv9dLzYJZSszKFtjk
> 8TmkZ8tnyCoKUrvUOWa63iq/pdVNPUITXipi8A22SNFw2dVwOsspoBNw3Q/gvBLe
> kMCoF8Y4t2KUnZ49luRzEypn6fc+FzVhWX5d8PuJNU7xUvLaJWUS16Ac6s1cQxpK
> BLzSwADcii7gwEGcTJu6psQTNbtXT1hZDx+Q1XEdADADdWVNAuXmutGhZnITJCQh
> lT24GBMNyRTUI6yfIxrMZLWEJkoLimSxvWst9CV7WI1pXssNKuptJGiIOixfjM43
> 69fL+kKlVwLZ1bTWKk5/O1J805bZK3lBmYYJIGwSh6y/CDgqMCo0ayHgCv8EjOj3
> c4cGve4bvL2RHmpOvxMkZX06g63MImDYwikDhrfKDGWlSW+/KOL1IQW58//3HXGt
> kmEPaHxHl2sECl0blm4MZYCIXq+SJem3Z/uQ7iylVooYnJwK4vaBHfKrpUeepm02
> mg0px2O4zueGFAA+iXt/mEB1kgA3YuQPD6Om9lxs+gJToZ13hhPMRIoBtHTmx0lp
> A/0AGrY1Qz9+oXoc5Ct7s9neTNAeC/Nlx+/aNLctG+jFf8KwlZ9Dq0DoxnOSuo8D
> bRJPml6k+aEKv86nQzMg
> =HfKT
> -----END PGP SIGNATURE-----
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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