From 75c0c5c2b460614fba6705c6e0d64859815a613c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Sep 2017 00:40:19 +0200
Subject: [stm] Switch to a functional API

We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.

For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.

Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
---
 plugins/ltac/profile_ltac.ml | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 32494a8793..9ae8bfe65b 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -367,18 +367,30 @@ let do_profile s call_trace tac =
 
 let get_local_profiling_results () = List.hd Local.(!stack)
 
-module SM = Map.Make(Stateid.Self)
+(* We maintain our own cache of document data, given that the
+   semantics of the STM implies that synchronized state for opaque
+   proofs will be lost on QED. This provides some complications later
+   on as we will have to simulate going back on the document on our
+   own. *)
+module DData = struct
+    type t = Feedback.doc_id * Stateid.t
+    let compare x y = Pervasives.compare x y
+end
+
+module SM = Map.Make(DData)
 
 let data = ref SM.empty
 
 let _ =
   Feedback.(add_feeder (function
-    | { id = s; contents = Custom (_, "ltacprof_results", xml) } ->
+    | { doc_id = d;
+        span_id = s;
+        contents = Custom (_, "ltacprof_results", xml) } ->
         let results = to_ltacprof_results xml in
         let other_results = (* Multi success can cause this *)
-          try SM.find s !data
+          try SM.find (d,s) !data
           with Not_found -> empty_treenode root in
-        data := SM.add s (merge_roots results other_results) !data
+        data := SM.add (d,s) (merge_roots results other_results) !data
     | _ -> ()))
 
 let reset_profile () =
@@ -388,7 +400,10 @@ let reset_profile () =
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =
-  let valid id _ = Stm.state_of_id id <> `Expired in
+  (* The STM doesn't provide yet a proper document query and traversal
+     API, thus we need to re-check if some states are current anymore
+     (due to backtracking) using the `state_of_id` API. *)
+  let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in
   data := SM.filter valid !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
-- 
cgit v1.2.3