<br><div class="gmail_quote">On Sun, Dec 4, 2011 at 8:13 PM, Silvio Frischknecht <span dir="ltr"><<a href="mailto:silvio.frischi@gmail.com">silvio.frischi@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br>
I see there is a {-# BUILTIN #-} pragma and I also found that in this file<br>
<br>
src/full/Agda/Compiler/MAlonzo/Primitives.hs<br>
<br>
in the MAlonzo backend integer functions like NATPLUS or NATTIMES are<br>
defined as you would expect that in haskell (+) (*) but somehow when I<br>
import Data.Nat from the standard library, which uses these BUILTINs<br>
it is still very slow, even for something like this.<br>
<br>
num = 1000 * 1000 * 1000 ∸ 1000 * 1000 * 999<br>
<br>
main = putStrLn $ toCostring $ show num<br>
<br>
1) What does BUILTIN do if not replacing ℕ with a haskell Integer?<br></blockquote><div><br></div><div>It does replace it with Haskell integers. The problem in this case is that the show</div><div>function isn't built in, and the implementation in the standard library is very inefficient.</div>
<div><br></div><div>If you replace the right hand side of num by 1000, I suspect you would get the</div><div>same behaviour.</div><div><br></div><div>/ Ulf</div><div><br></div></div>