search

coq-community / reduction-effects

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
Mozilla Public License 2.0
6 stars 6 forks source link

Printing Effects should support vm_compute and native_compute #8

Open JasonGross opened 4 years ago

JasonGross commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 1 year ago

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")