[Agda] practical integer/rational arithmetic?

[Noam Zeilberger]

Does anyone have experience writing Agda code involving some
non-trivial computation on the integers/rationals?  I'm writing some
code where the goal is not formalization of arithmetic per se, but
where I would like to be able to actually run some computations which
might require, e.g., addition-multiplication-division of six-digit
numbers.  I think I would be happy if there were a way to defer all
these calculations to Haskell's builtin exact rational arithmetic and
then reason axiomatically...which seems to be what the foreign
function interface would provide, except that if I understand
correctly (http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.FFI) it
only works with the Alonzo/MAlonzo backends, and not in interactive
mode.  Ideally, I would like to be able to run arithmetic computations
interactively, see their results, *and* have Agda verify that the
results have a particular normal form.

For now I'm using the standard library implementations of Data.Nat and
Data.Integer with a slightly modified Data.Rational (which does not
keep rationals in reduced form, to make it easier to do computations),
but this seems to be unworkably slow even on small examples.  For
example, computing the gcd (Data.Nat.Gcd) of 2012 and 1984 takes about
three and a half minutes on my laptop.

Noam