Support for timing effects

[JasonGross]

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?