[Agda] Raw natural numbers

[Alan Jeffrey]

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.

A.

On 10/21/2010 04:48 AM, Ulf Norell wrote:
>
> On Thu, Oct 21, 2010 at 12:22 AM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto:ajeffrey at bell-labs.com>> wrote:
>
>     Hi everyone,
>
>     I did some simple bindings for raw natural numbers:
>
>     http://github.com/agda/agda-system-io/tree/master/src/Data/Natural
>
>     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.
>
>     The idea would be to add a rule to Haskell's rewrite engine:
>
>     {-# RULES "int2nat2int" forall x .
>       MAlonzo.Data.Nat.mazNatToInteger (MAlonzo.Data.Nat.mazIntegerToNat x)
>         = x #-}
>
>     This almost works.  The two things stopping it are:
>
>     a) There isn't an FFI binding for Nat (grr) which means the compiler
>     inserts some unsafeCoerce operations which then stop rewrites from
>     firing.
>
>     b) The definitions of mazNatToInteger and mazIntegerToNat define a
>     local variable, which isn't in scope for rewriting.
>
>
> I removed the unnecessary coercion of integer literals, so now you get
>
>    Unsafe.Coerce.unsafeCoerce (mazIntegerToNat ((10) :: Integer))
>
> instead of
>
>    Unsafe.Coerce.unsafeCoerce (mazIntegerToNat
> (Unsafe.Coerce.unsafeCoerce ((10) :: Integer)))
>
> when using natural number literals. I also changed the implementation of
> mazNatToInteger/IntegerToNat to
>
> mazNatToInteger
>    = \ x -> case x of { C2 -> 0 :: Integer; C3 x -> 1 + (mazNatToInteger
> (Unsafe.Coerce.unsafeCoerce x)) }
> mazIntegerToNat
>    = \ x -> if x <= (0 :: Integer) then C2 else C3
> (Unsafe.Coerce.unsafeCoerce (mazIntegerToNat (x - 1)))
>
> (where C2 and C3 are the constructor names for zero and suc). Hopefully
> this will help a little.
>
> / Ulf