PSL: handle inf in star repeat sequence. Fix #1832

9 files changed, 44 insertions, 11 deletions

diff --git a/src/psl/psl-nodes.adb b/src/psl/psl-nodes.adb
index 6d392150b..108dfe7b2 100644
--- a/src/psl/psl-nodes.adb
+++ b/src/psl/psl-nodes.adb
@@ -391,7 +391,8 @@ package body PSL.Nodes is
             | N_HDL_Bool =>
             return Type_Boolean;
          when N_Number
-            | N_Const_Parameter =>
+            | N_Const_Parameter
+            | N_Inf =>
             return Type_Numeric;
          when N_Vmode
             | N_Vunit
@@ -482,6 +483,7 @@ package body PSL.Nodes is
            | N_EOS
            | N_Name
            | N_Name_Decl
+           | N_Inf
            | N_Number =>
             return Format_Short;
       end case;
diff --git a/src/psl/psl-nodes.adb.in b/src/psl/psl-nodes.adb.in
index 3bbb26538..a644ebb71 100644
--- a/src/psl/psl-nodes.adb.in
+++ b/src/psl/psl-nodes.adb.in
@@ -391,7 +391,8 @@ package body PSL.Nodes is
             | N_HDL_Bool =>
             return Type_Boolean;
          when N_Number
-            | N_Const_Parameter =>
+            | N_Const_Parameter
+            | N_Inf =>
             return Type_Numeric;
          when N_Vmode
             | N_Vunit
diff --git a/src/psl/psl-nodes.ads b/src/psl/psl-nodes.ads
index 07d4f7df6..c92af81dc 100644
--- a/src/psl/psl-nodes.ads
+++ b/src/psl/psl-nodes.ads
@@ -99,6 +99,7 @@ package PSL.Nodes is
 
       N_Name,
       N_Name_Decl,
+      N_Inf,
       N_Number
      );
    for Nkind'Size use 8;
@@ -253,6 +254,8 @@ package PSL.Nodes is
    --
    --   Get/Set_Chain (Field2)
 
+   -- N_Inf (Short)
+
    -- N_Number (Short)
    --
    --   Get/Set_Value (Field1)
diff --git a/src/psl/psl-nodes_meta.adb b/src/psl/psl-nodes_meta.adb
index 8486c177f..92d18b735 100644
--- a/src/psl/psl-nodes_meta.adb
+++ b/src/psl/psl-nodes_meta.adb
@@ -258,6 +258,8 @@ package body PSL.Nodes_Meta is
             return "name";
          when N_Name_Decl =>
             return "name_decl";
+         when N_Inf =>
+            return "inf";
          when N_Number =>
             return "number";
       end case;
@@ -574,6 +576,7 @@ package body PSL.Nodes_Meta is
       --  N_Name_Decl
       Field_Identifier,
       Field_Chain,
+      --  N_Inf
       --  N_Number
       Field_Value
      );
@@ -643,6 +646,7 @@ package body PSL.Nodes_Meta is
       N_EOS => 169,
       N_Name => 171,
       N_Name_Decl => 173,
+      N_Inf => 173,
       N_Number => 174
      );
 
diff --git a/src/psl/psl-prints.adb b/src/psl/psl-prints.adb
index c9b343760..e1beb27c2 100644
--- a/src/psl/psl-prints.adb
+++ b/src/psl/psl-prints.adb
@@ -24,7 +24,8 @@ package body PSL.Prints is
    function Get_Priority (N : Node) return Priority is
    begin
       case Get_Kind (N) is
-         when N_Never | N_Always =>
+         when N_Never
+            | N_Always =>
             return Prio_FL_Invariance;
          when N_Eventually
            | N_Next
@@ -65,6 +66,7 @@ package body PSL.Prints is
             return Prio_Bool_Imp;
          when N_Name_Decl
            | N_Number
+           | N_Inf
            | N_True
            | N_False
            | N_EOS
