The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

I don't know what you mean by returning complex structure. Is it really 
huge?
In that case vm_compute can be slow because it needs to recreate the 
large structure.

What I would do is to write a simple recursive function

count_size : complex_structure -> Z

that gives a rough measure of the size of the complex structure.

Then I would do a

Time vm_compute in count_size (propagateExists  ......).

If it is slow this means that your computation is slow.
If you are using 8.6, you may then try native_compute to get a speed up.

If it is fast but the return integer is quite large this means that
the time is spend in allocating your result.
The solution maybe then to try to accumulate your computation and only 
perform your computation when the result is "small".

--
Laurent