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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
