Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]

[James Deikun]

On Mon, 2012-04-23 at 15:04 +0200, Ulf Norell wrote:

> The purpose is to give you fast (=running on Haskell
> integers) div and mod on nats at compile time.

This is something pretty important, too -- if NATDIVSUCAUX is going to
be removed, it really needs to be replaced with something.  The current
stdlib implementation is clever, but thanks to depending on
optimizations Agda still doesn't implement, it can take about 25 seconds
to reduce the product of two rationals (involving no more than 2-digit
arithmetic).  More generic optimizations would of course be preferable,
but there really ought to be something.

> The sanity checking for BUILTINs is supposed to
> disallow incorrect definitions, if it doesn't it's a
> bug that should be fixed. The FFI and postulates
> obviously let you "prove" whatever you want, but
> BUILTINs shouldn't.

The problem in this case is not with an incorrect definition on
the .agda side -- it's that the optimized implementation does not match
the correct definition and will return negative naturals when called on
numbers outside the range that function was designed for.  It just needs
to be fixed to match the existing definition better.