[Agda] Raw natural numbers

[Alan Jeffrey]

Sigh, digging up this old chestnut...

Slightly annoyingly I now have an implementation of raw naturals. 
Horrid hackery is here:

   http://github.com/agda/agda-system-io/blob/master/src/Data/Natural

In particular Data.Natural.Primitive declares:

   private
     postulate
       # : ∀ {A} → A → Natural
   {-# COMPILED # (\ _ -> Data.Natural.AgdaFFI.convert
         MAlonzo.Data.Nat.mazNatToInteger) #-}

Yuk yuk yuk, but it does the job.  Or at least it does under Agda 2.2.6. 
  In the snapshot 2.2.9, the generated library names have changed so the 
above should be:

   {-# COMPILED # (\ _ -> Data.Natural.AgdaFFI.convert
         MAlonzo.Code.Data.Nat.mazNatToInteger) #-}

I'd like to maintain one version of the code which compiles with 2.2.6 
and above, at least while the Debian packages are still at 2.2.6 or 2.2.8.

Thoughts?

A.

On 11/10/2010 10:00 AM, Jeffrey, Alan S A (Alan) wrote:
> 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
>>
>