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

Support for timing effects #18

Open JasonGross opened 1 year ago

JasonGross commented 1 year ago

I'd like support for some sort of timing primitive, so that I can, e.g.,

Polymorphic Definition time_it {T} (tag : T) {A B} (f : A -> B) (x : A) : B := f x.
Declare Timing Effect time_it.

and have reduction of time_it print something like Finished reduction tag in ...., profiling the reduction of f x.

Probably the easiest way to implement this is with something like push_timer and pop_timer?