Improve AutoCorrode automation and timing diagnostics

Autogen/AutoCommon.thy

@@ -7,14 +7,48 @@ begin
 
 ML\<open>
   \<comment>\<open>Trace level: The higher, the more verbose the logging gets\<close>
-  val locality_trace_level = Attrib.setup_config_int @{binding "locality_trace_level"} (K 1)
+  val locality_trace_level = Attrib.setup_config_int @{binding "locality_trace_level"} (K 0)
 
-  \<comment>\<open>Log text at given debug level; will be dropped if larger than \<^verbatim>\<open>locality_trace_level\<close>.\<close>
-  fun locality_pretty_trace ctxt lvl =
-    if lvl <= Config.get ctxt locality_trace_level then
-      Pretty.string_of #> tracing
-    else
-      K ()
+  \<comment>\<open>Construct and log text at the given debug level only when tracing is enabled.
+     Level zero disables tracing; positive levels retain the existing verbosity ordering.\<close>
+  fun locality_pretty_trace ctxt lvl (pretty : unit -> Pretty.T) =
+    let val trace_level = Config.get ctxt locality_trace_level in
+      if 0 < trace_level andalso lvl <= trace_level
+      then pretty () |> Pretty.string_of |> tracing
+      else ()
+    end
+
+  \<comment>\<open>Authoritative invocation-context switch for AutoLocality cancellation simprocs.\<close>
+  val locality_cancel_enabled =
+    Attrib.setup_config_bool @{binding "locality_cancel_enabled"} (K true)
+
+  \<comment>\<open>When set, the locality commands report how long each generated sub-proof takes. This is a
+     diagnostic for spotting which phase (commutativity / disjointness / local-action) dominates,
+     independent of the verbosity governed by \<^verbatim>\<open>locality_trace_level\<close>.\<close>
+  val locality_timing = Attrib.setup_config_bool @{binding "locality_timing"} (K false)
+
+  \<comment>\<open>Time a thunk and, if \<^verbatim>\<open>locality_timing\<close> is set, report the elapsed time under \<^verbatim>\<open>label\<close>.\<close>
+  fun locality_time ctxt (label : string) (f : unit -> 'a) : 'a =
+    if Config.get ctxt locality_timing then
+      let
+        val timer = Timing.start ()
+        val result = f ()
+        val _ = tracing ("[locality timing] " ^ label ^ ": " ^ Timing.message (Timing.result timer))
+      in result end
+    else f ()
+
+  \<comment>\<open>As \<^verbatim>\<open>locality_time\<close>, but for a tactic. The tactic's result sequence is forced eagerly so the
+     measurement captures the real proof-search cost rather than the (lazy) construction of the
+     sequence. The generated goals are deterministic (at most one result), so forcing is safe.\<close>
+  fun locality_time_tac ctxt (label : string) (tac : tactic) : tactic =
+    if Config.get ctxt locality_timing then
+      (fn st =>
+        let
+          val timer = Timing.start ()
+          val results = Seq.list_of (tac st)
+          val _ = tracing ("[locality timing] " ^ label ^ ": " ^ Timing.message (Timing.result timer))
+        in Seq.of_list results end)
+    else tac
 
   \<comment>\<open>Lookup named theorem list by name. If it does not exist, return \<^verbatim>\<open>NONE\<close>.
      If it does, return the fully qualified name.\<close>
@@ -30,8 +64,9 @@ ML\<open>
        NONE =>
          let
            val (name', ctxt') = Named_Theorems.declare (Binding.make (name, Position.none)) "" ctxt
-           val _ = Pretty.text "Created named theorem list:" @ [Pretty.brk 1, Pretty.str name]
-                |> Pretty.block |> locality_pretty_trace ctxt 1
+           val _ = locality_pretty_trace ctxt 1 (fn () =>
+             Pretty.text "Created named theorem list:" @ [Pretty.brk 1, Pretty.str name]
+             |> Pretty.block)
          in
            (true, name', ctxt')
          end
@@ -57,4 +92,4 @@ ML\<open>
     end
 \<close>
 
-end
+end