From ca7f9200521590ecaf500a486673b83b2bc6ba51 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 24 Apr 2019 12:53:36 +0200
Subject: [PATCH] [wp] refactor why3 dp
---
src/plugins/wp/ProverDetect.None.ml | 9 +---
src/plugins/wp/ProverDetect.Why3.ml | 9 +---
src/plugins/wp/ProverDetect.mli | 9 +---
src/plugins/wp/ProverWhy3.ml | 72 +----------------------------
src/plugins/wp/ProverWhy3.mli | 19 ++------
src/plugins/wp/VCS.ml | 31 +++++++++++++
src/plugins/wp/VCS.mli | 24 ++++++++--
src/plugins/wp/register.ml | 18 ++------
8 files changed, 62 insertions(+), 129 deletions(-)
diff --git a/src/plugins/wp/ProverDetect.None.ml b/src/plugins/wp/ProverDetect.None.ml
index 771dbba1b78..6520404f80c 100644
--- a/src/plugins/wp/ProverDetect.None.ml
+++ b/src/plugins/wp/ProverDetect.None.ml
@@ -26,13 +26,6 @@
(* --- Prover Detection (no why3) --- *)
(* -------------------------------------------------------------------------- *)
-type dp = {
- dp_name : string ;
- dp_version : string ;
- dp_altern : string ;
- dp_shortcuts : string list ;
-}
-
-let detect () = []
+let detect () : VCS.dp list = []
(**************************************************************************)
diff --git a/src/plugins/wp/ProverDetect.Why3.ml b/src/plugins/wp/ProverDetect.Why3.ml
index ff6b33c6495..c2b6d1ac564 100644
--- a/src/plugins/wp/ProverDetect.Why3.ml
+++ b/src/plugins/wp/ProverDetect.Why3.ml
@@ -26,13 +26,6 @@
(* --- Why3 Prover Detection --- *)
(* -------------------------------------------------------------------------- *)
-type dp = {
- dp_name : string ;
- dp_version : string ;
- dp_altern : string ;
- dp_shortcuts : string list ;
-}
-
open Why3
open Wstdlib
open Whyconf
@@ -49,7 +42,7 @@ let detect () =
let dps =
Mprover.fold
(fun dp keys dps ->
- {
+ VCS.{
dp_name = dp.prover_name ;
dp_version = dp.prover_version ;
dp_altern = dp.prover_altern ;
diff --git a/src/plugins/wp/ProverDetect.mli b/src/plugins/wp/ProverDetect.mli
index 14630cc1e6e..7a2cba28ff0 100644
--- a/src/plugins/wp/ProverDetect.mli
+++ b/src/plugins/wp/ProverDetect.mli
@@ -24,13 +24,6 @@
(** Why3 Prover Detection *)
(* -------------------------------------------------------------------------- *)
-type dp = {
- dp_name : string ;
- dp_version : string ;
- dp_altern : string ;
- dp_shortcuts : string list ;
-}
-
-val detect : unit -> dp list
+val detect : unit -> VCS.dp list
(**************************************************************************)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index a40c44aecb8..38e73ded32b 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -612,74 +612,4 @@ let prove_prop ~timeout ~prover ~wpo =
let prove ?timeout ~prover wpo =
Task.todo (fun () -> prove_prop ~timeout ~wpo ~prover)
-(* -------------------------------------------------------------------------- *)
-(* --- Why3-Config --- *)
-(* -------------------------------------------------------------------------- *)
-
-type dp = {
- dp_name : string ;
- dp_version : string ;
- dp_prover : string ;
-}
-
-let prover dp = Why3 dp.dp_prover
-
-let find name dps =
- try List.find (fun d -> d.dp_prover = name) dps
- with Not_found ->
- let name = Transitioning.String.lowercase_ascii name in
- try
- List.find
- (fun d -> Transitioning.String.lowercase_ascii d.dp_name = name) dps
- with Not_found ->
- { dp_prover = name ; dp_name = name ; dp_version = "default" }
-
-let parse spec =
- try
- let k = String.index spec ':' in
- let dp_name = String.sub spec 0 k in
- let dp_version = String.sub spec (succ k) (String.length spec - k - 1)
- |> String.map (fun c -> if c =':' then ' ' else c) in
- { dp_prover = spec ; dp_name ; dp_version }
- with Not_found ->
- { dp_prover = spec ; dp_name = spec ; dp_version = "default" }
-
-let pe_prover = Str.regexp "\\([^ ]+\\) (\\([^)]+\\))"
-
-class why3detect job =
- object(why)
-
- inherit ProverTask.command "why3"
-
- val mutable dps = []
-
- method result st =
- job (if st = 0 then Some (List.rev dps) else None)
-
- method prover p =
- begin
- let dp_name = p#get_string 1 in
- let dp_version = p#get_string 2 in
- Wp_parameters.debug ~level:1
- "Prover %S, version %s detected." dp_name dp_version ;
- let dp_prover = Printf.sprintf "%s:%s" dp_name dp_version
- |> String.map
- (fun c -> if c = ' ' || c = ',' then ':' else c) in
- dps <- { dp_name ; dp_version ; dp_prover } :: dps
- end
-
- method detect : unit task =
- begin
- why#add [ "--list-provers" ] ;
- why#validate_pattern ~repeat:true ~logs:`OUT pe_prover why#prover ;
- why#run ~echo:true () >>= Task.call why#result
- end
-
- end
-
-let detect_why3 job =
- let task = (new why3detect job)#detect in
- Task.run (Task.thread task)
-
-let detect_provers job =
- detect_why3 (function None -> job [] | Some dps -> job dps)
+(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index bab64eec2e2..d6a9f5bc755 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -39,22 +39,7 @@ val assemble_goal: Wpo.t -> (string list (* includes *) * goal) option
val prove : ?timeout:int -> prover:string -> Wpo.t -> result task
(** The string must be a valid why3 prover identifier
- Return NoResult if it is already proved by Qed
-*)
-
-type dp = {
- dp_name : string ;
- dp_version : string ;
- dp_prover : string ;
-}
-
-val prover : dp -> prover
-
-val detect_why3 : (dp list option -> unit) -> unit
-val detect_provers : (dp list -> unit) -> unit
-
-val find : string -> dp list -> dp
-val parse : string -> dp
+ Return NoResult if it is already proved by Qed *)
(* -------------------------------------------------------------------------- *)
(* --- Why3 Multi-Theorem Prover --- *)
@@ -66,3 +51,5 @@ sig
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index f1b22877570..37fea1aa59e 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -170,6 +170,37 @@ module P = struct type t = prover let compare = cmp_prover end
module Pset = Set.Make(P)
module Pmap = Map.Make(P)
+(* -------------------------------------------------------------------------- *)
+(* --- Why3 Provers --- *)
+(* -------------------------------------------------------------------------- *)
+
+type dp = {
+ dp_name : string ;
+ dp_version : string ;
+ dp_altern : string ;
+ dp_shortcuts : string list ;
+}
+
+let pp_altern fmt a = if a<>"" then Format.fprintf fmt " (%s)" a
+
+let pp_shortcut fmt = function
+ | ("alt-ergo" | "coq" | "tip" | "script") as p ->
+ Format.fprintf fmt "why3:%s" p
+ | p -> Format.pp_print_string fmt p
+
+let pp_shortcuts =
+ Pretty_utils.pp_list ~pre:"[" ~sep:"," ~suf:"]" ~empty:"(disabled)"
+ pp_shortcut
+
+let pretty fmt dp =
+ Format.fprintf fmt "%s %s%a"
+ dp.dp_name dp.dp_version
+ pp_altern dp.dp_altern
+
+let prover_of_dp = function
+ | { dp_shortcuts = key::_ } -> Why3 key
+ | _ -> Why3 "none"
+
(* -------------------------------------------------------------------------- *)
(* --- Config --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 9357b0bcc94..7d9eb27c8d2 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -44,10 +44,6 @@ type language =
| L_coq
| L_altergo
-(* -------------------------------------------------------------------------- *)
-(* --- Prover Names --- *)
-(* -------------------------------------------------------------------------- *)
-
module Pset : Set.S with type elt = prover
module Pmap : Map.S with type key = prover
@@ -66,9 +62,29 @@ val pp_mode : Format.formatter -> mode -> unit
val cmp_prover : prover -> prover -> int
+(* -------------------------------------------------------------------------- *)
+(** {2 Why3 Provers} *)
+(* -------------------------------------------------------------------------- *)
+
+type dp = {
+ dp_name : string ;
+ dp_version : string ;
+ dp_altern : string ;
+ dp_shortcuts : string list ;
+}
+
+val prover_of_dp : dp -> prover
+
+(** Without shortcuts *)
+val pretty : Format.formatter -> dp -> unit
+val pp_shortcut : Format.formatter -> string -> unit
+val pp_shortcuts : Format.formatter -> string list -> unit
+
+(* -------------------------------------------------------------------------- *)
(** {2 Config}
[None] means current WP option default.
[Some 0] means prover default. *)
+(* -------------------------------------------------------------------------- *)
type config = {
valid : bool ;
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index e447b0ed84c..ad824c977d6 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -846,21 +846,11 @@ let do_prover_detect () =
begin
let open ProverDetect in
let dps = detect () in
- let pp_altern fmt a = if a<>"" then Format.fprintf fmt " (%s)" a in
- let pp_shortcut fmt = function
- | ("alt-ergo" | "coq" | "tip" | "script") as p ->
- Format.fprintf fmt "why3:%s" p
- | p -> Format.pp_print_string fmt p in
- let pp_shortcuts =
- Pretty_utils.pp_list ~pre:"[" ~sep:"," ~suf:"]" ~empty:"(disabled)"
- pp_shortcut in
- let pp_prover fmt dp =
- Format.fprintf fmt "%s %s%a %a"
- dp.dp_name dp.dp_version
- pp_altern dp.dp_altern
- pp_shortcuts dp.dp_shortcuts in
let pp_provers fmt dps =
- List.iter (Format.fprintf fmt "@\n - %a" pp_prover) dps in
+ List.iter (fun dp ->
+ Format.fprintf fmt "@\n - %a %a"
+ VCS.pretty dp VCS.pp_shortcuts dp.VCS.dp_shortcuts
+ ) dps in
if dps = [] then
Wp_parameters.result "No Why3 provers detected."
else
--
GitLab