[Agda] how does BUILTIN work - practical programming in Agda

[Nils Anders Danielsson]

On 2011-12-05 08:38, Ulf Norell wrote:
>
> On Sun, Dec 4, 2011 at 8:13 PM, Silvio Frischknecht <silvio.frischi at gmail.com <mailto:silvio.frischi at gmail.com>> wrote:

>     1) What does BUILTIN do if not replacing ℕ with a haskell Integer?
>
> It does replace it with Haskell integers.

This answer needs to be qualified:

* The type-checker uses Haskell Integers to compute with closed BUILTIN
   natural numbers.

* The MAlonzo compiler seems to generate code which uses Haskell
   Integers for constants. However, the plus function is still defined
   using pattern matching on unary natural numbers. For instance, 1 + 3
   is compiled into the following code:

     MAlonzo.RTE.mazCoerce
       (MAlonzo.Code.Data.Nat.d60
          (MAlonzo.RTE.mazCoerce
             (MAlonzo.Code.Data.Nat.mazIntegerToNat (1 :: Integer)))
          (MAlonzo.RTE.mazCoerce
             (MAlonzo.Code.Data.Nat.mazIntegerToNat (3 :: Integer))))

   Here d60 is defined as follows:

     d60 (C3) v0 = MAlonzo.RTE.mazCoerce v0
     d60 v0 v1
       = MAlonzo.RTE.mazCoerce
           (d_1_60 (MAlonzo.RTE.mazCoerce v0) (MAlonzo.RTE.mazCoerce v1))
       where d_1_60 (C5 v0) v1
               = MAlonzo.RTE.mazCoerce
                   (C5
                      (MAlonzo.RTE.mazCoerce
                         (d60 (MAlonzo.RTE.mazCoerce v0) (MAlonzo.RTE.mazCoerce v1))))
             d_1_60 v0 v1
               = error
                   "MAlonzo Runtime Error: incomplete pattern matching: Data.Nat._+_"

   I think MAlonzo used to do more, but I seem to recall removing some
   functionality because it seemed to be partially broken (or perhaps I
   didn't understand it).

* The Epic backend automatically detects data types structurally
   isomorphic (after forcing) to the natural numbers, and represents them
   using some kind of big-integer type. If the right BUILTIN pragmas are
   used, then some functions, like addition, are compiled into more
   efficient big-integer definitions. (I suppose that the use of pragmas
   could be replaced by automatic detection.)

* AFAIK the JavaScript backend does not contain any code for optimising
   unary natural numbers.

-- 
/NAD