[Agda] Type-checker evaluator performance

[Liam O'Connor]

If I tried to normalise petersons-search by C-c C-n, it definitely wouldn’t complete in reasonable time, because it would spend too long trying to pretty print the normal form of the term (which is pretty gigantic and pretty printing isn’t fast anyway).

Your performance results with that example seem really weird. Does anyone know why that would be the case?

--  
Liam

On 2 February 2016 at 2:40:02 AM, effectfully (effectfully at gmail.com) wrote:
> I've encountered problems with functions like `Pr' (which is just
> `from-just' from the standard library) several times. E.g. using
>  
> From-Maybe : ∀ {α β} {A : Set α} -> (A -> Set β) -> Maybe A -> Set β
> From-Maybe B nothing = Lift ⊤
> From-Maybe B (just x) = B x
>  
> from-Maybe : ∀ {α β} {A : Set α} {B : A -> Set β} -> (∀ x -> B x) ->
> (x : Maybe A) -> From-Maybe B x
> from-Maybe f nothing = _
> from-Maybe f (just x) = f x
>  
> `from-Maybe proj₂ x` consumed three times more memory than `proj₂
> (from-just x)` and was noticeably slower.
>  
> I don't know whether this is the same case, but have you tried to
> normalize `petersons-search' by C-c C-n?
>