From 6617613f93e70df2e2b964f380652ea43e2bb2a5 Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Sat, 3 Apr 2021 16:48:08 +0200
Subject: psl: prefix of goto/non-consecutive repetition is a bool.  Fix #1708

---
 src/psl/psl-nodes.ads      | 15 +++++++++++----
 src/psl/psl-nodes_meta.adb | 10 +++++-----
 src/psl/psl-rewrites.adb   | 22 +++++++++++-----------
 3 files changed, 27 insertions(+), 20 deletions(-)

(limited to 'src/psl')

diff --git a/src/psl/psl-nodes.ads b/src/psl/psl-nodes.ads
index 93ecd20f5..07d4f7df6 100644
--- a/src/psl/psl-nodes.ads
+++ b/src/psl/psl-nodes.ads
@@ -81,8 +81,8 @@ package PSL.Nodes is
 
       N_Star_Repeat_Seq,
       N_Goto_Repeat_Seq,
-      N_Plus_Repeat_Seq, -- [+]
-      N_Equal_Repeat_Seq,
+      N_Plus_Repeat_Seq,   -- [+]
+      N_Equal_Repeat_Seq,  -- [= ]
 
       --  Boolean layer.
       N_Paren_Bool,
@@ -276,8 +276,6 @@ package PSL.Nodes is
    --   Get/Set_Right (Field2)
 
    -- N_Star_Repeat_Seq (Short)
-   -- N_Goto_Repeat_Seq (Short)
-   -- N_Equal_Repeat_Seq (Short)
    --
    --  Note: can be null_node for star_repeat_seq.
    --   Get/Set_Sequence (Field3)
@@ -286,6 +284,15 @@ package PSL.Nodes is
    --
    --   Get/Set_High_Bound (Field2)
 
+   -- N_Equal_Repeat_Seq (Short)
+   -- N_Goto_Repeat_Seq (Short)
+   --
+   --   Get/Set_Boolean (Field3)
+   --
+   --   Get/Set_Low_Bound (Field1)
+   --
+   --   Get/Set_High_Bound (Field2)
+
    -- N_Plus_Repeat_Seq (Short)
    --
    --  Note: can be null_node.
diff --git a/src/psl/psl-nodes_meta.adb b/src/psl/psl-nodes_meta.adb
index 4d229b5cd..8486c177f 100644
--- a/src/psl/psl-nodes_meta.adb
+++ b/src/psl/psl-nodes_meta.adb
@@ -510,13 +510,13 @@ package body PSL.Nodes_Meta is
       Field_Low_Bound,
       Field_High_Bound,
       --  N_Goto_Repeat_Seq
-      Field_Sequence,
+      Field_Boolean,
       Field_Low_Bound,
       Field_High_Bound,
       --  N_Plus_Repeat_Seq
       Field_Sequence,
       --  N_Equal_Repeat_Seq
-      Field_Sequence,
+      Field_Boolean,
       Field_Low_Bound,
       Field_High_Bound,
       --  N_Paren_Bool
@@ -1130,9 +1130,7 @@ package body PSL.Nodes_Meta is
            | N_Imp_Seq
            | N_Overlap_Imp_Seq
            | N_Star_Repeat_Seq
-           | N_Goto_Repeat_Seq
-           | N_Plus_Repeat_Seq
-           | N_Equal_Repeat_Seq =>
+           | N_Plus_Repeat_Seq =>
             return True;
          when others =>
             return False;
@@ -1224,6 +1222,8 @@ package body PSL.Nodes_Meta is
            | N_Next_Event_E
            | N_Abort
            | N_Clocked_SERE
+           | N_Goto_Repeat_Seq
+           | N_Equal_Repeat_Seq
            | N_Paren_Bool
            | N_Not_Bool =>
             return True;
diff --git a/src/psl/psl-rewrites.adb b/src/psl/psl-rewrites.adb
index be9477088..7568ab8fc 100644
--- a/src/psl/psl-rewrites.adb
+++ b/src/psl/psl-rewrites.adb
@@ -188,12 +188,12 @@ package body PSL.Rewrites is
       end if;
    end Rewrite_Star_Repeat_Seq;
 
-   function Rewrite_Goto_Repeat_Seq (Seq : Node;
-                                     Lo, Hi : Node) return Node is
+   function Rewrite_Goto_Repeat_Seq (B : Node; Lo, Hi : Node) return Node
+   is
       Res : Node;
    begin
       --  b[->]  -->  {(~b)[*];b}
-      Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq);
+      Res := Build_Concat (Build_Star (Build_Bool_Not (B)), B);
 
       if Lo = Null_Node then
          return Res;
@@ -203,12 +203,12 @@ package body PSL.Rewrites is
       return Rewrite_Star_Repeat_Seq (Res, Lo, Hi);
    end Rewrite_Goto_Repeat_Seq;
 
-   function Rewrite_Goto_Repeat_Seq (Seq : Node;
-                                     Lo, Hi : Uns32) return Node is
+   function Rewrite_Goto_Repeat_Seq (B : Node; Lo, Hi : Uns32) return Node
+   is
       Res : Node;
    begin
       --  b[->]  -->  {(~b)[*];b}
-      Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq);
+      Res := Build_Concat (Build_Star (Build_Bool_Not (B)), B);
 
       --  b[->l:h]  -->  {b[->]}[*l:h]
       return Rewrite_Star_Repeat_Seq (Res, Lo, Hi);
@@ -216,13 +216,13 @@ package body PSL.Rewrites is
 
    function Rewrite_Equal_Repeat_Seq (N : Node) return Node
    is
-      Seq : constant Node := Get_Sequence (N);
+      B : constant Node := Get_Boolean (N);
       Lo : constant Node := Get_Low_Bound (N);
       Hi : constant Node := Get_High_Bound (N);
    begin
       --  b[=l:h]  -->  {b[->l:h]};(~b)[*]
-      return Build_Concat (Rewrite_Goto_Repeat_Seq (Seq, Lo, Hi),
-                           Build_Star (Build_Bool_Not (Seq)));
+      return Build_Concat (Rewrite_Goto_Repeat_Seq (B, Lo, Hi),
+                           Build_Star (Build_Bool_Not (B)));
    end Rewrite_Equal_Repeat_Seq;
 
    function Rewrite_Within (N : Node) return Node is
@@ -291,10 +291,10 @@ package body PSL.Rewrites is
             return N;
          when N_Goto_Repeat_Seq =>
             return Rewrite_Goto_Repeat_Seq
-              (Rewrite_SERE (Get_Sequence (N)),
+              (Rewrite_SERE (Get_Boolean (N)),
                Get_Low_Bound (N), Get_High_Bound (N));
          when N_Equal_Repeat_Seq =>
-            Set_Sequence (N, Rewrite_SERE (Get_Sequence (N)));
+            Set_Boolean (N, Rewrite_SERE (Get_Boolean (N)));
             return Rewrite_Equal_Repeat_Seq (N);
          when N_Braced_SERE =>
             return Rewrite_SERE (Get_SERE (N));
-- 
cgit v1.2.3