@@ -149,6 +151,8 @@ package body PSL.Prints is
             begin
                Put (Str (2 .. Str'Last));
             end;
+         when N_Inf =>
+            Put ("inf");
          when N_Name_Decl =>
             Put (Image (Get_Identifier (N)));
          when N_HDL_Expr
diff --git a/src/psl/psl-rewrites.adb b/src/psl/psl-rewrites.adb
index 7568ab8fc..d8d9d5ecb 100644
--- a/src/psl/psl-rewrites.adb
+++ b/src/psl/psl-rewrites.adb
@@ -161,14 +161,20 @@ package body PSL.Rewrites is
       Cnt_Lo : Uns32;
       Cnt_Hi : Uns32;
    begin
-      if Lo = Null_Node then
-         --  r[*]
-         raise Program_Error;
-      end if;
+      --  r[*]  must have been handled.
+      pragma Assert (Lo /= Null_Node);
 
       Cnt_Lo := Get_Value (Lo);
       if Hi = Null_Node then
          Cnt_Hi := Cnt_Lo;
+      elsif Get_Kind (Hi) = N_Inf then
+         --  r[*N to inf]  -->  r[*N] ; r[*]
+         if Cnt_Lo = 0 then
+            return Build_Star (Seq);
+         else
+            return Build_Concat (Rewrite_Star_Repeat_Seq (Seq, Cnt_Lo, Cnt_Lo),
+                                 Build_Star (Seq));
+         end if;
       else
          Cnt_Hi := Get_Value (Hi);
       end if;
diff --git a/src/psl/psl-subsets.adb b/src/psl/psl-subsets.adb
index d5e3c1985..303d01c1e 100644
--- a/src/psl/psl-subsets.adb
+++ b/src/psl/psl-subsets.adb
@@ -188,6 +188,7 @@ package body PSL.Subsets is
          when N_True
            | N_False
            | N_Number
+           | N_Inf
            | N_EOS
            | N_HDL_Expr
            | N_HDL_Bool =>
diff --git a/src/vhdl/vhdl-parse_psl.adb b/src/vhdl/vhdl-parse_psl.adb
index 314249c14..808c2dae7 100644
--- a/src/vhdl/vhdl-parse_psl.adb
+++ b/src/vhdl/vhdl-parse_psl.adb
@@ -57,9 +57,9 @@ package body Vhdl.Parse_Psl is
          Scan;
          return Res;
       elsif Current_Token = Tok_Inf then
-         --  FIXME: create node
+         Res := Create_Node_Loc (N_Inf);
          Scan;
-         return Null_Node;
+         return Res;
       else
          Error_Msg_Parse ("number expected");
          return Null_Node;
@@ -68,9 +68,16 @@ package body Vhdl.Parse_Psl is
 
    procedure Check_Positive_Count (N : Node)
    is
-      Low  : constant Uns32 := Get_Value (Get_Low_Bound (N));
-      High : constant Uns32 := Get_Value (Get_High_Bound (N));
+      Low_B : constant Node := Get_Low_Bound (N);
+      High_B : constant Node := Get_High_Bound (N);
+      Low  : constant Uns32 := Get_Value (Low_B);
+      High : Uns32;
    begin
+      if Get_Kind (High_B) = N_Inf then
+         return;
+      end if;
+
+      High := Get_Value (High_B);
       if Low > High then
          Error_Msg_Parse
            ("Low bound of range must be lower than High bound," &
@@ -840,6 +847,7 @@ package body Vhdl.Parse_Psl is
             | N_False
             | N_True
             | N_Number
+            | N_Inf
             | N_Name_Decl
             | N_Name
             | N_EOS
diff --git a/src/vhdl/vhdl-prints.adb b/src/vhdl/vhdl-prints.adb
index 361cbe18b..ec4d870e5 100644
--- a/src/vhdl/vhdl-prints.adb
+++ b/src/vhdl/vhdl-prints.adb
@@ -1958,6 +1958,10 @@ package body Vhdl.Prints is
                Disp_Str (Ctxt, Str);
                Close_Lit (Ctxt);
             end;
+         when N_Inf =>
+            Start_Lit (Ctxt, Tok_Identifier);
+            Disp_Str (Ctxt, "INF");
+            Close_Lit (Ctxt);
          when N_Name_Decl =>
             Disp_Ident (Ctxt, Get_Identifier (N));
          when N_HDL_Expr