[Agda] Interactive copattern splitting

[Andreas Abel]

I created a git-branch 'splitResult' that implements copattern splitting:

* New feature: Interactively split result.

   Make case (C-c C-c) with no variables given tries to split on the
   result to introduce projection patterns.  The hole needs to be of
   record type, of course.

     test : {A B : Set} (a : A) (b : B) → A × B
     test a b = ?

   Result-splitting ? will produce the new clauses:

     proj₁ (test a b) = ?
     proj₂ (test a b) = ?

   If hole is of function type ending in a record type, the necessary
   pattern variables will be introduced before the split.  Thus, the
   same result can be obtained by starting from:

     test : {A B : Set} (a : A) (b : B) → A × B
     test = ?

It has been on my todo-list for long, but Cezar's question on DTP 
whether such a feature would be available in Idris soon made me jealous 
enough to implement it now.

Feedback welcome.

Since this feature is release-ready, I might merge it into maint-2.4.0 
for faster dissemination.  'master' contains also features that are not 
so stable and cannot be released from one day to the next.

Opinions? Ulf?

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/