From 5400738a60c0b93eb2c5c21c69cf955e0cd8e849 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 22 Aug 2019 18:03:57 +0200
Subject: [PATCH] [wp] rename prover-why3
---
headers/header_spec.txt | 4 ++--
src/plugins/wp/Makefile.in | 2 +-
src/plugins/wp/{why3_api.ml => ProverWhy3.ml} | 2 +-
src/plugins/wp/{why3_api.mli => ProverWhy3.mli} | 0
src/plugins/wp/prover.ml | 13 +++++--------
src/plugins/wp/register.ml | 2 +-
6 files changed, 10 insertions(+), 13 deletions(-)
rename src/plugins/wp/{why3_api.ml => ProverWhy3.ml} (99%)
rename src/plugins/wp/{why3_api.mli => ProverWhy3.mli} (100%)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 0090e3b22d8..42a5e04927a 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1442,6 +1442,8 @@ src/plugins/wp/ProverSearch.ml: CEA_WP
src/plugins/wp/ProverSearch.mli: CEA_WP
src/plugins/wp/ProverTask.ml: CEA_WP
src/plugins/wp/ProverTask.mli: CEA_WP
+src/plugins/wp/ProverWhy3.mli: CEA_WP
+src/plugins/wp/ProverWhy3.ml: CEA_WP
src/plugins/wp/REVISION: .ignore
src/plugins/wp/RefUsage.ml: CEA_WP
src/plugins/wp/RefUsage.mli: CEA_WP
@@ -1525,8 +1527,6 @@ src/plugins/wp/ctypes.ml: CEA_WP
src/plugins/wp/ctypes.mli: CEA_WP
src/plugins/wp/filter_axioms.ml: CEA_WP
src/plugins/wp/filter_axioms.mli: CEA_WP
-src/plugins/wp/why3_api.mli: CEA_WP
-src/plugins/wp/why3_api.ml: CEA_WP
src/plugins/wp/doc/MakeDoc: .ignore
src/plugins/wp/doc/coqdoc/Makefile: .ignore
src/plugins/wp/doc/coqdoc/coqdoc.sty: .ignore
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 900a4581d63..cc19d6ae68d 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -88,7 +88,7 @@ PLUGIN_CMO:= \
TacCongruence TacOverflow Auto \
ProofSession ProofScript ProofEngine \
ProverTask ProverErgo ProverCoq \
- filter_axioms why3_api \
+ filter_axioms ProverWhy3 \
driver prover ProverSearch ProverScript \
Generator Factory \
calculus cfgDump cfgWP \
diff --git a/src/plugins/wp/why3_api.ml b/src/plugins/wp/ProverWhy3.ml
similarity index 99%
rename from src/plugins/wp/why3_api.ml
rename to src/plugins/wp/ProverWhy3.ml
index 1d4c70adb63..83e0c580858 100644
--- a/src/plugins/wp/why3_api.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -608,7 +608,7 @@ module CLUSTERS = Model.Index
(struct
type key = Definitions.cluster
type data = int * Why3.Theory.theory
- let name = "Why3_api.CLUSTERS"
+ let name = "ProverWhy3.CLUSTERS"
let compare = Definitions.cluster_compare
let pretty = Definitions.pp_cluster
end)
diff --git a/src/plugins/wp/why3_api.mli b/src/plugins/wp/ProverWhy3.mli
similarity index 100%
rename from src/plugins/wp/why3_api.mli
rename to src/plugins/wp/ProverWhy3.mli
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index 245225db0d9..85b63a14b2b 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -30,18 +30,15 @@ open Task
open Wpo
let dispatch ?(config=VCS.default) mode prover wpo =
- let why3 prover =
- Why3_api.prove
- ~timeout:(VCS.get_timeout config)
- ~steplimit:(VCS.get_stepout config)
- ~prover wpo
- in
begin
match prover with
- | Why3 prover -> why3 prover
+ | Qed | Tactical -> Task.return VCS.no_result
| NativeAltErgo -> ProverErgo.prove ~config ~mode wpo
| NativeCoq -> ProverCoq.prove mode wpo
- | Qed | Tactical -> Task.return VCS.no_result
+ | Why3 prover -> ProverWhy3.prove
+ ~timeout:(VCS.get_timeout config)
+ ~steplimit:(VCS.get_stepout config)
+ ~prover wpo
end
let started ?start wpo =
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 04fc43af94d..2a4a6c5f31c 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -837,7 +837,7 @@ let () = Cmdline.run_after_setting_files
if Wp_parameters.has_dkey dkey_shell then
Log.print_on_output pp_wp_parameters)
-let () = Cmdline.run_after_configuring_stage Why3_api.parse_why3_options
+let () = Cmdline.run_after_configuring_stage ProverWhy3.parse_why3_options
let do_prover_detect () =
if not !Config.is_gui && Wp_parameters.Detect.get () then
--
GitLab