[Agda] Raw natural numbers

[Ulf Norell]

On Fri, Oct 29, 2010 at 10:36 PM, Alan Jeffrey <ajeffrey at bell-labs.com>wrote:

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

These coercions are now generated together with conversion functions.

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.


I've put mazCoerce in its own module MAlonzo.RTE (the other generated
modules end up in MAlonzo.Code.*). That way you should be able to write
coercion-aware libraries as long as you compile them together with the Agda
program. Hopefully that'll work for now, but eventually I guess we should
put it in a cabal package that is installed together with Agda.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101109/87f78111/attachment.html