[wp] added wpo hooks

src/plugins/wp/ProofEngine.ml

@@ -63,7 +63,8 @@ module PROOFS = WpContext.StaticGenerator(Wpo.S)
         }
     end)
 
-let () = Wpo.on_remove PROOFS.remove
+let () = Wpo.add_removed_hook PROOFS.remove
+let () = Wpo.add_cleared_hook PROOFS.clear
 
 let get wpo =
   try

src/plugins/wp/ProofEngine.mli

@@ -67,8 +67,6 @@ val node_context : node -> WpContext.t
 val title : node -> string
 val proved : node -> bool
 val pending : node -> int
-(** 0 means proved *)
-
 val parent : node -> node option
 val children : node -> (string * node) list
 val tactical : node -> ProofScript.jtactic option

src/plugins/wp/wpo.ml

@@ -549,6 +549,18 @@ struct
 
 end
 
+(* -------------------------------------------------------------------------- *)
+(* --- Wpo Hooks                                                          --- *)
+(* -------------------------------------------------------------------------- *)
+
+let modified_hooks : (t -> unit) list ref = ref []
+let removed_hooks : (t -> unit) list ref = ref []
+let cleared_hooks : (unit -> unit) list ref = ref []
+
+let add_modified_hook f = modified_hooks := !modified_hooks @ [f]
+let add_removed_hook f = removed_hooks := !removed_hooks @ [f]
+let add_cleared_hook f = cleared_hooks := !cleared_hooks @ [f]
+
 (* -------------------------------------------------------------------------- *)
 (* --- Wpo Database                                                       --- *)
 (* -------------------------------------------------------------------------- *)
@@ -596,6 +608,7 @@ let clear_system system =
     system.results <- WPOmap.empty ;
     system.age <- WPOmap.empty ;
     Hproof.clear system.proofs ;
+    List.iter (fun f -> f ()) !cleared_hooks ;
   end
 
 module SYSTEM = State_builder.Ref
@@ -667,15 +680,12 @@ let add g =
           Wp_parameters.feedback ~ontty:`Feedback "Computing [%d goals...]" !added ;
         added := 0 ;
       end ;
+    List.iter (fun f -> f g) !modified_hooks ;
   end
 
-let remove_hook = ref []
-let on_remove f = remove_hook := !remove_hook @ [f]
-
 let remove g =
   let system = SYSTEM.get () in
   begin
-    List.iter (fun f -> f g) !remove_hook ;
     let ip = WpPropId.property_of_id g.po_pid in
     system.wpo_idx <- unindex_wpo Gmap.add Gmap.find g.po_idx g system.wpo_idx ;
     system.wpo_ip <- unindex_wpo Pmap.add Pmap.find ip g system.wpo_ip ;
@@ -687,6 +697,7 @@ let remove g =
     end ;
     system.results <- WPOmap.remove g system.results ;
     Hproof.remove system.proofs (proof g ip) ;
+    List.iter (fun f -> f g) !removed_hooks ;
   end
 
 let warnings = function
@@ -722,31 +733,34 @@ let clear_results g =
   try
     let rs = WPOmap.find g system.results in
     Results.clear rs ;
+    List.iter (fun f -> f g) !modified_hooks ;
   with Not_found -> ()
 
 let set_result g p r =
   let system = SYSTEM.get () in
-  begin
-    let rs =
-      try WPOmap.find g system.results
-      with Not_found ->
-        let rs = Results.create () in
-        system.results <- WPOmap.add g rs system.results ; rs
-    in
-    Results.replace rs p r ;
-    if not (WpPropId.is_check g.po_pid) &&
-       not (WpPropId.is_tactic g.po_pid) &&
-       VCS.is_verdict r
-    then
+  let rs =
+    try WPOmap.find g system.results
+    with Not_found ->
+      let rs = Results.create () in
+      system.results <- WPOmap.add g rs system.results ; rs
+  in
+  Results.replace rs p r ;
+  if not (WpPropId.is_check g.po_pid) &&
+     not (WpPropId.is_tactic g.po_pid) &&
+     VCS.is_verdict r
+  then
+    begin
       let smoke = is_smoke_test g in
       let proof = find_proof system g in
       let emitter = WpContext.get_emitter g.po_model in
       let target = WpPropId.target proof in
       let unproved = not (WpPropId.is_proved proof) in
-      if VCS.is_valid r then
-        WpPropId.add_proof proof g.po_pid (get_depend g)
-      else if smoke then
-        WpPropId.add_invalid_proof proof ;
+      begin
+        if VCS.is_valid r then
+          WpPropId.add_proof proof g.po_pid (get_depend g)
+        else if smoke then
+          WpPropId.add_invalid_proof proof ;
+      end ;
       let proved = WpPropId.is_proved proof in
       let status =
         if smoke then
@@ -762,8 +776,10 @@ let set_result g p r =
       in
       let hyps = if smoke then [] else WpPropId.dependencies proof in
       Property_status.emit emitter ~hyps target status ;
-      if smoke && unproved && proved then WpReached.set_doomed emitter g.po_pid ;
-  end
+      if smoke && unproved && proved then
+        WpReached.set_doomed emitter g.po_pid ;
+    end ;
+  List.iter (fun f -> f g) !modified_hooks
 
 let has_verdict g p =
   let system = SYSTEM.get () in

src/plugins/wp/wpo.mli

@@ -142,7 +142,6 @@ val qed_time : t -> float
 
 val clear : unit -> unit
 val remove : t -> unit
-val on_remove : (t -> unit) -> unit
 
 val add : t -> unit
 val age : t -> int (* generation *)
@@ -156,6 +155,19 @@ val resolve : t -> bool
 val set_result : t -> prover -> result -> unit
 val clear_results : t -> unit
 
+val add_modified_hook : (t -> unit) -> unit
+(** Hook is invoked for each goal results modification.
+    Remark: [clear()] does not trigger those hooks,
+    Cf. [add_cleared_hook] instead. *)
+
+val add_removed_hook : (t -> unit) -> unit
+(** Hook is invoked for each removed goal.
+    Remark: [clear()] does not trigger those hooks,
+    Cf. [add_cleared_hook] instead. *)
+
+val add_cleared_hook : (unit -> unit) -> unit
+(** Register a hook when the entire table is cleared. *)
+
 val compute : t -> Definitions.axioms option * Conditions.sequent
 
 (** Warning: Prover results are stored as they are from prover output,