[Agda] Using machine integers / Data.Int from Haskell in Agda

[Ulf Norell]

As long as you don't need the machine integers to compute at compile time,
you can set up the bindings with the foreign function interface:

postulate
  Int : Set
  intPlus : Int -> Int -> Int

-- Agda 2.5.2
{-# COMPILED_TYPE Int Int #-}
{-# COMPILED intPlus (+) #-}

-- Agda > 2.5.2
{-# COMPILE GHC Int = type Int #-}
{-# COMPILE GHC intPlus = (+) #-}

If you need compile time computations you will either have to do a modest
amount of hacking on the Agda implementation (mainly in
Agda.TypeChecking.Monad.Builtin and Agda.TypeChecking.Rules.Builtin), or
make do with the builtin natural numbers which map to Haskell bignums
(Integer rather than Int).

/ Ulf

On Thu, Mar 2, 2017 at 7:38 PM, stvienna wiener <stvienna at gmail.com> wrote:

> Hi,
>
> I am programming a benchmark in Agda and would like to use machine
> integers. I would need bindings similar to Agda.Builtin.Float.
>
> I know there was some Agda library in the past regarding Naturals on
> github.com (perhaps from Alan Jeffrey?).
>
> Did anyone use machine integers in Agda and has code? Or at least the link
> to the old code on github.
>
> Thanks & cheers,
> Stephan
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170303/e42131a3/attachment.html>