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