Theory profile_conversion

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory profile_conversion imports
  "AutoCorres2_Main.AutoCorres_Main"
begin


install_C_file "profile_conversion.c"

text ‹Some ML profiling for the various optimisation stages. See also the additional information
on tracing and timing in 🗏‹../examples/TraceDemo.thy›.›


declare [[verbose=1]]
declare [[verbose_timing=2]]
declare [[autocorres_profile_conversion_enabled=true]]
declare [[autocorres_profile_conversion_verbosity=1]]
declare [[ML_print_depth=10000]]

text ‹Option ▩‹trace_opt› has to be set in order for the profiling to step in.›

autocorres [trace_opt]"profile_conversion.c"

ML ‹
val res = (AutoCorresTrace.ProfileConv.get ( @{context}))
›

text ‹The table is index by a tuple: function name, phase, stage.
The output is a tuple: timing information, input term and the output term of the optimisation.
›
ML ‹
val t = AutoCorresTrace.ProfileConv.Table.lookup res ("in_loop", FunctionInfo.WA, FunctionInfo.PEEP)
›

ML ‹
val ps = AutoCorresTrace.ProfileConv.Table.dest res
›


ML ‹
open AutoCorresTrace.Statistics
›

text ‹Summary of all the information.›
ML
‹
val _ = statistics ps
›

text ‹Examples of a retrieval of results by a predicate on the elements.›
ML ‹
val unchanged_glob_add = select ps (unchanged_eq andf (same_name "glob_add"))
val changed_glob_add = select ps (changed_eq andf (same_name "glob_add"))
›

end