[Agda] original Nat

[Sergei Meshveliani]

On Wed, 2017-12-20 at 12:09 +0100, Ulf Norell wrote:
> Removing the BUILTIN pragmas would do it, but I would suggest
> using a different, but isomorphic, type for your termination measures.
> That way you don't have to mess with the builtin libraries.
> 

I thought of this.
But:
this my  Bin3  library proves the isomorphism of   toℕ : Bin -> ℕ
with respect to  +, *, monotonicity of toℕ for _<_, and so on.
And this all uses many items from  Data.Nat.Properties,
and the latter items refer to the items of Data.Nat:  Nat._+_, Nat._*_,
Nat._∸_.
So that I would need to also have the version of  Nat.Properties 
with a different import.
And I wonder of whether this is all that will be needed.

Also may it have sense for Agda to provide somewhat  --primitiveNat  key
for type-checking or/and compiling without built-ins for operations on ℕ
?

------
Sergei


> 
> On Wed, Dec 20, 2017 at 12:04 PM, Sergei Meshveliani
> <mechvel at botik.ru> wrote:
>         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
>         >
>         >
>         
>         
>         
> 
>