[Agda] Raw natural numbers

[Alan Jeffrey]

Thanks!

On 11/09/2010 07:41 AM, Ulf Norell wrote:
>
> On Fri, Oct 29, 2010 at 10:36 PM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto: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
>