Add debugging support to the rewriter

[JasonGross]

It's quite painful to figure out why rewriter rules aren't matching. It should be possible, using a combination of reduction-effects for cbv (alas, no support for native_compute / vm_compute, yet; see https://github.com/coq-community/reduction-effects/issues/8) and using extraction directives for OCaml/Haskell, to insert debug print calls in the main loop of the rewriter, to thread through and print out some sort of debugging information, with minimal overhead when we're not printing debug info.