diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index f261a580dd75e40ef1ba245c2637c389722f5cf7..8afee8c578720ab8426e8ec11efc503a4f0b4305 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -655,7 +655,7 @@ let prove_annot wpo vcq ~mode =
begin fun () ->
let prop =
WpContext.on_context (Wpo.get_context wpo)
- GOAL.compute_proof vcq.VC_Annot.goal in
+ (GOAL.compute_proof ~pid:wpo.po_pid) vcq.VC_Annot.goal in
prove_prop wpo ~mode ~axioms:None ~prop
end
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index f217f28fc42c4b4e3a7b8df7eedd7ccd6d45683d..e78bb4bb0f79193b9f870cac7d9b4633963886ff 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -491,7 +491,7 @@ let prove_annot context pid vcq ~config ~mode =
Task.todo
begin fun () ->
let axioms = vcq.VC_Annot.axioms in
- let prop = GOAL.compute_proof vcq.VC_Annot.goal in
+ let prop = GOAL.compute_proof ~pid vcq.VC_Annot.goal in
prove_prop ~pid ~config ~mode ~context ~axioms ~prop
end
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 803bf87115076503721d2446610b4cb13265dc57..adb7fd3e831b90bc20e8cdb0d4acdd56eb84ac60 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1104,7 +1104,7 @@ let task_of_wpo wpo =
| Wpo.GoalAnnot v ->
let pid = wpo.Wpo.po_pid in
let axioms = v.Wpo.VC_Annot.axioms in
- let prop = Wpo.GOAL.compute_proof v.Wpo.VC_Annot.goal in
+ let prop = Wpo.GOAL.compute_proof ~pid v.Wpo.VC_Annot.goal in
(* Format.printf "Goal: %a@." Lang.F.pp_pred prop; *)
prove_prop ~pid prop ?axioms
| Wpo.GoalLemma v ->
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index 32355d2fc93dbf0e666f73d1439067e66e63d405..4c9c013695cf456b287d57b70fd109bf6a1a380c 100644
--- a/src/plugins/wp/VC.ml
+++ b/src/plugins/wp/VC.ml
@@ -46,7 +46,8 @@ let get_formula po =
match po.po_formula with
| GoalLemma l -> l.VC_Lemma.lemma.Definitions.l_lemma
| GoalAnnot { VC_Annot.goal = g } ->
- WpContext.on_context (get_context po) Wpo.GOAL.compute_proof g
+ WpContext.on_context
+ (get_context po) (Wpo.GOAL.compute_proof ~pid:po.po_pid) g
let clear = Wpo.clear
let proof = Wpo.goals_of_property
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 87e0a0e59fb8e235300525eb4c570f89474260ed..bd90f0d1795fcc69eed0efada0cc924598649f2d 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1248,7 +1248,7 @@ let print_generated ?header file =
let protect e =
if debug_atleast 1 then false else
match e with
- | Db.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
+ | Sys.Break | Db.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
| _ -> true
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 0d0bf47c4f8059caf2d74312150bcc67f866f3ae..d94196679bf26f7b825d4f23d4ab8fcc44ca70ea 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -190,8 +190,13 @@ struct
let is_trivial g = Conditions.is_trivial g.sequent
+ let dkey = Wp_parameters.register_category "qed"
+
let apply option phi g =
- try g.sequent <- phi g.sequent
+ try
+ Db.yield () ;
+ Wp_parameters.debug ~dkey "Appy %s" option ;
+ g.sequent <- phi g.sequent ;
with exn when Wp_parameters.protect exn ->
Wp_parameters.warning ~current:false ~once:true
"Goal simplification aborted (%s):@\n\
@@ -207,7 +212,7 @@ struct
let preprocess g =
if Wp_parameters.Let.get () then
begin
- apply "introcution" Conditions.introduction_eq g ;
+ apply "introduction" Conditions.introduction_eq g ;
let fold acc (get,solver) = if get () then solver::acc else acc in
let solvers = List.fold_left fold [] default_simplifiers in
apply "-wp-simplify-*" (Conditions.simplify ~solvers) g ;
@@ -229,26 +234,24 @@ struct
g.sequent <- Conditions.trivial ;
g.obligation <- Conditions.close g.sequent
- let dkey = Wp_parameters.register_category "prover"
-
- let safecompute g =
+ let safecompute ~pid g =
begin
g.simplified <- true ;
let timer = ref 0.0 in
- Wp_parameters.debug ~dkey "Simplify goal" ;
+ Wp_parameters.debug ~dkey "Simplify %a" WpPropId.pretty pid ;
Command.time ~rmax:timer preprocess g ;
Wp_parameters.debug ~dkey "Simplification time: %a"
Rformat.pp_time !timer ;
g.time <- !timer ;
end
- let compute g =
+ let compute ~pid g =
if not g.simplified then
Lang.local ~vars:(Conditions.vars_seq g.sequent)
- safecompute g
+ (safecompute ~pid) g
- let compute_proof g = compute g ; g.obligation
- let compute_descr g = compute g ; g.sequent
+ let compute_proof ~pid g = compute ~pid g ; g.obligation
+ let compute_descr ~pid g = compute ~pid g ; g.sequent
let get_descr g = g.sequent
let qed_time g = g.time
@@ -324,7 +327,7 @@ struct
effect = None ;
}
- let resolve vcq = GOAL.compute_proof vcq.goal == Lang.F.p_true
+ let resolve ~pid vcq = GOAL.compute_proof ~pid vcq.goal == Lang.F.p_true
let is_trivial vcq = GOAL.is_trivial vcq.goal
let pp_effect fmt = function
@@ -350,7 +353,7 @@ struct
Format.fprintf fmt "@].@\n" ;
end ;
pp_warnings fmt vc.warn ;
- Pcond.pretty fmt (GOAL.compute_descr vc.goal) ;
+ Pcond.pretty fmt (GOAL.compute_descr ~pid vc.goal) ;
List.iter
(fun (prover,result) ->
if result.verdict <> NoResult then
@@ -792,8 +795,11 @@ let is_trivial g =
let reduce g =
match g.po_formula with
- | GoalLemma vc -> WpContext.on_context (get_context g) VC_Lemma.is_trivial vc
- | GoalAnnot vc -> WpContext.on_context (get_context g) VC_Annot.resolve vc
+ | GoalLemma vc ->
+ WpContext.on_context (get_context g) VC_Lemma.is_trivial vc
+ | GoalAnnot vc ->
+ let pid = g.po_pid in
+ WpContext.on_context (get_context g) (VC_Annot.resolve ~pid) vc
let resolve g =
let valid = reduce g in
@@ -806,7 +812,8 @@ let compute g =
let ctxt = get_context g in
match g.po_formula with
| GoalAnnot { VC_Annot.axioms ; VC_Annot.goal = goal } ->
- axioms , WpContext.on_context ctxt GOAL.compute_descr goal
+ let pid = g.po_pid in
+ axioms , WpContext.on_context ctxt (GOAL.compute_descr ~pid) goal
| GoalLemma ({ VC_Lemma.depends = depends ; VC_Lemma.lemma = lemma } as w) ->
let open Definitions in
Some( lemma.l_cluster , depends ) ,
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 98e14b7efc254befdda2e7a1c6eecfb4942c2f8f..580b64694974e7616ee540e1c31dd8e83d09b8ac 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -54,10 +54,10 @@ sig
val trivial : t
val is_trivial : t -> bool
val make : Conditions.sequent -> t
- val compute_proof : t -> F.pred
- val compute_descr : t -> Conditions.sequent
+ val compute : pid:WpPropId.prop_id -> t -> unit
+ val compute_proof : pid:WpPropId.prop_id -> t -> F.pred
+ val compute_descr : pid:WpPropId.prop_id -> t -> Conditions.sequent
val get_descr : t -> Conditions.sequent
- val compute : t -> unit
val qed_time : t -> float
end
@@ -88,8 +88,8 @@ sig
effect : (stmt * effect_source) option ;
}
- val resolve : t -> bool
val is_trivial : t -> bool
+ val resolve : pid:prop_id -> t -> bool
val cache_descr : pid:prop_id -> t -> (prover * result) list -> string
end