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

[Silvio Frischknecht]

-----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-----