There has been some sort of profiling support in Poly/ML almost since the beginning. I have a feeling that the numbering system used in PolyML.profiling dates back to the old Poly language. There have been some recent changes to add support for yet another profiling mode, an option that profiles the time spent in a function but only for the calling thread, giving a way of separating out the work done in a multi-threaded application. It seemed like a good opportunity to revisit the whole thing.
I've moved all aspects of profiling into a new structure PolyML.Profiling and removed the PolyML.profiling switch. The various options are now controlled by a datatype and there is a function "profile" that takes a mode, a function and an argument, runs the function by applying it the argument and prints the profile at the end.
datatype profileMode = ProfileTime | ProfileAllocations | ProfileLongIntEmulation | ProfileTimeThisThread
val profile = fn: profileMode -> ('a -> 'b) -> 'a -> 'b
There are a couple of profiling modes that are a bit different since they print information about the state of the heap as the result of the previous computation. They are intended for use with PolyML.Compiler.allocationProfiling which causes the compiler to add extra information about where cells have been allocated.
datatype profileDataMode = ProfileLiveData | ProfileLiveMutableData val profileData = fn: profileDataMode -> unit
Finally there are additional versions of the functions that take an extra argument to enable an application (e.g. Isabelle) to capture the output from profiling. They take a function that is called with the unsorted list of counts and names.
val profileDataStream = fn: ((int * string) list -> unit) -> profileDataMode -> unit val profileStream = fn: ((int * string) list -> unit) -> profileMode -> ('a -> 'b) -> 'a -> 'b
David