diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 4d7794474d2f920f9dd6c27e89524573862cd13b..cccb5817a939c6b371bbfe05ccacffa4e7e0c482 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/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
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index e64e6f3234b74e5d428e69eedd951199b1d46c91..55dde001ca197b013eeaaf9d7b8f57ee7c331ab5 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/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
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index d21eb22095cfe5e1361c2a8a4ecd77d567de4ccd..852c10d1bdd7fe38048854828e9f82d97e56a41c 100644
--- a/src/plugins/wp/wpo.ml
+++ b/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
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 2cc7c59e74cbcb6db40d230dd56947588af1c254..4023e885a48b869beaaa712e1045bc9c0ee70845 100644
--- a/src/plugins/wp/wpo.mli
+++ b/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,