3.4.9 Profile structure values

profile

Type

Summary

The type used to record profiler results.

Signature

MLWORKS.Profile

Structure

MLWorks.Profile

Type

datatype profile = Profile of {general: general_header, call: call_header, time: time_header, space: space_header, cost: cost_header, functions: function_profile list, centres: cost_centre_profile list}

Description

The type used to record profiler results. The profile function returns a value of this type. The record contains the following data:

functions: A value of type function_profile list. This value contains the execution profile of each function call profiled.
general: A value of type general_header. This value contains general data about the allocation during and time taken by the call to the profiler.
call: A value of type call_header. This value records the number of functions that were call-count profiled.
time: A value of type time_header. This value records overall time-profiling statistics.
space: A value of type space_header. This value records overall space-profiling statistics.
cost: A value of type cost_header. This value is unused at present. It may record cost-centre profiling information in a future release.
centres: A value of type cost_centre_profile. This value is unused at present. It may record cost-centre profiling information in a future release.