From c5d247a87cc9992a254e9e0287dc722a1bf45692 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Jan 2024 11:03:55 +0100
Subject: [PATCH] [wp] removed nodes callbacks
---
src/plugins/server/data.ml | 17 +++++++++++++++++
src/plugins/server/data.mli | 4 ++++
src/plugins/wp/ProofEngine.ml | 14 +++++++++-----
src/plugins/wp/ProofEngine.mli | 2 ++
src/plugins/wp/wpTipApi.ml | 6 ++++++
5 files changed, 38 insertions(+), 5 deletions(-)
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index bdaa0d0c315..c3229cdde4a 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -593,6 +593,7 @@ sig
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val find : key -> 'a t -> 'a
+ val remove : key -> 'a t -> 'a t
end
module type Index =
@@ -601,6 +602,7 @@ sig
type tag
val get : t -> tag
val find : tag -> t
+ val remove : t -> unit
val clear : unit -> unit
end
@@ -611,6 +613,7 @@ sig
val clear : index -> unit
val get : index -> M.key -> int
val find : index -> int -> M.key
+ val remove : index -> M.key -> unit
val to_json : index -> M.key -> json
val of_json : index -> json -> M.key
end =
@@ -643,6 +646,13 @@ struct
m.index <- M.add a id m.index ;
Hashtbl.add m.lookup id a ; id
+ let remove m a =
+ try
+ let id = M.find a m.index in
+ Hashtbl.remove m.lookup id ;
+ m.index <- M.remove a m.index ;
+ with Not_found -> ()
+
let find m id = Hashtbl.find m.lookup id
let to_json m a = `Int (get m a)
@@ -662,6 +672,7 @@ struct
let clear () = INDEX.clear index
let get = INDEX.get index
let find = INDEX.find index
+ let remove = INDEX.remove index
include
(struct
type t = M.key
@@ -694,6 +705,7 @@ struct
let index () = STATE.get ()
let clear () = INDEX.clear (index())
+ let remove a = INDEX.remove (index()) a
let get a = INDEX.get (index()) a
let find id = INDEX.find (index()) id
@@ -761,6 +773,11 @@ struct
let hash = lookup () in
if not (Hashtbl.mem hash tag) then Hashtbl.add hash tag x ; tag
+ let remove x =
+ let tag = A.id x in
+ let hash = lookup () in
+ Hashtbl.remove hash tag
+
include
(struct
type t = A.t
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index c9fe14a36a5..36a02e94a65 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -357,6 +357,7 @@ sig
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val find : key -> 'a t -> 'a
+ val remove : key -> 'a t -> 'a t
end
(** Datatype extended with access to value identifiers. *)
@@ -368,6 +369,9 @@ sig
val find : tag -> t
(** @raise Not_found if not registered. *)
+ val remove : t -> unit
+ (** Remove item from index tables. Use with extreme care. *)
+
val clear : unit -> unit
(** Clear index tables. Use with extreme care. *)
end
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index c1398c17a5c..1d223fd0864 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -113,6 +113,12 @@ let set_saved t s = t.saved <- s
(* --- Removal --- *)
(* -------------------------------------------------------------------------- *)
+let clear_hooks = ref []
+let remove_hooks = ref []
+
+let add_clear_hook fn = clear_hooks := !clear_hooks @ [fn]
+let add_remove_hook fn = remove_hooks := !remove_hooks @ [fn]
+
let rec revert_tactic t n =
n.strategy <- None ;
match n.script with
@@ -125,15 +131,13 @@ and remove_node t n =
Wpo.remove n.goal
else
Wpo.clear_results n.goal ;
- begin
- match t.head with
- | Some n0 when n0 == n -> t.head <- None
- | _ -> ()
- end ;
+ List.iter (fun f -> f n) !remove_hooks ;
+ Option.iter (fun n0 -> if n0 == n then t.head <- None) t.head ;
revert_tactic t n
let clear_tree t =
begin
+ List.iter (fun f -> f ()) !clear_hooks ;
Wpo.clear_results t.main ;
Option.iter (remove_node t) t.root ;
t.gid <- 0 ;
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 31931dcb6cf..7e57c95aabc 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -101,6 +101,8 @@ val clear_tree : tree -> unit
val clear_node : tree -> node -> unit
val clear_node_tactic : tree -> node -> unit
val clear_parent_tactic : tree -> node -> unit
+val add_clear_hook : (unit -> unit) -> unit
+val add_remove_hook : (node -> unit) -> unit
val cancel_parent_tactic : tree -> unit
val cancel_current_node : tree -> unit
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index 46d2716b89b..6e56e120d90 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -59,6 +59,12 @@ module Node = D.Index
let descr = Md.plain "Proof Node index"
end)
+let () = Server.Main.once
+ begin fun () ->
+ ProofEngine.add_clear_hook Node.clear ;
+ ProofEngine.add_remove_hook Node.remove ;
+ end
+
module Tactic : D.S with type t = Tactical.t =
struct
type t = Tactical.t
--
GitLab