From 4d4140250f1e76afb6d46ecfce0c231b97766060 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 19 Jan 2022 11:31:45 +0100
Subject: [PATCH] [wp] Improve Sequence tactic feedback - disable tactic in Sum
mode when parameter in not a sum - set description according to selected
option
---
src/plugins/wp/TacSequence.ml | 67 ++++++++++++++++++++++-------------
1 file changed, 42 insertions(+), 25 deletions(-)
diff --git a/src/plugins/wp/TacSequence.ml b/src/plugins/wp/TacSequence.ml
index 83ef006f631..ab689630267 100644
--- a/src/plugins/wp/TacSequence.ml
+++ b/src/plugins/wp/TacSequence.ml
@@ -53,42 +53,59 @@ class sequence =
~descr:"Unroll repeat-sequence operator"
~params:[pmode]
- method select _feedback (s : Tactical.selection) =
+ method select feedback (s : Tactical.selection) =
let value = Tactical.selected s in
match F.repr value with
| Fun(f,[a;n]) when f == Vlist.f_repeat ->
let result = F.typeof value in
let at = Tactical.at s in
- Tactical.Applicable
- begin
- match self#get_field vmode with
- | `Sum ->
- (* n1>=0 && n2>=0 && ... |- (a *^ (n1 + n2 + ...)) -+-> ((a *^ n1) ^ (a *^ n2) ^ ...) *)
- let ns = sum n in
- (* NB. the term is rewriten in itself when the initial term is not a sum *)
- let pos = F.p_all positive ns in
- let cat = concat ~result (List.map (repeat ~result a) ns) in
- Tactical.condition "Positive" pos @@
- Tactical.rewrite ?at [ "Unroll" , pos , value , cat ]
- | `Left ->
- (* n<=0 |- (a *^ n) -+-> [] *)
- (* n-1>=0 |- (a *^ n) -+-> (a ^ (a *^ (n-1))) *)
- let p = F.e_add n F.e_minus_one in
- let unroll = concat ~result [a ; repeat ~result a p] in
+ begin
+ match self#get_field vmode with
+ | `Sum ->
+ (* n1>=0 && n2>=0 && ... |- (a *^ (n1 + n2 + ...)) -+-> ((a *^ n1) ^ (a *^ n2) ^ ...) *)
+ begin
+ match sum n with
+ | [ s ] ->
+ feedback#set_descr
+ "Cannot unroll with selected option, '%a' is not a sum"
+ F.pp_term s ;
+ Tactical.Not_configured
+ | ns ->
+ (* NB. the term is rewriten in itself when the initial term is not a sum *)
+ let pos = F.p_all positive ns in
+ let cat =
+ concat ~result (List.map (repeat ~result a) ns) in
+ feedback#set_descr
+ "Unroll repeat-sequence: unroll sum" ;
+ Tactical.Applicable (
+ Tactical.condition "Positive" pos @@
+ Tactical.rewrite ?at [ "Unroll" , pos , value , cat ])
+ end
+ | `Left ->
+ (* n<=0 |- (a *^ n) -+-> [] *)
+ (* n-1>=0 |- (a *^ n) -+-> (a ^ (a *^ (n-1))) *)
+ let p = F.e_add n F.e_minus_one in
+ let unroll = concat ~result [a ; repeat ~result a p] in
+ feedback#set_descr
+ "Unroll repeat-sequence: unroll first element" ;
+ Tactical.Applicable(
Tactical.rewrite ?at [
"Nil", negative n , value , concat ~result [] ;
"Unroll", positive p , value , unroll ;
- ]
- | `Right ->
- (* n<=0 |- (a *^ n) -+-> [] *)
- (* n-1>=0 |- (a *^ n) -+-> ((a *^ (n-1)) ^ a) *)
- let p = F.e_add n F.e_minus_one in
- let unroll = concat ~result [repeat ~result a p ; a] in
+ ])
+ | `Right ->
+ (* n<=0 |- (a *^ n) -+-> [] *)
+ (* n-1>=0 |- (a *^ n) -+-> ((a *^ (n-1)) ^ a) *)
+ let p = F.e_add n F.e_minus_one in
+ let unroll = concat ~result [repeat ~result a p ; a] in
+ feedback#set_descr
+ "Unroll repeat-sequence: unroll last element" ;
+ Tactical.Applicable(
Tactical.rewrite ?at [
"Nil", negative n , value , concat ~result [] ;
"Unroll", positive p , value , unroll ;
- ]
- end
+ ])
+ end
| _ -> Not_applicable
end
--
GitLab