Hi René,
You are right, in the case of pattern matches on a single argument, the elimination of the
0/Suc patterns could be done like that. The only tricky bit is to handle sequential
pattern matches correctly, i.e.,
lemma [code]:
"foo (Suc n) = False"
"foo m = Code.abort ''invalid argument'' (%_. foo m)"
should raise the error "invalid argument" rather than ''pattern match failed''.
The situation gets complicated when there are pattern matches on several arguments and the
patterns overlap. Especially if you want to preserve the strictness of generated Haskell
functions, the task becomes non-trivial.
Feel free to improve the current preprocessor. Maybe being able to deal with a few special
cases would be enough in practice.
Andreas