I wonder if it would be possible to add explicit support for Church numerals.
You can't detect any if they are created during reduction, but you could probably recognize constants and do simple pattern matching for succ, addition, multiplication, and exponentiation.
