From aa590968cbe50cac72fa14b7992bfa6f80fada84 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 12 Jan 2022 15:08:26 +0100
Subject: [PATCH] [WP] adds comments in the tactics dedicated to sequences
---
src/plugins/wp/TacSequence.ml | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/src/plugins/wp/TacSequence.ml b/src/plugins/wp/TacSequence.ml
index 3671cd67b73..83ef006f631 100644
--- a/src/plugins/wp/TacSequence.ml
+++ b/src/plugins/wp/TacSequence.ml
@@ -63,12 +63,16 @@ class sequence =
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
Tactical.rewrite ?at [
@@ -76,6 +80,8 @@ class sequence =
"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
Tactical.rewrite ?at [
--
GitLab