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?
I'd like support for some sort of timing primitive, so that I can, e.g.,
and have reduction of
time_itprint something likeFinished reduction tag in ...., profiling the reduction off x.Probably the easiest way to implement this is with something like
push_timerandpop_timer?