[Agda] original Nat

[Sergei Meshveliani]

On Wed, 2017-12-20 at 09:08 +0100, Ulf Norell wrote:
> Natural number operations _are_ implemented in Agda, and you'll find
> the definitions in
> Agda.Builtin.Nat. The way that they are built in is that when called
> on closed terms (for
> instance 101 + 52), the type checker evaluates that using Haskell
> integer arithmetic rather
> than the Agda definitions.
> 
> 
> You can read more
> here: http://agda.readthedocs.io/en/latest/language/built-ins.html#natural-numbers
> 
> 
> Agda.Builtin.Nat is shipped with Agda. You can find its location
> either by middle-clicking
> the module name in Emacs, or by calling Agda from the command line
> with `-v2`:
> 
> 
> Bla.agda:

>   import Agda.Builtin.Nat

> $ agda -v2 Bla.agda
> [..]


Thank you.

Now, I find it on my machine on

/home/mechvel/.cabal/share/x86_64-linux-ghc-7.10.2/Agda-2.5.3/lib/prim/Agda/Builtin/Nat.agda



The problem is as follows.

I have prepared a new certified arithmetic for  Bin,  including 
* _<_ and <-cmp comparison based on lexicographic ordering on bit lists,
* _∸_,  divMod,  gcd,
* proofs for all important things, like CommutativeMonoid for _+_ and
_*_, and other properties.

The aim is to avoid any built-in arithmetic, with keeping a reasonable
cost order. For example, (divMod x y) needs to cost somewhat  O(l^2) 
for  l = max (bitLength x) (bitLength y). 

But:
in some paces it uses the counter  cnt : ℕ  for termination proof
(I do not know how to arrange some termination proofs without using
toℕ).
It is initially obtained by  (Bin.toℕ b),  and works in the loops by
pattern-matching against  (1+ cnt).
 
Now, I need a performance test showing that, for example,  divMod x y
has the intended cost order. 
And it does so.
But:  
(Bin.toℕ b)  applies  Nat._+_  and  (Nat._*_ 2)  in a loop at the
running time.  

The cost order for operating with  cnt  can be small due to the two
reasons:
(1) lazy evaluation of toℕ, with stepping from  (1+ cnt)  to  cnt  
    a few  number of times,
(2) built-in performance for   Nat._+_  and  (Nat._*_ 2).

I need to make sure that the source of (2) can be removed.
For this, I, probably, need to switch out built-ins for all Nat items,
with letting them evaluate really in _unary_ system. For example, 
(Nat.+ 101 52)  to compute in 53 steps of pattern matching.

Right?

How does one arrange this?  

Needs one to edit the file
.../share/x86_64-linux-ghc-7.10.2/Agda-2.5.3/lib/prim/Agda/Builtin/Nat.agda

with removing all the lines containing the pragma of
                                           {-# BUILTIN  ...  #-}
?

Thanks,

------
Sergei


> 
> On Tue, Dec 19, 2017 at 7:43 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Please, what is a regular way to switch between the built-in
>         Nat
>         arithmetic and the original one (implemented in Agda) ?
>         
>         Data.Nat.Base  of  lib-0.14  contains
>         
>          open import Agda.Builtin.Nat public using ( zero; suc; _+_;
>         _*_ )
>                                              renaming ( Nat to ℕ; _-_
>         to _∸_ )
>         
>         But I do not find the module  Agda.Builtin.Nat.
>         
>         I need to use the Nat arithmetic programmed in Agda
>         (ℕ; _+_, _*_, _∸_, _≤_ ...) as in early days.
>         
>         Thanks,
>         
>         ------
>         Sergei
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>