From cccc12b5dba204b91042a0f14373b978b42ead91 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 28 Mar 2023 10:55:57 +0200
Subject: [PATCH] [wp] insert strategy in jscript
---
src/plugins/wp/ProofScript.ml | 11 ++++++++---
src/plugins/wp/ProofScript.mli | 3 ++-
src/plugins/wp/ProverScript.ml | 17 +++++++++++------
3 files changed, 21 insertions(+), 10 deletions(-)
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index b0d374a7456..9d72711ea9a 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -281,14 +281,16 @@ type jtactic = {
tactic : string ;
params : Json.t ;
select : Json.t ;
+ strategy : string option ;
}
-let jtactic (tac : tactical) (sel : selection) =
+let jtactic ?strategy (tac : tactical) (sel : selection) =
{
header = tac#title ;
tactic = tac#id ;
params = json_of_parameters tac ;
select = json_of_selection sel ;
+ strategy = Option.map ProofStrategy.name strategy ;
}
let json_of_tactic t js =
@@ -314,8 +316,11 @@ let tactic_of_json js =
let tactic = js >? "tactic" |> Json.string in
let params = try js >? "params" with Not_found -> `Null in
let select = try js >? "select" with Not_found -> `Null in
- let children = try js >? "children" |> children_of_json with Not_found -> [] in
- Some( { header ; tactic ; params ; select } , children )
+ let children =
+ try js >? "children" |> children_of_json with Not_found -> [] in
+ let strategy =
+ try Some (js >? "strategy" |> Json.string) with Not_found -> None in
+ Some( { header ; tactic ; params ; select ; strategy } , children )
with _ -> None
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofScript.mli b/src/plugins/wp/ProofScript.mli
index eb368c02225..7fe27cbb04d 100644
--- a/src/plugins/wp/ProofScript.mli
+++ b/src/plugins/wp/ProofScript.mli
@@ -35,6 +35,7 @@ and jtactic = {
tactic : string ;
params : Json.t ;
select : Json.t ;
+ strategy : string option ;
}
val is_prover : alternative -> bool
@@ -54,7 +55,7 @@ val has_proof : jscript -> bool
val decode : Json.t -> jscript
val encode : jscript -> Json.t
-val jtactic : tactical -> selection -> jtactic
+val jtactic : ?strategy:ProofStrategy.strategy -> tactical -> selection -> jtactic
val configure : jtactic -> sequent -> (tactical * selection) option
(** Json Codecs *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 12cd19f184c..4b246d88518 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -340,13 +340,13 @@ let rec crawl env on_child node = function
if ok then Env.validate env else Env.stuck env ;
Task.return ()
- | Error(msg,json) :: alternative ->
+ | Error(msg,json) :: alternatives ->
Wp_parameters.warning "@[<hov 2>Script Error: on goal %a@\n%S: %a@]@."
WpPropId.pretty (Env.goal env node).po_pid
msg Json.pp json ;
- crawl env on_child node alternative
+ crawl env on_child node alternatives
- | Prover( prv , res ) :: alternative ->
+ | Prover( prv , res ) :: alternatives ->
begin
let task =
if Env.play env prv res then
@@ -357,12 +357,12 @@ let rec crawl env on_child node = function
let continue ok =
if ok
then (Env.validate env ; Task.return ())
- else crawl env on_child node alternative
+ else crawl env on_child node alternatives
in
task >>= continue
end
- | Tactic( _ , jtactic , subscripts ) :: alternative ->
+ | Tactic( _ , jtactic , subscripts ) :: alternatives ->
begin
try
let residual = apply env node jtactic subscripts in
@@ -383,7 +383,12 @@ let rec crawl env on_child node = function
(Printexc.to_string exn)
Json.pp jtactic.params
Json.pp jtactic.select ;
- crawl env on_child node alternative
+ match jtactic.strategy with
+ | None -> crawl env on_child node alternatives
+ | Some s ->
+ (*TODO TRY STRATEGY FIRST *)
+ ignore s ;
+ crawl env on_child node alternatives
end
(* -------------------------------------------------------------------------- *)
--
GitLab