[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

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