From 0a289372c33fa16b13cf47e335ad53b12253bb0a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 5 May 2023 11:32:07 +0200
Subject: [PATCH] [wp] fix things
---
src/plugins/wp/ProofEngine.ml | 2 +-
src/plugins/wp/ProverScript.ml | 39 +++++++++++++++++-----------------
2 files changed, 21 insertions(+), 20 deletions(-)
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 52c83f5c4e1..c15320f187b 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -141,7 +141,7 @@ let iteri f tree =
let rec depth node =
match node.parent with
| None -> 0
- | Some p -> depth p
+ | Some p -> succ @@ depth p
(* -------------------------------------------------------------------------- *)
(* --- Consolidating --- *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index cd6df4e6436..146c4e82eaa 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -331,19 +331,20 @@ let rec sequence (f : 'a -> solver) = function
| [] -> unknown
| x::xs -> f x +>> sequence f xs
-let rec explore_strategy env p s : solver =
+let rec explore_strategy env process strategy : solver =
sequence
- (explore_alternative env p s)
- (ProofStrategy.alternatives s)
-
-and explore_alternative env p s a : solver =
- explore_provers env a +>>
- explore_tactic env p s a +>>
- explore_auto env p a +>>
- explore_fallback env p a
-
-and explore_provers env a : solver =
- let provers,timeout = ProofStrategy.provers ~default:env.Env.provers a in
+ (explore_alternative env process strategy)
+ (ProofStrategy.alternatives strategy)
+
+and explore_alternative env process strategy alternative : solver =
+ explore_provers env alternative +>>
+ explore_tactic env process strategy alternative +>>
+ explore_auto env process alternative +>>
+ explore_fallback env process alternative
+
+and explore_provers env alternative : solver =
+ let provers,timeout =
+ ProofStrategy.provers ~default:env.Env.provers alternative in
sequence (explore_prover env timeout) provers
and explore_prover env timeout prover node =
@@ -354,13 +355,13 @@ and explore_prover env timeout prover node =
let config = { VCS.default with timeout = Some timeout } in
Env.prove env wpo ~config prover
-and explore_tactic env process s a node =
- match ProofStrategy.tactic env.tree node s a with
+and explore_tactic env process strategy alternative node =
+ match ProofStrategy.tactic env.tree node strategy alternative with
| None -> failed
| Some nodes -> List.iter process nodes ; success
-and explore_auto env process a node =
- match ProofStrategy.auto a with
+and explore_auto env process alternative node =
+ match ProofStrategy.auto alternative with
| None -> failed
| Some h ->
match ProverSearch.search env.tree ~anchor:node [h] with
@@ -369,10 +370,10 @@ and explore_auto env process a node =
List.iter (fun (_,node) -> process node) @@
snd @@ ProofEngine.commit fork ; success
-and explore_fallback env process a node =
- match ProofStrategy.fallback a with
+and explore_fallback env process alternative node =
+ match ProofStrategy.fallback alternative with
| None -> failed
- | Some s -> explore_strategy env process s node
+ | Some strategy -> explore_strategy env process strategy node
let explore_hint env process node =
if ProofEngine.depth node > env.Env.depth then failed
--
GitLab