[Agda] Raw natural numbers

[Ulf Norell]

On Thu, Oct 21, 2010 at 12:22 AM, Alan Jeffrey <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101021/ad2f77ae/attachment.html