1-- PSL - Utils 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.Nodes_Priv; 19with PSL.Errors; use PSL.Errors; 20 21package body PSL.NFAs.Utils is 22 generic 23 with function Get_First_Edge (S : NFA_State) return NFA_Edge; 24 with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; 25 with procedure Set_First_Edge (S : NFA_State; E : NFA_Edge); 26 with procedure Set_Next_Edge (E : NFA_Edge; N_E : NFA_Edge); 27 with function Get_Edge_State (E : NFA_Edge) return NFA_State; 28 package Sort_Edges is 29 procedure Sort_Edges (S : NFA_State); 30 procedure Sort_Edges (N : NFA); 31 end Sort_Edges; 32 33 package body Sort_Edges is 34 -- Use merge sort to sort a list of edges. 35 -- The first edge is START and the list has LEN edges. 36 -- RES is the head of the sorted list. 37 -- NEXT_EDGE is the LEN + 1 edge (not sorted). 38 procedure Edges_Merge_Sort (Start : NFA_Edge; 39 Len : Natural; 40 Res : out NFA_Edge; 41 Next_Edge : out NFA_Edge) 42 is 43 function Lt (L, R : NFA_Edge) return Boolean 44 is 45 L_Expr : constant Node := Get_Edge_Expr (L); 46 R_Expr : constant Node := Get_Edge_Expr (R); 47 begin 48 return PSL.Nodes_Priv."<" (L_Expr, R_Expr) 49 or else (L_Expr = R_Expr 50 and then Get_Edge_State (L) < Get_Edge_State (R)); 51 end Lt; 52 53 pragma Inline (Lt); 54 55 Half : constant Natural := Len / 2; 56 Left_Start, Right_Start : NFA_Edge; 57 Left_Next, Right_Next : NFA_Edge; 58 L, R : NFA_Edge; 59 Last, E : NFA_Edge; 60 begin 61 -- With less than 2 elements, the sort is trivial. 62 if Len < 2 then 63 if Len = 0 then 64 Next_Edge := Start; 65 else 66 Next_Edge := Get_Next_Edge (Start); 67 end if; 68 Res := Start; 69 return; 70 end if; 71 72 -- Sort each half. 73 Edges_Merge_Sort (Start, Half, Left_Start, Left_Next); 74 Edges_Merge_Sort (Left_Next, Len - Half, Right_Start, Right_Next); 75 76 -- Merge. 77 L := Left_Start; 78 R := Right_Start; 79 Last := No_Edge; 80 loop 81 -- Take from left iff: 82 -- * it is not empty 83 -- * right is empty or else (left < right) 84 if L /= Left_Next and then (R = Right_Next or else Lt (L, R)) then 85 E := L; 86 L := Get_Next_Edge (L); 87 88 -- Take from right if right is not empty. 89 elsif R /= Right_Next then 90 E := R; 91 R := Get_Next_Edge (R); 92 93 -- Both left are right are empty. 94 else 95 exit; 96 end if; 97 98 if Last = No_Edge then 99 Res := E; 100 else 101 Set_Next_Edge (Last, E); 102 end if; 103 Last := E; 104 end loop; 105 -- Let the link clean. 106 Next_Edge := Right_Next; 107 Set_Next_Edge (Last, Next_Edge); 108 end Edges_Merge_Sort; 109 110 procedure Sort_Edges (S : NFA_State) 111 is 112 Nbr_Edges : Natural; 113 First_E, E, Res : NFA_Edge; 114 begin 115 -- Count number of edges. 116 Nbr_Edges := 0; 117 First_E := Get_First_Edge (S); 118 E := First_E; 119 while E /= No_Edge loop 120 Nbr_Edges := Nbr_Edges + 1; 121 E := Get_Next_Edge (E); 122 end loop; 123 124 -- Sort edges by expression. 125 Edges_Merge_Sort (First_E, Nbr_Edges, Res, E); 126 pragma Assert (E = No_Edge); 127 Set_First_Edge (S, Res); 128 129 end Sort_Edges; 130 131 procedure Sort_Edges (N : NFA) 132 is 133 S : NFA_State; 134 begin 135 -- Iterate on states. 136 S := Get_First_State (N); 137 while S /= No_State loop 138 Sort_Edges (S); 139 S := Get_Next_State (S); 140 end loop; 141 end Sort_Edges; 142 end Sort_Edges; 143 144 package Sort_Src_Edges_Pkg is new 145 Sort_Edges (Get_First_Edge => Get_First_Src_Edge, 146 Get_Next_Edge => Get_Next_Src_Edge, 147 Set_First_Edge => Set_First_Src_Edge, 148 Set_Next_Edge => Set_Next_Src_Edge, 149 Get_Edge_State => Get_Edge_Dest); 150 151 procedure Sort_Src_Edges (S : NFA_State) renames 152 Sort_Src_Edges_Pkg.Sort_Edges; 153 procedure Sort_Src_Edges (N : NFA) renames 154 Sort_Src_Edges_Pkg.Sort_Edges; 155 156 package Sort_Dest_Edges_Pkg is new 157 Sort_Edges (Get_First_Edge => Get_First_Dest_Edge, 158 Get_Next_Edge => Get_Next_Dest_Edge, 159 Set_First_Edge => Set_First_Dest_Edge, 160 Set_Next_Edge => Set_Next_Dest_Edge, 161 Get_Edge_State => Get_Edge_Src); 162 163 procedure Sort_Dest_Edges (S : NFA_State) renames 164 Sort_Dest_Edges_Pkg.Sort_Edges; 165 procedure Sort_Dest_Edges (N : NFA) renames 166 Sort_Dest_Edges_Pkg.Sort_Edges; 167 168 generic 169 with function Get_First_Edge_Reverse (S : NFA_State) return NFA_Edge; 170 with function Get_First_Edge (S : NFA_State) return NFA_Edge; 171 with procedure Set_First_Edge (S : NFA_State; E : NFA_Edge); 172 with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; 173 with procedure Set_Next_Edge (E : NFA_Edge; E1 : NFA_Edge); 174 with procedure Set_Edge_State (E : NFA_Edge; S : NFA_State); 175 procedure Merge_State (N : NFA; S : NFA_State; S1 : NFA_State); 176 177 procedure Merge_State (N : NFA; S : NFA_State; S1 : NFA_State) 178 is 179 E, First_E, Next_E : NFA_Edge; 180 begin 181 pragma Assert (S /= S1); 182 183 -- Discard outgoing edges of S1. 184 loop 185 E := Get_First_Edge_Reverse (S1); 186 exit when E = No_Edge; 187 Remove_Edge (E); 188 end loop; 189 190 -- Prepend incoming edges of S1 to S. 191 First_E := Get_First_Edge (S); 192 E := Get_First_Edge (S1); 193 while E /= No_Edge loop 194 Next_E := Get_Next_Edge (E); 195 Set_Next_Edge (E, First_E); 196 Set_Edge_State (E, S); 197 First_E := E; 198 E := Next_E; 199 end loop; 200 Set_First_Edge (S, First_E); 201 Set_First_Edge (S1, No_Edge); 202 203 -- Move the active state if it is deleted. 204 if Get_Active_State (N) = S1 then 205 Set_Active_State (N, S); 206 end if; 207 208 Remove_State (N, S1); 209 end Merge_State; 210 211 procedure Merge_State_Dest_1 is new Merge_State 212 (Get_First_Edge_Reverse => Get_First_Src_Edge, 213 Get_First_Edge => Get_First_Dest_Edge, 214 Set_First_Edge => Set_First_Dest_Edge, 215 Get_Next_Edge => Get_Next_Dest_Edge, 216 Set_Next_Edge => Set_Next_Dest_Edge, 217 Set_Edge_State => Set_Edge_Dest); 218 219 procedure Merge_State_Dest (N : NFA; S : NFA_State; S1 : NFA_State) renames 220 Merge_State_Dest_1; 221 222 procedure Merge_State_Src_1 is new Merge_State 223 (Get_First_Edge_Reverse => Get_First_Dest_Edge, 224 Get_First_Edge => Get_First_Src_Edge, 225 Set_First_Edge => Set_First_Src_Edge, 226 Get_Next_Edge => Get_Next_Src_Edge, 227 Set_Next_Edge => Set_Next_Src_Edge, 228 Set_Edge_State => Set_Edge_Src); 229 230 procedure Merge_State_Src (N : NFA; S : NFA_State; S1 : NFA_State) renames 231 Merge_State_Src_1; 232 233 procedure Sort_Outgoing_Edges (N : NFA; Nbr_States : Natural) 234 is 235 Last_State : constant NFA_State := NFA_State (Nbr_States) - 1; 236 type Edge_Array is array (0 .. Last_State) of NFA_Edge; 237 Edges : Edge_Array := (others => No_Edge); 238 S, D : NFA_State; 239 E, Next_E : NFA_Edge; 240 First_Edge, Last_Edge : NFA_Edge; 241 begin 242 -- Iterate on states. 243 S := Get_First_State (N); 244 while S /= No_State loop 245 246 -- Create an array of edges 247 E := Get_First_Dest_Edge (S); 248 while E /= No_Edge loop 249 Next_E := Get_Next_Dest_Edge (E); 250 D := Get_Edge_Dest (E); 251 if Edges (D) /= No_Edge then 252 -- TODO: merge edges. 253 raise Program_Error; 254 end if; 255 Edges (D) := E; 256 E := Next_E; 257 end loop; 258 259 -- Rebuild the edge list (sorted by destination). 260 Last_Edge := No_Edge; 261 First_Edge := No_Edge; 262 for I in Edge_Array'Range loop 263 E := Edges (I); 264 if E /= No_Edge then 265 Edges (I) := No_Edge; 266 if First_Edge = No_Edge then 267 First_Edge := E; 268 else 269 Set_Next_Dest_Edge (Last_Edge, E); 270 end if; 271 Last_Edge := E; 272 end if; 273 end loop; 274 Set_First_Dest_Edge (S, First_Edge); 275 S := Get_Next_State (S); 276 end loop; 277 end Sort_Outgoing_Edges; 278 pragma Unreferenced (Sort_Outgoing_Edges); 279 280 generic 281 with function Get_First_Edge (S : NFA_State) return NFA_Edge; 282 with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; 283 with function Get_State_Reverse (E : NFA_Edge) return NFA_State; 284 with function Get_First_Edge_Reverse (S : NFA_State) return NFA_Edge; 285 with function Get_Next_Edge_Reverse (E : NFA_Edge) return NFA_Edge; 286 procedure Check_Edges_Gen (N : NFA); 287 288 procedure Check_Edges_Gen (N : NFA) 289 is 290 S : NFA_State; 291 E : NFA_Edge; 292 R_S : NFA_State; 293 R_E : NFA_Edge; 294 begin 295 S := Get_First_State (N); 296 while S /= No_State loop 297 E := Get_First_Edge (S); 298 while E /= No_Edge loop 299 R_S := Get_State_Reverse (E); 300 R_E := Get_First_Edge_Reverse (R_S); 301 while R_E /= No_Edge and then R_E /= E loop 302 R_E := Get_Next_Edge_Reverse (R_E); 303 end loop; 304 if R_E /= E then 305 raise Program_Error; 306 end if; 307 E := Get_Next_Edge (E); 308 end loop; 309 S := Get_Next_State (S); 310 end loop; 311 end Check_Edges_Gen; 312 313 procedure Check_Edges_Src is new Check_Edges_Gen 314 (Get_First_Edge => Get_First_Src_Edge, 315 Get_Next_Edge => Get_Next_Src_Edge, 316 Get_State_Reverse => Get_Edge_Dest, 317 Get_First_Edge_Reverse => Get_First_Dest_Edge, 318 Get_Next_Edge_Reverse => Get_Next_Dest_Edge); 319 320 procedure Check_Edges_Dest is new Check_Edges_Gen 321 (Get_First_Edge => Get_First_Dest_Edge, 322 Get_Next_Edge => Get_Next_Dest_Edge, 323 Get_State_Reverse => Get_Edge_Src, 324 Get_First_Edge_Reverse => Get_First_Src_Edge, 325 Get_Next_Edge_Reverse => Get_Next_Src_Edge); 326 327 procedure Check_NFA (N : NFA) is 328 begin 329 Check_Edges_Src (N); 330 Check_Edges_Dest (N); 331 end Check_NFA; 332 333 function Has_EOS (N : Node) return Boolean is 334 begin 335 case Get_Kind (N) is 336 when N_EOS => 337 return True; 338 when N_False 339 | N_True 340 | N_HDL_Bool => 341 return False; 342 when N_Not_Bool => 343 return Has_EOS (Get_Boolean (N)); 344 when N_And_Bool 345 | N_Or_Bool 346 | N_Imp_Bool => 347 return Has_EOS (Get_Left (N)) or else Has_EOS (Get_Right (N)); 348 when others => 349 Error_Kind ("Has_EOS", N); 350 end case; 351 end Has_EOS; 352 353 procedure Set_Init_Loop (N : NFA) 354 is 355 Start : constant NFA_State := Get_Start_State (N); 356 E : NFA_Edge; 357 Expr : Node; 358 begin 359 -- Look for existing edge. 360 E := Get_First_Src_Edge (Start); 361 while E /= No_Edge loop 362 if Get_Edge_Dest (E) = Start then 363 Expr := Get_Edge_Expr (E); 364 if Get_Kind (Expr) = N_True then 365 return; 366 end if; 367 Set_Edge_Expr (E, True_Node); 368 return; 369 end if; 370 E := Get_Next_Src_Edge (E); 371 end loop; 372 373 -- No existing edge. Create one. 374 Add_Edge (Start, Start, True_Node); 375 end Set_Init_Loop; 376 377end PSL.NFAs.Utils; 378