[Agda] Normalisation before termination checking

[Anton Setzer]

Nils Anders Danielsson wrote:
> 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.
> 

Can you explain what the exact problem is? There might be a theoretical
problem behind this, and making a quick adhoc fix might not be the
right solution.

Anton


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------