From 13e11b6aec1444071dc3787da15e89a6bc0eb0dc Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 14 May 2016 23:09:20 -0400
Subject: Synchronize the profiler state with the document

This is suboptimal, because mutation leaves room for subtle bugs, but
rewriting @tebbi's code to be functional was a pain, and not something I
could figure out how to do easily.  I'm working under the assumption
that there is no sharing in a single treenode, which I'm not completely
sure is valid.  That said, a few simple tests seem to indicate that this
works as expected.
---
 ltacprof/profile_ltac.ml | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

(limited to 'ltacprof')

diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml
index 71b96614ce..6ae07689dd 100644
--- a/ltacprof/profile_ltac.ml
+++ b/ltacprof/profile_ltac.ml
@@ -3,7 +3,8 @@ open Printer
 open Util
 
 
-let is_profiling = ref false
+(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. *)
+let is_profiling = Summary.ref false ~name:"is-profiling-ltac"
 let set_profiling b = is_profiling := b
 
 let should_display_profile_at_close = ref false
@@ -40,7 +41,21 @@ let add_entry e add_total {total; local; ncalls; max_total} =
   if add_total then e.max_total <- max e.max_total max_total
 
 type treenode = {entry : entry; children : (string, treenode) Hashtbl.t}
-let stack = ref [{entry=empty_entry(); children=Hashtbl.create 20}]
+
+(** Tobias Tebbi wrote some tricky code involving mutation.  Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *)
+let deepcopy_entry {total; local; ncalls; max_total} =
+  {total; local; ncalls; max_total}
+
+let rec deepcopy_treenode {entry; children} =
+  {entry = deepcopy_entry entry;
+   children =
+      (let children' = Hashtbl.create (Hashtbl.length children) in
+       Hashtbl.iter
+	 (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree))
+	 children;
+       children')}
+
+let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack"
 
 let on_stack = Hashtbl.create 5
 
-- 
cgit v1.2.3