1--  PSL - Simple subset
2--  Copyright (C) 2002-2016 Tristan Gingold
3--
4--  This program is free software: you can redistribute it and/or modify
5--  it under the terms of the GNU General Public License as published by
6--  the Free Software Foundation, either version 2 of the License, or
7--  (at your option) any later version.
8--
9--  This program is distributed in the hope that it will be useful,
10--  but WITHOUT ANY WARRANTY; without even the implied warranty of
11--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12--  GNU General Public License for more details.
13--
14--  You should have received a copy of the GNU General Public License
15--  along with this program.  If not, see <gnu.org/licenses>.
16
17with PSL.Types; use PSL.Types;
18with PSL.Errors; use PSL.Errors;
19
20package body PSL.Subsets is
21   procedure Check_Simple (N : Node)
22   is
23   begin
24      case Get_Kind (N) is
25         when N_Not_Bool =>
26            if Get_Psl_Type (Get_Boolean (N)) /= Type_Boolean then
27               Error_Msg_Sem
28                 ("operand of a negation operator must be a boolean", N);
29            end if;
30         when N_Never =>
31            case Get_Psl_Type (Get_Property (N)) is
32               when Type_Sequence | Type_Boolean =>
33                  null;
34               when others =>
35                  Error_Msg_Sem ("operand of a 'never' operator must be "
36                                   & "a boolean or a sequence", N);
37            end case;
38         when N_Eventually =>
39            case Get_Psl_Type (Get_Property (N)) is
40               when Type_Sequence | Type_Boolean =>
41                  null;
42               when others =>
43                  Error_Msg_Sem ("operand of an 'eventually!' operator must be"
44                                   & " a boolean or a sequence", N);
45            end case;
46         when N_And_Bool =>
47            if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then
48               Error_Msg_Sem ("left-hand side operand of logical 'and' must be"
49                                & " a boolean", N);
50            end if;
51         when N_Or_Bool =>
52            if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then
53               Error_Msg_Sem ("left-hand side operand of logical 'or' must be"
54                                & " a boolean", N);
55            end if;
56         when N_Log_Imp_Prop =>
57            if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then
58               Error_Msg_Sem ("left-hand side operand of logical '->' must be"
59                                & " a boolean", N);
60            end if;
61            --  FIXME: <->
62         when N_Until =>
63            if not Get_Inclusive_Flag (N) then
64               if Get_Psl_Type (Get_Right (N)) /= Type_Boolean then
65                  Error_Msg_Sem ("right-hand side of a non-overlapping "
66                                   & "'until*' operator must be a boolean", N);
67               end if;
68            else
69               if Get_Psl_Type (Get_Right (N)) /= Type_Boolean
70                 or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean
71               then
72                  Error_Msg_Sem ("both operands of an overlapping 'until*'"
73                                   & " operator are boolean", N);
74               end if;
75            end if;
76         when N_Before =>
77            if Get_Psl_Type (Get_Right (N)) /= Type_Boolean
78              or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean
79            then
80               Error_Msg_Sem ("both operands of a 'before*'"
81                                & " operator are boolean", N);
82            end if;
83         when others =>
84            null;
85      end case;
86
87      --  Recursion.
88      case Get_Kind (N) is
89         when N_Error =>
90            null;
91         when N_Hdl_Mod_Name =>
92            null;
93         when N_Vunit
94            | N_Vmode
95            | N_Vprop =>
96            declare
97               Item : Node;
98            begin
99               Item := Get_Item_Chain (N);
100               while Item /= Null_Node loop
101                  Check_Simple (Item);
102                  Item := Get_Chain (Item);
103               end loop;
104            end;
105         when N_Name_Decl =>
106            null;
107         when N_Assert_Directive
108            | N_Property_Declaration =>
109            Check_Simple (Get_Property (N));
110         when N_Endpoint_Declaration
111            | N_Sequence_Declaration =>
112            Check_Simple (Get_Sequence (N));
113         when N_Clock_Event =>
114            Check_Simple (Get_Property (N));
115            Check_Simple (Get_Boolean (N));
116         when N_Always
117            | N_Never
118            | N_Eventually
119            | N_Strong =>
120            Check_Simple (Get_Property (N));
121         when N_Braced_SERE
122            | N_Clocked_SERE =>
123            Check_Simple (Get_SERE (N));
124         when N_Concat_SERE
125            | N_Fusion_SERE
126            | N_Within_SERE =>
127            Check_Simple (Get_Left (N));
128            Check_Simple (Get_Right (N));
129         when N_Name =>
130            null;
131         when N_Star_Repeat_Seq
132            | N_Goto_Repeat_Seq
133            | N_Equal_Repeat_Seq =>
134            declare
135               N2 : constant Node := Get_Sequence (N);
136            begin
137               if N2 /= Null_Node then
138                  Check_Simple (N2);
139               end if;
140            end;
141         when N_Plus_Repeat_Seq =>
142            Check_Simple (Get_Sequence (N));
143         when N_Match_And_Seq
144            | N_And_Seq
145            | N_Or_Seq =>
146            Check_Simple (Get_Left (N));
147            Check_Simple (Get_Right (N));
148         when N_Imp_Seq
149            | N_Overlap_Imp_Seq =>
150            Check_Simple (Get_Sequence (N));
151            Check_Simple (Get_Property (N));
152         when N_Log_Imp_Prop
153            | N_Log_Equiv_Prop
154            | N_Until
155            | N_Before
156            | N_Or_Prop
157            | N_And_Prop
158            | N_And_Bool
159            | N_Or_Bool
160            | N_Imp_Bool
161            | N_Equiv_Bool =>
162            Check_Simple (Get_Left (N));
163            Check_Simple (Get_Right (N));
164         when N_Next
165            | N_Next_A
166            | N_Next_E
167            | N_Paren_Prop =>
168            Check_Simple (Get_Property (N));
169         when N_Next_Event
170           | N_Next_Event_A
171           | N_Next_Event_E
172           | N_Abort =>
173            Check_Simple (Get_Boolean (N));
174            Check_Simple (Get_Property (N));
175         when N_Not_Bool
176           | N_Paren_Bool =>
177            Check_Simple (Get_Boolean (N));
178         when N_Const_Parameter
179           | N_Sequence_Parameter
180           | N_Boolean_Parameter
181           | N_Property_Parameter =>
182            null;
183         when N_Actual =>
184            null;
185         when N_Sequence_Instance
186           | N_Endpoint_Instance
187           | N_Property_Instance =>
188            null;
189         when N_True
190           | N_False
191           | N_Number
192           | N_EOS
193           | N_HDL_Expr
194           | N_HDL_Bool =>
195            null;
196      end case;
197   end Check_Simple;
198end PSL.Subsets;
199