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

[Ulf Norell]

On Sun, Dec 4, 2011 at 8:13 PM, Silvio Frischknecht <
silvio.frischi at gmail.com> wrote:

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

It does replace it with Haskell integers. The problem in this case is that
the show
function isn't built in, and the implementation in the standard library is
very inefficient.

If you replace the right hand side of num by 1000, I suspect you would get
the
same behaviour.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111205/0afb10a0/attachment.html