[Agda] Normalisation before termination checking

[Arnaud Spiwack]

Note that you must be careful when doing that, if you are interested in 
Strong Normalisation :
F x = ( \ y . 0 ) ( F x )

Is weakly normalisable but not strongly normalisable, whereas    F x = 
0  (which is what you are testing after normalising the right-hand side) 
is both.


Arnaud

Nils Anders Danielsson a écrit :
> Hi,
>
> I suggest that right-hand sides should be normalised before the
> termination checker is run (with the defined names treated as neutral,
> of course). This is not very important in the inductive case, but for
> coinductive definitions my impression is that it would really improve
> modularity and abstraction.
>
> One drawback might be that typechecking becomes considerably slower.
> Currently there are two termination checking passes. The first one
> does not include dotted arguments, whereas the second does, and the
> second one is only run if the first one fails. I suggest that
> normalisation is only performed in the second pass.
>
> Are there any other drawbacks that I have missed? I suspect that it is
> very easy to implement this change.
>
>