The Coq mailing list

["Tillmann Weisser" <tweisser AT laas.fr>]

Dear Coq-Club,

I want to do a time analysis of a function in my code. However, I don't 
really know how to do this. Here is my problem:

Given 3 types A, B and C and converting functions g: A -> B and h: B -> C. I 
want to analyse the function f:= h o g.  In particular I'm interested in the 
question which part of f (i.e. g or h)  takes most of the time.

Let now a be of type A. I ran the commands

Time Eval vm_compute in (f a).
Time Eval vm_compute in (g a).
Let b:= Eval vm_compute in (g a).
Time Eval vm_compute in (h b).

However, the evaluation of (h b) is as slow as the evaluation of (f a), 
whereas the evaluation of (g a) is a little bit faster than the others. (The 
times of (g a) and (h b) do not sum up to the time of (f a).) What can I 
conclude from that? Is there a better way to analyse f?

Thanks for your help in advance!
 Tillmann