<br><div class="gmail_quote">On Thu, Oct 21, 2010 at 12:22 AM, Alan Jeffrey <span dir="ltr"><<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi everyone,<br>
<br>
I did some simple bindings for raw natural numbers:<br>
<br>
<a href="http://github.com/agda/agda-system-io/tree/master/src/Data/Natural" target="_blank">http://github.com/agda/agda-system-io/tree/master/src/Data/Natural</a><br>
<br>
The interesting thing is that we can almost optimize away many of the uses of unary numbers -- in particular to get constants such as #1000000 to be represented in native form rather than unary.<br>
<br>
The idea would be to add a rule to Haskell's rewrite engine:<br>
<br>
{-# RULES "int2nat2int" forall x .<br>
MAlonzo.Data.Nat.mazNatToInteger (MAlonzo.Data.Nat.mazIntegerToNat x)<br>
= x #-}<br>
<br>
This almost works. The two things stopping it are:<br>
<br>
a) There isn't an FFI binding for Nat (grr) which means the compiler inserts some unsafeCoerce operations which then stop rewrites from firing.<br>
<br>
b) The definitions of mazNatToInteger and mazIntegerToNat define a local variable, which isn't in scope for rewriting.<br></blockquote><div><br></div><div>I removed the unnecessary coercion of integer literals, so now you get</div>
<div><br></div><div> Unsafe.Coerce.unsafeCoerce (mazIntegerToNat ((10) :: Integer))</div><div><br></div><div>instead of </div><div><br></div><div> Unsafe.Coerce.unsafeCoerce (mazIntegerToNat (Unsafe.Coerce.unsafeCoerce ((10) :: Integer)))</div>
<div><br></div><div>when using natural number literals. I also changed the implementation of mazNatToInteger/IntegerToNat to</div><div><br></div><div>mazNatToInteger</div><div> = \ x -> case x of { C2 -> 0 :: Integer; C3 x -> 1 + (mazNatToInteger (Unsafe.Coerce.unsafeCoerce x)) }</div>
<div>mazIntegerToNat</div><div> = \ x -> if x <= (0 :: Integer) then C2 else C3 (Unsafe.Coerce.unsafeCoerce (mazIntegerToNat (x - 1)))</div><div><br></div><div>(where C2 and C3 are the constructor names for zero and suc). Hopefully this will help a little.</div>
<div><br></div><div>/ Ulf</div></div>