<div dir="ltr"><div>Removing the BUILTIN pragmas would do it, but I would suggest</div><div>using a different, but isomorphic, type for your termination measures.</div><div>That way you don't have to mess with the builtin libraries.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Dec 20, 2017 at 12:04 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Wed, 2017-12-20 at 09:08 +0100, Ulf Norell wrote:<br>
> Natural number operations _are_ implemented in Agda, and you'll find<br>
> the definitions in<br>
> Agda.Builtin.Nat. The way that they are built in is that when called<br>
> on closed terms (for<br>
> instance 101 + 52), the type checker evaluates that using Haskell<br>
> integer arithmetic rather<br>
> than the Agda definitions.<br>
><br>
><br>
> You can read more<br>
> here: <a href="http://agda.readthedocs.io/en/latest/language/built-ins.html#natural-numbers" rel="noreferrer" target="_blank">http://agda.readthedocs.io/en/<wbr>latest/language/built-ins.<wbr>html#natural-numbers</a><br>
><br>
><br>
> Agda.Builtin.Nat is shipped with Agda. You can find its location<br>
> either by middle-clicking<br>
> the module name in Emacs, or by calling Agda from the command line<br>
> with `-v2`:<br>
><br>
><br>
> Bla.agda:<br>
<br>
>   import Agda.Builtin.Nat<br>
<br>
> $ agda -v2 Bla.agda<br>
</span>> [..]<br>
<br>
<br>
Thank you.<br>
<br>
Now, I find it on my machine on<br>
<br>
/home/mechvel/.cabal/share/<wbr>x86_64-linux-ghc-7.10.2/Agda-<wbr>2.5.3/lib/prim/Agda/Builtin/<wbr>Nat.agda<br>
<br>
<br>
<br>
The problem is as follows.<br>
<br>
I have prepared a new certified arithmetic for  Bin,  including<br>
* _<_ and <-cmp comparison based on lexicographic ordering on bit lists,<br>
* _∸_,  divMod,  gcd,<br>
* proofs for all important things, like CommutativeMonoid for _+_ and<br>
_*_, and other properties.<br>
<br>
The aim is to avoid any built-in arithmetic, with keeping a reasonable<br>
cost order. For example, (divMod x y) needs to cost somewhat  O(l^2)<br>
for  l = max (bitLength x) (bitLength y).<br>
<br>
But:<br>
in some paces it uses the counter  cnt : ℕ  for termination proof<br>
(I do not know how to arrange some termination proofs without using<br>
toℕ).<br>
It is initially obtained by  (Bin.toℕ b),  and works in the loops by<br>
pattern-matching against  (1+ cnt).<br>
<br>
Now, I need a performance test showing that, for example,  divMod x y<br>
has the intended cost order.<br>
And it does so.<br>
But:<br>
(Bin.toℕ b)  applies  Nat._+_  and  (Nat._*_ 2)  in a loop at the<br>
running time.<br>
<br>
The cost order for operating with  cnt  can be small due to the two<br>
reasons:<br>
(1) lazy evaluation of toℕ, with stepping from  (1+ cnt)  to  cnt<br>
    a few  number of times,<br>
(2) built-in performance for   Nat._+_  and  (Nat._*_ 2).<br>
<br>
I need to make sure that the source of (2) can be removed.<br>
For this, I, probably, need to switch out built-ins for all Nat items,<br>
with letting them evaluate really in _unary_ system. For example,<br>
(Nat.+ 101 52)  to compute in 53 steps of pattern matching.<br>
<br>
Right?<br>
<br>
How does one arrange this?<br>
<br>
Needs one to edit the file<br>
.../share/x86_64-linux-ghc-7.<wbr>10.2/Agda-2.5.3/lib/prim/Agda/<wbr>Builtin/Nat.agda<br>
<br>
with removing all the lines containing the pragma of<br>
                                           {-# BUILTIN  ...  #-}<br>
?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
><br>
> On Tue, Dec 19, 2017 at 7:43 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
>         Please, what is a regular way to switch between the built-in<br>
>         Nat<br>
>         arithmetic and the original one (implemented in Agda) ?<br>
><br>
>         Data.Nat.Base  of  lib-0.14  contains<br>
><br>
>          open import Agda.Builtin.Nat public using ( zero; suc; _+_;<br>
>         _*_ )<br>
>                                              renaming ( Nat to ℕ; _-_<br>
>         to _∸_ )<br>
><br>
>         But I do not find the module  Agda.Builtin.Nat.<br>
><br>
>         I need to use the Nat arithmetic programmed in Agda<br>
>         (ℕ; _+_, _*_, _∸_, _≤_ ...) as in early days.<br>
><br>
>         Thanks,<br>
><br>
>         ------<br>
>         Sergei<br>
><br>
>         ______________________________<wbr>_________________<br>
>         Agda mailing list<br>
>         <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>         <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
<br>
<br>
</div></div></blockquote></div><br></div>