Printing Effects should support vm_compute and native_compute

[JasonGross]

Or if there is already support, this should be tested. @herbelin @maximedenes @ppedrot @silene (apparently I can't just tag @coq/vm-native-maintainers from a different repo), any thoughts on how feasible this is?

[maximedenes]

I'd expect it to be reasonably simple for native_compute (because it generates OCaml code, you could simply insert a call to a hook). Maybe less so for vm_compute, where you'd need to call this hook from the VM.

[silene]

I have some long-term plans to make it possible to register arbitrary OCaml functions fot VM execution (i.e., an Axiom command that would also take the name of a plugin-registered OCaml function). This would make this feature trivial to implement.

[JasonGross]

I am thinking about this feature again. I presume this needs special support Coq-side? Some sort of hook that plugins can call which says "when emitting native/VM code for this constant, please also emit this extra code above the function, and, underneath the closure for n arguments, emit let () := <custom code> in ... where the custom code is wrapped in parens and applied to the first n arguments"?

(Also, I'd like a version that works in the VM that doesn't require Axiom if possible. It seems fine to require a constant that is Qed-opaque / module-locked, and to taint it for Print Assumptions / the checker as "uses custom reduction in the VM")