1--  PSL - Pretty print
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 Types; use Types;
18with PSL.Types; use PSL.Types;
19with PSL.Errors; use PSL.Errors;
20with Name_Table; use Name_Table;
21with Ada.Text_IO; use Ada.Text_IO;
22
23package body PSL.Prints is
24   function Get_Priority (N : Node) return Priority is
25   begin
26      case Get_Kind (N) is
27         when N_Never | N_Always =>
28            return Prio_FL_Invariance;
29         when N_Eventually
30           | N_Next
31           | N_Next_A
32           | N_Next_E
33           | N_Next_Event
34           | N_Next_Event_A
35           | N_Next_Event_E =>
36            return Prio_FL_Occurence;
37         when N_Braced_SERE =>
38            return Prio_SERE_Brace;
39         when N_Concat_SERE =>
40            return Prio_Seq_Concat;
41         when N_Fusion_SERE =>
42            return Prio_Seq_Fusion;
43         when N_Within_SERE =>
44            return Prio_Seq_Within;
45         when N_Match_And_Seq
46           | N_And_Seq =>
47            return Prio_Seq_And;
48         when N_Or_Seq =>
49            return Prio_Seq_Or;
50         when N_Until
51           | N_Before =>
52            return Prio_FL_Bounding;
53         when N_Abort =>
54            return Prio_FL_Abort;
55         when N_Or_Prop =>
56            return Prio_Seq_Or;
57         when N_And_Prop =>
58            return Prio_Seq_And;
59         when N_Paren_Prop =>
60            return Prio_FL_Paren;
61         when N_Imp_Seq
62           | N_Overlap_Imp_Seq
63           | N_Log_Imp_Prop
64           | N_Imp_Bool =>
65            return Prio_Bool_Imp;
66         when N_Name_Decl
67           | N_Number
68           | N_True
69           | N_False
70           | N_EOS
71           | N_HDL_Expr
72           | N_HDL_Bool
73           | N_Property_Instance
74           | N_Sequence_Instance =>
75            return Prio_HDL;
76         when N_Or_Bool =>
77            return Prio_Seq_Or;
78         when N_And_Bool =>
79            return Prio_Seq_And;
80         when N_Not_Bool =>
81            return Prio_Bool_Not;
82         when N_Star_Repeat_Seq
83           | N_Goto_Repeat_Seq
84           | N_Equal_Repeat_Seq
85           | N_Plus_Repeat_Seq =>
86            return Prio_SERE_Repeat;
87         when N_Strong =>
88            return Prio_Strong;
89         when others =>
90            Error_Kind ("get_priority", N);
91      end case;
92   end Get_Priority;
93
94   procedure Print_HDL_Expr (N : HDL_Node) is
95   begin
96      Put (Image (Get_Identifier (Node (N))));
97   end Print_HDL_Expr;
98
99   procedure Dump_Expr (N : Node)
100   is
101   begin
102      case Get_Kind (N) is
103         when N_HDL_Expr =>
104            if HDL_Expr_Printer = null then
105               Put ("Expr");
106            else
107               HDL_Expr_Printer.all (Get_HDL_Node (N));
108            end if;
109         when N_True =>
110            Put ("TRUE");
111         when N_False =>
112            Put ("FALSE");
113         when N_Not_Bool =>
114            Put ("!");
115            Dump_Expr (Get_Boolean (N));
116         when N_And_Bool =>
117            Put ("(");
118            Dump_Expr (Get_Left (N));
119            Put (" && ");
120            Dump_Expr (Get_Right (N));
121            Put (")");
122         when N_Or_Bool =>
123            Put ("(");
124            Dump_Expr (Get_Left (N));
125            Put (" || ");
126            Dump_Expr (Get_Right (N));
127            Put (")");
128         when others =>
129            PSL.Errors.Error_Kind ("dump_expr", N);
130      end case;
131   end Dump_Expr;
132
133   procedure Print_Expr (N : Node; Parent_Prio : Priority := Prio_Lowest)
134   is
135      Prio : Priority;
136   begin
137      if N = Null_Node then
138         Put (".");
139         return;
140      end if;
141      Prio := Get_Priority (N);
142      if Prio < Parent_Prio then
143         Put ("(");
144      end if;
145      case Get_Kind (N) is
146         when N_Number =>
147            declare
148               Str : constant String := Uns32'Image (Get_Value (N));
149            begin
150               Put (Str (2 .. Str'Last));
151            end;
152         when N_Name_Decl =>
153            Put (Image (Get_Identifier (N)));
154         when N_HDL_Expr
155           | N_HDL_Bool =>
156            if HDL_Expr_Printer = null then
157               Put ("HDL_Expr");
158            else
159               HDL_Expr_Printer.all (Get_HDL_Node (N));
160            end if;
161            --  FIXME: this is true only when using the scanner.
162            --  Print_Expr (Node (Get_HDL_Node (N)));
163         when N_True =>
164            Put ("TRUE");
165         when N_False =>
166            Put ("FALSE");
167         when N_EOS =>
168            Put ("EOS");
169         when N_Not_Bool =>
170            Put ("!");
171            Print_Expr (Get_Boolean (N), Prio);
172         when N_And_Bool =>
173            Print_Expr (Get_Left (N), Prio);
174            Put (" && ");
175            Print_Expr (Get_Right (N), Prio);
176         when N_Or_Bool =>
177            Print_Expr (Get_Left (N), Prio);
178            Put (" || ");
179            Print_Expr (Get_Right (N), Prio);
180         when N_Imp_Bool =>
181            Print_Expr (Get_Left (N), Prio);
182            Put (" -> ");
183            Print_Expr (Get_Right (N), Prio);
184         when others =>
185            Error_Kind ("print_expr", N);
186      end case;
187      if Prio < Parent_Prio then
188         Put (")");
189      end if;
190   end Print_Expr;
191
192   procedure Print_Count (N : Node) is
193      B : Node;
194   begin
195      B := Get_Low_Bound (N);
196      if B = Null_Node then
197         return;
198      end if;
199      Print_Expr (B);
200      B := Get_High_Bound (N);
201      if B = Null_Node then
202         return;
203      end if;
204      Put (":");
205      Print_Expr (B);
206   end Print_Count;
207
208   procedure Print_Binary_Sequence (Name : String; N : Node; Prio : Priority)
209   is
210   begin
211      Print_Sequence (Get_Left (N), Prio);
212      Put (Name);
213      Print_Sequence (Get_Right (N), Prio);
214   end Print_Binary_Sequence;
215
216   procedure Print_Repeat_Sequence (Name : String; N : Node) is
217      S : Node;
218   begin
219      S := Get_Sequence (N);
220      if S /= Null_Node then
221         Print_Sequence (S, Prio_SERE_Repeat);
222      end if;
223      Put (Name);
224      Print_Count (N);
225      Put ("]");
226   end Print_Repeat_Sequence;
227
228   procedure Print_Sequence (Seq : Node; Parent_Prio : Priority := Prio_Lowest)
229   is
230      Prio : constant Priority := Get_Priority (Seq);
231      Add_Paren : constant Boolean := Prio < Parent_Prio
232        or else Parent_Prio <= Prio_FL_Paren;
233   begin
234      if Add_Paren then
235         Put ("{");
236      end if;
237      case Get_Kind (Seq) is
238         when N_Braced_SERE =>
239            Put ("{");
240            Print_Sequence (Get_SERE (Seq), Prio_Lowest);
241            Put ("}");
242         when N_Concat_SERE =>
243            Print_Binary_Sequence (";", Seq, Prio);
244         when N_Fusion_SERE =>
245            Print_Binary_Sequence (":", Seq, Prio);
246         when N_Within_SERE =>
247            Print_Binary_Sequence (" within ", Seq, Prio);
248         when N_Match_And_Seq =>
249            Print_Binary_Sequence (" && ", Seq, Prio);
250         when N_Or_Seq =>
251            Print_Binary_Sequence (" | ", Seq, Prio);
252         when N_And_Seq =>
253            Print_Binary_Sequence (" & ", Seq, Prio);
254         when N_Star_Repeat_Seq =>
255            Print_Repeat_Sequence ("[*", Seq);
256         when N_Goto_Repeat_Seq =>
257            Print_Repeat_Sequence ("[->", Seq);
258         when N_Equal_Repeat_Seq =>
259            Print_Repeat_Sequence ("[=", Seq);
260         when N_Plus_Repeat_Seq =>
261            Print_Sequence (Get_Sequence (Seq), Prio);
262            Put ("[+]");
263         when N_Booleans
264           | N_Name_Decl =>
265            Print_Expr (Seq);
266         when N_Sequence_Instance =>
267            Put (Image (Get_Identifier (Get_Declaration (Seq))));
268         when others =>
269            Error_Kind ("print_sequence", Seq);
270      end case;
271      if Add_Paren then
272         Put ("}");
273      end if;
274   end Print_Sequence;
275
276   procedure Print_Binary_Property (Name : String; N : Node; Prio : Priority)
277   is
278   begin
279      Print_Property (Get_Left (N), Prio);
280      Put (Name);
281      Print_Property (Get_Right (N), Prio);
282   end Print_Binary_Property;
283
284   procedure Print_Binary_Property_SI (Name : String;
285                                       N : Node; Prio : Priority)
286   is
287   begin
288      Print_Property (Get_Left (N), Prio);
289      Put (Name);
290      if Get_Strong_Flag (N) then
291         Put ('!');
292      end if;
293      if Get_Inclusive_Flag (N) then
294         Put ('_');
295      end if;
296      Put (' ');
297      Print_Property (Get_Right (N), Prio);
298   end Print_Binary_Property_SI;
299
300   procedure Print_Range_Property (Name : String; N : Node) is
301   begin
302      Put (Name);
303      Put ("[");
304      Print_Count (N);
305      Put ("](");
306      Print_Property (Get_Property (N), Prio_FL_Paren);
307      Put (")");
308   end Print_Range_Property;
309
310   procedure Print_Boolean_Range_Property (Name : String; N : Node) is
311   begin
312      Put (Name);
313      Put ("(");
314      Print_Expr (Get_Boolean (N));
315      Put (")[");
316      Print_Count (N);
317      Put ("](");
318      Print_Property (Get_Property (N), Prio_FL_Paren);
319      Put (")");
320   end Print_Boolean_Range_Property;
321
322   procedure Print_Property (Prop : Node;
323                             Parent_Prio : Priority := Prio_Lowest)
324   is
325      Prio : constant Priority := Get_Priority (Prop);
326   begin
327      if Prio < Parent_Prio then
328         Put ("(");
329      end if;
330      case Get_Kind (Prop) is
331         when N_Never =>
332            Put ("never ");
333            Print_Property (Get_Property (Prop), Prio);
334         when N_Always =>
335            Put ("always (");
336            Print_Property (Get_Property (Prop), Prio);
337            Put (")");
338         when N_Eventually =>
339            Put ("eventually! (");
340            Print_Property (Get_Property (Prop), Prio);
341            Put (")");
342         when N_Strong =>
343            Print_Property (Get_Property (Prop), Prio);
344            Put ("!");
345         when N_Next =>
346            Put ("next");
347--              if Get_Strong_Flag (Prop) then
348--                 Put ('!');
349--              end if;
350            Put (" (");
351            Print_Property (Get_Property (Prop), Prio);
352            Put (")");
353         when N_Next_A =>
354            Print_Range_Property ("next_a", Prop);
355         when N_Next_E =>
356            Print_Range_Property ("next_e", Prop);
357         when N_Next_Event =>
358            Put ("next_event");
359            Put ("(");
360            Print_Expr (Get_Boolean (Prop));
361            Put (")(");
362            Print_Property (Get_Property (Prop), Prio);
363            Put (")");
364         when N_Next_Event_A =>
365            Print_Boolean_Range_Property ("next_event_a", Prop);
366         when N_Next_Event_E =>
367            Print_Boolean_Range_Property ("next_event_e", Prop);
368         when N_Until =>
369            Print_Binary_Property_SI (" until", Prop, Prio);
370         when N_Abort =>
371            Print_Property (Get_Property (Prop), Prio);
372            Put (" abort ");
373            Print_Expr (Get_Boolean (Prop));
374         when N_Before =>
375            Print_Binary_Property_SI (" before", Prop, Prio);
376         when N_Or_Prop =>
377            if True then
378               Print_Binary_Property (" or ", Prop, Prio);
379            else
380               Print_Binary_Property (" || ", Prop, Prio);
381            end if;
382         when N_And_Prop =>
383            if True then
384               Print_Binary_Property (" and ", Prop, Prio);
385            else
386               Print_Binary_Property (" && ", Prop, Prio);
387            end if;
388         when N_Paren_Prop =>
389            Put ("(");
390            Print_Property (Get_Property (Prop), Prio);
391            Put (")");
392         when N_Imp_Seq =>
393            Print_Property (Get_Sequence (Prop), Prio);
394            Put (" |=> ");
395            Print_Property (Get_Property (Prop), Prio);
396         when N_Overlap_Imp_Seq =>
397            Print_Property (Get_Sequence (Prop), Prio);
398            Put (" |-> ");
399            Print_Property (Get_Property (Prop), Prio);
400         when N_Log_Imp_Prop =>
401            Print_Binary_Property (" -> ", Prop, Prio);
402         when N_Booleans
403           | N_Name_Decl =>
404            Print_Expr (Prop);
405         when N_Sequences =>
406            Print_Sequence (Prop, Parent_Prio);
407         when N_Property_Instance =>
408            Put (Image (Get_Identifier (Get_Declaration (Prop))));
409         when N_EOS =>
410            Put ("EOS");
411         when others =>
412            Error_Kind ("print_property", Prop);
413      end case;
414      if Prio < Parent_Prio then
415         Put (")");
416      end if;
417   end Print_Property;
418
419   procedure Print_Assert (N : Node) is
420      Label : Name_Id;
421   begin
422      Put ("  ");
423      Label := Get_Label (N);
424      if Label /= Null_Identifier then
425         Put (Image (Label));
426         Put (": ");
427      end if;
428      Put ("assert ");
429      Print_Property (Get_Property (N));
430      Put_Line (";");
431   end Print_Assert;
432
433   procedure Print_Property_Declaration (N : Node) is
434   begin
435      Put ("  ");
436      Put ("property ");
437      Put (Image (Get_Identifier (N)));
438      Put (" = ");
439      Print_Property (Get_Property (N));
440      Put_Line (";");
441   end Print_Property_Declaration;
442
443   procedure Print_Unit (Unit : Node) is
444      Item : Node;
445   begin
446      case Get_Kind (Unit) is
447         when N_Vunit =>
448            Put ("vunit");
449         when others =>
450            Error_Kind ("disp_unit", Unit);
451      end case;
452      Put (' ');
453      Put (Image (Get_Identifier (Unit)));
454      Put_Line (" {");
455      Item := Get_Item_Chain (Unit);
456      while Item /= Null_Node loop
457         case Get_Kind (Item) is
458            when N_Name_Decl =>
459               null;
460            when N_Assert_Directive =>
461               Print_Assert (Item);
462            when N_Property_Declaration =>
463               Print_Property_Declaration (Item);
464            when others =>
465               Error_Kind ("disp_unit", Item);
466         end case;
467         Item := Get_Chain (Item);
468      end loop;
469      Put_Line ("}");
470   end Print_Unit;
471end PSL.Prints;
472