[wp] fix fallback in scripts

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)

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 ->

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
 

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                                                             --- *)

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