From 0022105b213560b2183720f51de7c36e3ef96945 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 27 Mar 2023 10:06:57 +0200
Subject: [PATCH] [wp] -wp-auto fallback in strategies
---
src/plugins/wp/ProofStrategy.ml | 4 ++++
src/plugins/wp/doc/manual/wp_plugin.tex | 3 +++
2 files changed, 7 insertions(+)
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index fc7f9f6e8e3..47ca11e43a0 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -42,6 +42,7 @@ type strategy = {
and alternative =
| Strategy of string loc
| Provers of string loc list * float option (* timeout *)
+ | Auto of string loc list (* deprecated -wp-auto *)
| Tactic of {
tactic : string loc ;
select : value list ;
@@ -193,6 +194,9 @@ let parse_alternative ctxt p =
let tactic = parse_name ctxt ~kind:"tactic" p in
parse_tactic_params ctxt (Pattern.context ctxt) ~tactic
~select:[] ~lookup:[] ~params:[] ~children:[] ~default:None ps
+ | PLapp("\\auto",[],ps) ->
+ let strategies = List.map (parse_name ctxt ~kind:"auto") ps in
+ Auto strategies
| _ -> ctxt.error loc "Strategy definition expected (%a)" debug p
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 26d719a21dc..844e49f5c2f 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1686,6 +1686,7 @@ Strategy consists of list of alternatives with the following syntax:
\textit{alternative} $::=$ \\
\quad$|$\quad\verb+\prover+(\verb+"p"+\pdots\verb+"p"+, \textit{timeout}) \\
\quad$|$\quad\verb+\tactic+(\verb+"id"+, \textit{param}\pdots\textit{param}) \\
+ \quad$|$\quad\verb+\auto+(\verb+"id"+,\pdots\verb+"id"+) \\
\quad$|$\quad\verb+\default+ \\
\quad$|$\quad\textit{strategy}
\end{tabular}
@@ -1702,6 +1703,8 @@ Each form \emph{alternative} consists of one possible solution to discharge a pr
\item \verb+\tactic(id,prm...)+ will try to apply the specified tactic with the
associated parameters. Tactic parameters allows to select the target of the tactic,
and the strategy to be used on generated sub-goals.
+\item \verb+\auto(id,...)+ will try to apply the (deprecated) auto-strategies
+ available in \textsf{WP} versions prior to Cobalt.
\item \textit{name} or \verb$\default$ tries the specified strategy.
\end{itemize}
--
GitLab