From 50db185796c2078e827c1db5deafe2dba62f501d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 10 Apr 2024 12:52:54 +0200
Subject: [PATCH] [wp] fix fallback in scripts
---
src/plugins/wp/ProofScript.ml | 8 ++++----
src/plugins/wp/VCS.ml | 16 ++++++++++++----
src/plugins/wp/VCS.mli | 5 +++++
src/plugins/wp/Why3Provers.ml | 26 +++++++++++++++++++++-----
src/plugins/wp/Why3Provers.mli | 2 +-
5 files changed, 43 insertions(+), 14 deletions(-)
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index da270ebd1d8..a6db6ea1b03 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -358,8 +358,9 @@ let json_of_result (p : VCS.prover) (r : VCS.result) =
`Assoc (name :: verdict :: (time @ steps))
let prover_of_json js =
- try VCS.parse_prover (js >? "prover" |> Json.string)
- with Not_found -> None
+ match js >? "prover" |> Json.string with
+ | exception Not_found -> None
+ | pname -> VCS.prover_of_name ~fallback:true pname
let result_of_json js =
let verdict = try js >? "verdict" |> verdict_of_json with _ -> VCS.NoResult in
@@ -417,8 +418,7 @@ and alternative js =
| Some prover -> Prover(prover,result_of_json js)
| None ->
match tactic_of_json js with
- | Some(tactic, children) ->
- a_tactic tactic (List.map subscript children)
+ | Some(tactic, children) -> a_tactic tactic (List.map subscript children)
| None -> Error("Invalid Tactic",js)
let rec encode script = `List (alternatives script)
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index fb2766c4ac9..265f0d4c0a8 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -49,8 +49,9 @@ let parse_prover = function
| name ->
match Why3Provers.lookup name with
| Some p -> Some (Why3 p)
- | None -> Wp_parameters.error ~once:true
- "Prover '%s' not found in why3.conf" name ; None
+ | None ->
+ Wp_parameters.error ~once:true
+ "Prover '%s' not found in why3.conf" name ; None
let parse_mode m =
match String.lowercase_ascii m with
@@ -61,14 +62,21 @@ let parse_mode m =
| "fixup" -> FixUpdate
| _ ->
Wp_parameters.error ~once:true
- "Unrecognized mode %S (use 'batch' instead)" m ;
- Batch
+ "Unrecognized mode %S (use 'batch' instead)" m ; Batch
let name_of_prover = function
| Why3 s -> Why3Provers.ident_wp s
| Qed -> "qed"
| Tactical -> "script"
+let prover_of_name ?fallback = function
+ | "qed" -> Some Qed
+ | "script" -> Some Tactical
+ | name ->
+ match Why3Provers.lookup ?fallback name with
+ | None -> None
+ | Some prv -> Some (Why3 prv)
+
let title_of_prover ?version = function
| Why3 s ->
let version = match version with Some v -> v | None ->
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 6f9c67f88d0..4a737a298f3 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -50,8 +50,13 @@ val filename_for_prover : prover -> string
val title_of_mode : mode -> string
val parse_mode : string -> mode
+
+(** For the command line *)
val parse_prover : string -> prover option
+(** For scripts *)
+val prover_of_name : ?fallback:bool -> string -> prover option
+
val pp_prover : Format.formatter -> prover -> unit
val pp_mode : Format.formatter -> mode -> unit
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index f84d4b764a1..276f4890834 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -134,12 +134,28 @@ let filter ~name ?version (p:t) =
String.lowercase_ascii p.prover_name = name &&
match version with None -> true | Some v -> p.prover_version = v
-let select name =
+let select ~name ?version () =
+ match
+ List.sort by_version @@ List.filter (filter ~name ?version) @@ provers ()
+ with p::_ -> Some p | [] -> None
+
+let lookup ?(fallback=false) name =
match String.split_on_char ':' @@ String.lowercase_ascii name with
- | [name;version] -> List.filter (filter ~name ~version) @@ provers ()
- | [name] -> List.sort by_version @@ List.filter (filter ~name) @@ provers ()
- | _ -> []
-let lookup name = match select name with p :: _ -> Some p | [] -> None
+ | [name] -> select ~name ()
+ | [name;version] ->
+ begin
+ match select ~name ~version () with
+ | Some _ as res -> res
+ | None ->
+ if fallback then
+ match select ~name () with
+ | None -> None
+ | Some p as res ->
+ Wp_parameters.warning ~once:true
+ "Prover %s not found, fallback to %s" name (ident_wp p) ; res
+ else None
+ end
+ | _ -> None
(* -------------------------------------------------------------------------- *)
(* --- Models --- *)
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 11e189d5799..58fa30bd287 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -35,7 +35,7 @@ val version : t -> string
val altern : t -> string
val compare : t -> t -> int
-val lookup : string -> t option
+val lookup : ?fallback:bool -> string -> t option
val provers : unit -> t list
val provers_set : unit -> Why3.Whyconf.Sprover.t
val is_auto : t -> bool
--
GitLab