[Agda] Raw natural numbers

[Alan Jeffrey]

Yay, victory!  Or very close to it...  (# 2 + # 2) now generates:

MAlonzo.System.IO.Examples.Four.d42 = GHC.Integer.Type.S# 2
MAlonzo.System.IO.Examples.Four.d41 =
   GHC.Integer.plusInteger
     MAlonzo.System.IO.Examples.Four.d42
     MAlonzo.System.IO.Examples.Four.d42

No intermediate conversions, hooray!  The only gotcha is we need a place 
for the following RULES to live... any chance you could generate them 
along with the converter functions?

{-# RULES "i-n-i" forall x . mazNatToInteger (mazIntegerToNat x) = x #-}
{-# RULES "n-i-n" forall x . mazIntegerToNat (mazNatToInteger x) = x #-}

The other issue is that at the moment, every module is getting its own 
mazCoerce function, which means that there's no way to write 
coercion-aware FFI libraries (e.g. for stream fusion).  Fixing this 
would involve generating a tiny run time system, which the compiler is 
currently avoiding.

A.

On 10/29/2010 02:52 AM, Ulf Norell wrote:
>
> On Thu, Oct 21, 2010 at 8:44 PM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto:ajeffrey at bell-labs.com>> wrote:
>
>     I'm building the new compiler now...  Fingers crossed!
>
>     A more general solution to the problem of unsafeCoerce getting in
>     the way would be for Agda to use its own coerce function, defined
>     something like:
>
>       {-# INLINE [1] coerce #-}
>       coerce = Unsafe.Coerce.unsafeCoerce
>
>       {-# RULES "coerce-id" forall (x :: a) . coerce x = x #-}
>
>     This would at least remove all the identity coercions, and would
>     allow other FFI bindings to define their own RULES.
>
>
> I've pushed a patch that does this. Let me know how it works out.
>
> / Ulf