[Agda] Typing.CheckRHS

[Ulf Norell]

Why don't you try to nail down the culprit further by replacing terms by
'any', defined as

postulate any : ∀ {a} {A : Set a} → Set

?

/ Ulf

On Mon, Apr 17, 2017 at 11:14 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Mon, 2017-04-17 at 23:07 +0300, Sergei Meshveliani wrote:
> > Dear Agda developers,
> >
> > I continue investigating the type check cost of various parts in my
> > project.
> > And for certain module  Integer2.agda,  the option  -v profile:7
> > shows something new:
> >
> >     Typing.CheckRHS    267,464ms
> >
> > This occurs the greatest part in Total for this module
> > (while in other considered modules the main part was Serialization and
> > Serialization).
> > Can you, please comment this?
>
>
> First I comment out a large last part in  Integer2.agda.
> Then I move the "{-" mark down, to add a small current piece of code,
> and see how the checker profile report changes.
> And I find the point at which the cost jumps up.
> The Total increases 2.5 times, and instead of  Serialization and
> Deserialization, the main cost part becomes
>
>   Typing.CheckRHS   266,620ms
>
> What does this Typing.CheckRHS mean, what is its difference to
> Serialization ?
> The responsible fragment is small:
>
> hasSquare?-asd :  Decidable HasSquare-asd
> hasSquare?-asd (asd' (x , x≢0)) =
>   case
>       Nat2.hasSquare? ∣ x ∣
>   of \
>   { (yes hasSq-∣x∣) →
>                let hasSq-x : HasSquare x
>                    hasSq-x = proj₂ HasSquare-x←→HasSquare-∣x∣ hasSq-∣x∣
>                in  yes $ HasSquare→HasSquare-asd hasSq-x
>
>   ; (no ¬hasSq-∣x∣) →
>        let
>          ¬hasSq[X] : ¬ HasSquare-asd (asd' (x , x≢0))
>          ¬hasSq[X] =
>             \hasSq[X] →
>             let hasSq-x   = HasSquare-asd→HasSquare x≢0 hasSq[X]
>                 hasSq-∣x∣ = proj₁ HasSquare-x←→HasSquare-∣x∣ hasSq-x
>             in  ¬hasSq-∣x∣ hasSq-∣x∣
>        in
>        no ¬hasSq[X]
>   }
>
> Can you please, give a hint about what can be happening there in the
> checker?
>
> (The code is about an integer  x  having a square factor,  (abs x) : Nat
> having a square factor,  and  (asd x)   having a square factor
> -- about the relation between these three assertions. And  asd x  means
> here  x  or  (- x).
>
> The module  Integer2.hs  uses many instances for ℤ of rather complex
> deneric structures.
> ).
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170418/15382440/attachment.html>