[Agda] interactive Bin arith performance

[Ulf Norell]

On Thu, Jan 31, 2019 at 5:53 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Thu, 2019-01-31 at 18:40 +0300, Sergei Meshveliani wrote:
>
> >
> > And in my example of  test0 = remainder (divRem 520 10),
> > proofs are not evaluated in the compiled program.
> >
> > Now, return to Agda interpreter.
> > [..]
>
>
> Consider a more clear example of test1:
>
>
> -- of Binary-4.2 ---------------------------------------------------
> open import Binary using (Bin; 0#; 1#; 2#; 3#; 4#; 5#; _+_;
>                                                DivMod; divMod; rem)
> 10' : Bin
> 10' = 5# + 5#
>
> -- test0 = let b = stringToBin "1000001000" in rem b 10' (λ())
>
> test1 : String → Bin
> test1 str =
>           let b = stringToBin str in  rem b 10' (λ())
> -------------------------------------------------------------
>
>
> First,  C-c C-l  is applied.
> rem  is here  remainder (divRem b 10' _).
>
> test1  is type-checked, together with all functions needed for divRem.
>
> Is it known after this that no proofs need to be evaluated for
> evaluation of  test1 ?


No, why would you think that? Also it's not clear what you mean by
"evaluation of test1".
Do you mean using the compile-time evaluator, running the compiled code, or
some hypothetical
ideal evaluator.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190131/24dbc566/attachment.html>