diff options
| author | Tristan Gingold <tgingold@free.fr> | 2014-11-04 20:14:19 +0100 |
|---|---|---|
| committer | Tristan Gingold <tgingold@free.fr> | 2014-11-04 20:14:19 +0100 |
| commit | 9c195bf5d86d67ea5eb419ccf6e48dc153e57c68 (patch) | |
| tree | 575346e529b99e26382b4a06f6ff2caa0b391ab2 /psl | |
| parent | 184a123f91e07c927292d67462561dc84f3a920d (diff) | |
| download | ghdl-9c195bf5d86d67ea5eb419ccf6e48dc153e57c68.tar.gz ghdl-9c195bf5d86d67ea5eb419ccf6e48dc153e57c68.tar.bz2 ghdl-9c195bf5d86d67ea5eb419ccf6e48dc153e57c68.zip | |
Move sources to src/ subdirectory.
Diffstat (limited to 'psl')
| -rw-r--r-- | psl/psl-build.adb | 1009 | ||||
| -rw-r--r-- | psl/psl-build.ads | 7 | ||||
| -rw-r--r-- | psl/psl-cse.adb | 201 | ||||
| -rw-r--r-- | psl/psl-cse.ads | 10 | ||||
| -rw-r--r-- | psl/psl-disp_nfas.adb | 111 | ||||
| -rw-r--r-- | psl/psl-disp_nfas.ads | 12 | ||||
| -rw-r--r-- | psl/psl-dump_tree.adb | 867 | ||||
| -rw-r--r-- | psl/psl-dump_tree.ads | 9 | ||||
| -rw-r--r-- | psl/psl-hash.adb | 60 | ||||
| -rw-r--r-- | psl/psl-hash.ads | 11 | ||||
| -rw-r--r-- | psl/psl-nfas-utils.adb | 330 | ||||
| -rw-r--r-- | psl/psl-nfas-utils.ads | 21 | ||||
| -rw-r--r-- | psl/psl-nfas.adb | 529 | ||||
| -rw-r--r-- | psl/psl-nfas.ads | 108 | ||||
| -rw-r--r-- | psl/psl-nodes.adb | 1231 | ||||
| -rw-r--r-- | psl/psl-nodes.ads | 563 | ||||
| -rw-r--r-- | psl/psl-optimize.adb | 460 | ||||
| -rw-r--r-- | psl/psl-optimize.ads | 24 | ||||
| -rw-r--r-- | psl/psl-prints.adb | 433 | ||||
| -rw-r--r-- | psl/psl-prints.ads | 20 | ||||
| -rw-r--r-- | psl/psl-priorities.ads | 63 | ||||
| -rw-r--r-- | psl/psl-qm.adb | 318 | ||||
| -rw-r--r-- | psl/psl-qm.ads | 49 | ||||
| -rw-r--r-- | psl/psl-rewrites.adb | 604 | ||||
| -rw-r--r-- | psl/psl-rewrites.ads | 7 | ||||
| -rw-r--r-- | psl/psl-subsets.adb | 177 | ||||
| -rw-r--r-- | psl/psl-subsets.ads | 23 | ||||
| -rw-r--r-- | psl/psl-tprint.adb | 255 | ||||
| -rw-r--r-- | psl/psl-tprint.ads | 6 | ||||
| -rw-r--r-- | psl/psl.ads | 3 |
30 files changed, 0 insertions, 7521 deletions
diff --git a/psl/psl-build.adb b/psl/psl-build.adb deleted file mode 100644 index c3e47baa6..000000000 --- a/psl/psl-build.adb +++ /dev/null @@ -1,1009 +0,0 @@ -with GNAT.Table; -with Ada.Text_IO; use Ada.Text_IO; -with Types; use Types; -with PSL.Errors; use PSL.Errors; -with PSL.CSE; use PSL.CSE; -with PSL.QM; -with PSL.Disp_NFAs; use PSL.Disp_NFAs; -with PSL.Optimize; use PSL.Optimize; -with PSL.NFAs.Utils; -with PSL.Prints; -with PSL.NFAs; use PSL.NFAs; - -package body PSL.Build is - function Build_SERE_FA (N : Node) return NFA; - - - package Intersection is - function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA; - end Intersection; - - package body Intersection is - - type Stack_Entry_Id is new Natural; - No_Stack_Entry : constant Stack_Entry_Id := 0; - type Stack_Entry is record - L, R : NFA_State; - Res : NFA_State; - Next_Unhandled : Stack_Entry_Id; - end record; - - package Stackt is new GNAT.Table - (Table_Component_Type => Stack_Entry, - Table_Index_Type => Stack_Entry_Id, - Table_Low_Bound => 1, - Table_Initial => 128, - Table_Increment => 100); - - First_Unhandled : Stack_Entry_Id; - - procedure Init_Stack is - begin - Stackt.Init; - First_Unhandled := No_Stack_Entry; - end Init_Stack; - - function Not_Empty return Boolean is - begin - return First_Unhandled /= No_Stack_Entry; - end Not_Empty; - - procedure Pop_State (L, R : out NFA_State) is - begin - L := Stackt.Table (First_Unhandled).L; - R := Stackt.Table (First_Unhandled).R; - First_Unhandled := Stackt.Table (First_Unhandled).Next_Unhandled; - end Pop_State; - - function Get_State (N : NFA; L, R : NFA_State) return NFA_State - is - Res : NFA_State; - begin - for I in Stackt.First .. Stackt.Last loop - if Stackt.Table (I).L = L - and then Stackt.Table (I).R = R - then - return Stackt.Table (I).Res; - end if; - end loop; - Res := Add_State (N); - Stackt.Append ((L => L, R => R, Res => Res, - Next_Unhandled => First_Unhandled)); - First_Unhandled := Stackt.Last; - return Res; - end Get_State; - - function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA - is - Start_L, Start_R : NFA_State; - Final_L, Final_R : NFA_State; - S_L, S_R : NFA_State; - E_L, E_R : NFA_Edge; - Res : NFA; - Start : NFA_State; - Extra_L, Extra_R : NFA_Edge; - begin - Start_L := Get_Start_State (L); - Start_R := Get_Start_State (R); - Final_R := Get_Final_State (R); - Final_L := Get_Final_State (L); - - if False then - Disp_Body (L); - Disp_Body (R); - Put ("//start state: "); - Disp_State (Start_L); - Put (","); - Disp_State (Start_R); - New_Line; - end if; - - if Match_Len then - Extra_L := No_Edge; - Extra_R := No_Edge; - else - Extra_L := Add_Edge (Final_L, Final_L, True_Node); - Extra_R := Add_Edge (Final_R, Final_R, True_Node); - end if; - - Res := Create_NFA; - Init_Stack; - Start := Get_State (Res, Start_L, Start_R); - Set_Start_State (Res, Start); - - while Not_Empty loop - Pop_State (S_L, S_R); - - if False then - Put ("//poped state: "); - Disp_State (S_L); - Put (","); - Disp_State (S_R); - New_Line; - end if; - - E_L := Get_First_Src_Edge (S_L); - while E_L /= No_Edge loop - E_R := Get_First_Src_Edge (S_R); - while E_R /= No_Edge loop - if not (E_L = Extra_L and E_R = Extra_R) then - Add_Edge (Get_State (Res, S_L, S_R), - Get_State (Res, - Get_Edge_Dest (E_L), - Get_Edge_Dest (E_R)), - Build_Bool_And (Get_Edge_Expr (E_L), - Get_Edge_Expr (E_R))); - end if; - E_R := Get_Next_Src_Edge (E_R); - end loop; - E_L := Get_Next_Src_Edge (E_L); - end loop; - end loop; - Set_Final_State (Res, Get_State (Res, Final_L, Final_R)); - Remove_Unreachable_States (Res); - - if not Match_Len then - Remove_Edge (Extra_L); - Remove_Edge (Extra_R); - end if; - - -- FIXME: free L and R. - return Res; - end Build_Inter; - end Intersection; - - -- All edges from A are duplicated using B as a source. - -- Handle epsilon-edges. - procedure Duplicate_Src_Edges (N : NFA; A, B : NFA_State) - is - pragma Unreferenced (N); - E : NFA_Edge; - Expr : Node; - Dest : NFA_State; - begin - pragma Assert (A /= B); - E := Get_First_Src_Edge (A); - while E /= No_Edge loop - Expr := Get_Edge_Expr (E); - Dest := Get_Edge_Dest (E); - if Expr /= Null_Node then - Add_Edge (B, Dest, Expr); - end if; - E := Get_Next_Src_Edge (E); - end loop; - end Duplicate_Src_Edges; - - -- All edges to A are duplicated using B as a destination. - -- Handle epsilon-edges. - procedure Duplicate_Dest_Edges (N : NFA; A, B : NFA_State) - is - pragma Unreferenced (N); - E : NFA_Edge; - Expr : Node; - Src : NFA_State; - begin - pragma Assert (A /= B); - E := Get_First_Dest_Edge (A); - while E /= No_Edge loop - Expr := Get_Edge_Expr (E); - Src := Get_Edge_Src (E); - if Expr /= Null_Node then - Add_Edge (Src, B, Expr); - end if; - E := Get_Next_Dest_Edge (E); - end loop; - end Duplicate_Dest_Edges; - - procedure Remove_Epsilon_Edge (N : NFA; S, D : NFA_State) is - begin - if Get_First_Src_Edge (S) = No_Edge then - -- No edge from S. - -- Move edges to S to D. - Redest_Edges (S, D); - Remove_Unconnected_State (N, S); - if Get_Start_State (N) = S then - Set_Start_State (N, D); - end if; - elsif Get_First_Dest_Edge (D) = No_Edge then - -- No edge to D. - -- Move edges from D to S. - Resource_Edges (D, S); - Remove_Unconnected_State (N, D); - if Get_Final_State (N) = D then - Set_Final_State (N, S); - end if; - else - Duplicate_Dest_Edges (N, S, D); - Duplicate_Src_Edges (N, D, S); - Remove_Identical_Src_Edges (S); - end if; - end Remove_Epsilon_Edge; - - procedure Remove_Epsilon (N : NFA; - E : NFA_Edge) is - S : constant NFA_State := Get_Edge_Src (E); - D : constant NFA_State := Get_Edge_Dest (E); - begin - Remove_Edge (E); - - Remove_Epsilon_Edge (N, S, D); - end Remove_Epsilon; - - function Build_Concat (L, R : NFA) return NFA - is - Start_L, Start_R : NFA_State; - Final_L, Final_R : NFA_State; - Eps_L, Eps_R : Boolean; - E_L, E_R : NFA_Edge; - begin - Start_L := Get_Start_State (L); - Start_R := Get_Start_State (R); - Final_R := Get_Final_State (R); - Final_L := Get_Final_State (L); - Eps_L := Get_Epsilon_NFA (L); - Eps_R := Get_Epsilon_NFA (R); - - Merge_NFA (L, R); - - Set_Start_State (L, Start_L); - Set_Final_State (L, Final_R); - Set_Epsilon_NFA (L, False); - - if Eps_L then - E_L := Add_Edge (Start_L, Final_L, Null_Node); - end if; - - if Eps_R then - E_R := Add_Edge (Start_R, Final_R, Null_Node); - end if; - - Remove_Epsilon_Edge (L, Final_L, Start_R); - - if Eps_L then - Remove_Epsilon (L, E_L); - end if; - if Eps_R then - Remove_Epsilon (L, E_R); - end if; - - if (Start_L = Final_L or else Eps_L) - and then (Start_R = Final_R or else Eps_R) - then - Set_Epsilon_NFA (L, True); - end if; - - Remove_Identical_Src_Edges (Final_L); - Remove_Identical_Dest_Edges (Start_R); - - return L; - end Build_Concat; - - function Build_Or (L, R : NFA) return NFA - is - Start_L, Start_R : NFA_State; - Final_L, Final_R : NFA_State; - Eps : Boolean; - Start, Final : NFA_State; - E_S_L, E_S_R, E_L_F, E_R_F : NFA_Edge; - begin - Start_L := Get_Start_State (L); - Start_R := Get_Start_State (R); - Final_R := Get_Final_State (R); - Final_L := Get_Final_State (L); - Eps := Get_Epsilon_NFA (L) or Get_Epsilon_NFA (R); - - -- Optimize [*0] | R. - if Start_L = Final_L - and then Get_First_Src_Edge (Start_L) = No_Edge - then - if Start_R /= Final_R then - Set_Epsilon_NFA (R, True); - end if; - -- FIXME - -- delete_NFA (L); - return R; - end if; - - Merge_NFA (L, R); - - -- Use Thompson construction. - Start := Add_State (L); - Set_Start_State (L, Start); - E_S_L := Add_Edge (Start, Start_L, Null_Node); - E_S_R := Add_Edge (Start, Start_R, Null_Node); - - Final := Add_State (L); - Set_Final_State (L, Final); - E_L_F := Add_Edge (Final_L, Final, Null_Node); - E_R_F := Add_Edge (Final_R, Final, Null_Node); - - Set_Epsilon_NFA (L, Eps); - - Remove_Epsilon (L, E_S_L); - Remove_Epsilon (L, E_S_R); - Remove_Epsilon (L, E_L_F); - Remove_Epsilon (L, E_R_F); - - return L; - end Build_Or; - - function Build_Fusion (L, R : NFA) return NFA - is - Start_R : NFA_State; - Final_L, Final_R, S_L : NFA_State; - E_L : NFA_Edge; - E_R : NFA_Edge; - N_L, Expr : Node; - begin - Start_R := Get_Start_State (R); - Final_R := Get_Final_State (R); - Final_L := Get_Final_State (L); - - Merge_NFA (L, R); - - E_L := Get_First_Dest_Edge (Final_L); - while E_L /= No_Edge loop - S_L := Get_Edge_Src (E_L); - N_L := Get_Edge_Expr (E_L); - - E_R := Get_First_Src_Edge (Start_R); - while E_R /= No_Edge loop - Expr := Build_Bool_And (N_L, Get_Edge_Expr (E_R)); - Expr := PSL.QM.Reduce (Expr); - if Expr /= False_Node then - Add_Edge (S_L, Get_Edge_Dest (E_R), Expr); - end if; - E_R := Get_Next_Src_Edge (E_R); - end loop; - Remove_Identical_Src_Edges (S_L); - E_L := Get_Next_Dest_Edge (E_L); - end loop; - - Set_Final_State (L, Final_R); - - Set_Epsilon_NFA (L, False); - - if Get_First_Src_Edge (Final_L) = No_Edge then - Remove_State (L, Final_L); - end if; - if Get_First_Dest_Edge (Start_R) = No_Edge then - Remove_State (L, Start_R); - end if; - - return L; - end Build_Fusion; - - function Build_Star_Repeat (N : Node) return NFA is - Res : NFA; - Start, Final, S : NFA_State; - Seq : Node; - begin - Seq := Get_Sequence (N); - if Seq = Null_Node then - -- Epsilon. - Res := Create_NFA; - S := Add_State (Res); - Set_Start_State (Res, S); - Set_Final_State (Res, S); - return Res; - end if; - Res := Build_SERE_FA (Seq); - Start := Get_Start_State (Res); - Final := Get_Final_State (Res); - Redest_Edges (Final, Start); - Set_Final_State (Res, Start); - Remove_Unconnected_State (Res, Final); - Set_Epsilon_NFA (Res, False); - return Res; - end Build_Star_Repeat; - - function Build_Plus_Repeat (N : Node) return NFA is - Res : NFA; - Start, Final : NFA_State; - T : NFA_Edge; - begin - Res := Build_SERE_FA (Get_Sequence (N)); - Start := Get_Start_State (Res); - Final := Get_Final_State (Res); - T := Get_First_Dest_Edge (Final); - while T /= No_Edge loop - Add_Edge (Get_Edge_Src (T), Start, Get_Edge_Expr (T)); - T := Get_Next_Src_Edge (T); - end loop; - return Res; - end Build_Plus_Repeat; - - -- Association actual to formals, so that when a formal is referenced, the - -- actual can be used instead. - procedure Assoc_Instance (Decl : Node; Instance : Node) - is - Formal : Node; - Actual : Node; - begin - -- Temporary associates actuals to formals. - Formal := Get_Parameter_List (Decl); - Actual := Get_Association_Chain (Instance); - while Formal /= Null_Node loop - if Actual = Null_Node then - -- Not enough actual. - raise Internal_Error; - end if; - if Get_Actual (Formal) /= Null_Node then - -- Recursion - raise Internal_Error; - end if; - Set_Actual (Formal, Get_Actual (Actual)); - Formal := Get_Chain (Formal); - Actual := Get_Chain (Actual); - end loop; - if Actual /= Null_Node then - -- Too many actual. - raise Internal_Error; - end if; - end Assoc_Instance; - - procedure Unassoc_Instance (Decl : Node) - is - Formal : Node; - begin - -- Remove temporary association. - Formal := Get_Parameter_List (Decl); - while Formal /= Null_Node loop - Set_Actual (Formal, Null_Node); - Formal := Get_Chain (Formal); - end loop; - end Unassoc_Instance; - - function Build_SERE_FA (N : Node) return NFA - is - Res : NFA; - S1, S2 : NFA_State; - begin - case Get_Kind (N) is - when N_Booleans => - Res := Create_NFA; - S1 := Add_State (Res); - S2 := Add_State (Res); - Set_Start_State (Res, S1); - Set_Final_State (Res, S2); - if N /= False_Node then - Add_Edge (S1, S2, N); - end if; - return Res; - when N_Braced_SERE => - return Build_SERE_FA (Get_SERE (N)); - when N_Concat_SERE => - return Build_Concat (Build_SERE_FA (Get_Left (N)), - Build_SERE_FA (Get_Right (N))); - when N_Fusion_SERE => - return Build_Fusion (Build_SERE_FA (Get_Left (N)), - Build_SERE_FA (Get_Right (N))); - when N_Match_And_Seq => - return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)), - Build_SERE_FA (Get_Right (N)), - True); - when N_And_Seq => - return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)), - Build_SERE_FA (Get_Right (N)), - False); - when N_Or_Prop - | N_Or_Seq => - return Build_Or (Build_SERE_FA (Get_Left (N)), - Build_SERE_FA (Get_Right (N))); - when N_Star_Repeat_Seq => - return Build_Star_Repeat (N); - when N_Plus_Repeat_Seq => - return Build_Plus_Repeat (N); - when N_Sequence_Instance - | N_Endpoint_Instance => - declare - Decl : Node; - begin - Decl := Get_Declaration (N); - Assoc_Instance (Decl, N); - Res := Build_SERE_FA (Get_Sequence (Decl)); - Unassoc_Instance (Decl); - return Res; - end; - when N_Boolean_Parameter - | N_Sequence_Parameter => - declare - Actual : constant Node := Get_Actual (N); - begin - if Actual = Null_Node then - raise Internal_Error; - end if; - return Build_SERE_FA (Actual); - end; - when others => - Error_Kind ("build_sere_fa", N); - end case; - end Build_SERE_FA; - - function Count_Edges (S : NFA_State) return Natural - is - Res : Natural; - E : NFA_Edge; - begin - Res := 0; - E := Get_First_Src_Edge (S); - while E /= No_Edge loop - Res := Res + 1; - E := Get_Next_Src_Edge (E); - end loop; - return Res; - end Count_Edges; - - type Count_Vector is array (Natural range <>) of Natural; - - procedure Count_All_Edges (N : NFA; Res : out Count_Vector) - is - S : NFA_State; - begin - S := Get_First_State (N); - while S /= No_State loop - Res (Natural (Get_State_Label (S))) := Count_Edges (S); - S := Get_Next_State (S); - end loop; - end Count_All_Edges; - - pragma Unreferenced (Count_All_Edges); - - package Determinize is - -- Create a new NFA that reaches its final state only when N fails - -- (ie when the final state is not reached). - function Determinize (N : NFA) return NFA; - end Determinize; - - package body Determinize is - -- In all the comments N stands for the initial NFA (ie the NFA to - -- determinize). - - use Prints; - - Flag_Trace : constant Boolean := False; - Last_Label : Int32 := 0; - - -- The tree associates a set of states in N to *an* uniq set in the - -- result NFA. - -- - -- As the NFA is labelized, each node represent a state in N, and has - -- two branches: one for state is present and one for state is absent. - -- - -- The leaves contain the state in the result NFA. - -- - -- The leaves are chained to create a stack of state to handle. - -- - -- The root of the tree is node Start_Tree_Id and represent the start - -- state of N. - type Deter_Tree_Id is new Natural; - No_Tree_Id : constant Deter_Tree_Id := 0; - Start_Tree_Id : constant Deter_Tree_Id := 1; - - -- List of unhanded leaves. - Deter_Head : Deter_Tree_Id; - - type Deter_Tree_Id_Bool_Array is array (Boolean) of Deter_Tree_Id; - - -- Node in the tree. - type Deter_Tree_Entry is record - Parent : Deter_Tree_Id; - - -- For non-leaf: - Child : Deter_Tree_Id_Bool_Array; - - -- For leaf: - Link : Deter_Tree_Id; - State : NFA_State; - -- + value ? - end record; - - package Detert is new GNAT.Table - (Table_Component_Type => Deter_Tree_Entry, - Table_Index_Type => Deter_Tree_Id, - Table_Low_Bound => 1, - Table_Initial => 128, - Table_Increment => 100); - - type Bool_Vector is array (Natural range <>) of Boolean; - pragma Pack (Bool_Vector); - - -- Convert a set of states in N to a state in the result NFA. - -- The set is represented by a vector of boolean. An element of the - -- vector is true iff the corresponding state is present. - function Add_Vector (V : Bool_Vector; N : NFA) return NFA_State - is - E : Deter_Tree_Id; - Added : Boolean; - Res : NFA_State; - begin - E := Start_Tree_Id; - Added := False; - for I in V'Range loop - if Detert.Table (E).Child (V (I)) = No_Tree_Id then - Detert.Append ((Child => (No_Tree_Id, No_Tree_Id), - Parent => E, - Link => No_Tree_Id, - State => No_State)); - Detert.Table (E).Child (V (I)) := Detert.Last; - E := Detert.Last; - Added := True; - else - E := Detert.Table (E).Child (V (I)); - Added := False; - end if; - end loop; - if Added then - -- Create the new state. - Res := Add_State (N); - Detert.Table (E).State := Res; - - if Flag_Trace then - Set_State_Label (Res, Last_Label); - Put ("Result state" & Int32'Image (Last_Label) & " for"); - for I in V'Range loop - if V (I) then - Put (Natural'Image (I)); - end if; - end loop; - New_Line; - Last_Label := Last_Label + 1; - end if; - - -- Put it to the list of states to be handled. - Detert.Table (E).Link := Deter_Head; - Deter_Head := E; - - return Res; - else - return Detert.Table (E).State; - end if; - end Add_Vector; - - -- Return true iff the stack is empty (ie all the states have been - -- handled). - function Stack_Empty return Boolean is - begin - return Deter_Head = No_Tree_Id; - end Stack_Empty; - - -- Get an element from the stack. - -- Extract the state in the result NFA. - -- Rebuild the set of states in N (ie rebuild the vector of states). - procedure Stack_Pop (V : out Bool_Vector; S : out NFA_State) - is - L, P : Deter_Tree_Id; - begin - L := Deter_Head; - pragma Assert (L /= No_Tree_Id); - S := Detert.Table (L).State; - Deter_Head := Detert.Table (L).Link; - - for I in reverse V'Range loop - pragma Assert (L /= Start_Tree_Id); - P := Detert.Table (L).Parent; - if L = Detert.Table (P).Child (True) then - V (I) := True; - elsif L = Detert.Table (P).Child (False) then - V (I) := False; - else - raise Program_Error; - end if; - L := P; - end loop; - pragma Assert (L = Start_Tree_Id); - end Stack_Pop; - - type State_Vector is array (Natural range <>) of Natural; - type Expr_Vector is array (Natural range <>) of Node; - - procedure Build_Arcs (N : NFA; - State : NFA_State; - States : State_Vector; - Exprs : Expr_Vector; - Expr : Node; - V : Bool_Vector) - is - begin - if Expr = False_Node then - return; - end if; - - if States'Length = 0 then - declare - Reduced_Expr : constant Node := PSL.QM.Reduce (Expr); - --Reduced_Expr : constant Node := Expr; - S : NFA_State; - begin - if Reduced_Expr = False_Node then - return; - end if; - S := Add_Vector (V, N); - Add_Edge (State, S, Reduced_Expr); - if Flag_Trace then - Put (" Add edge"); - Put (Int32'Image (Get_State_Label (State))); - Put (" to"); - Put (Int32'Image (Get_State_Label (S))); - Put (", expr="); - Dump_Expr (Expr); - Put (", reduced="); - Dump_Expr (Reduced_Expr); - New_Line; - end if; - end; - else - declare - N_States : State_Vector renames - States (States'First + 1 .. States'Last); - N_V : Bool_Vector (V'Range) := V; - S : constant Natural := States (States'First); - E : constant Node := Exprs (S); - begin - N_V (S) := True; - if Expr = Null_Node then - Build_Arcs (N, State, N_States, Exprs, E, N_V); - Build_Arcs (N, State, N_States, Exprs, - Build_Bool_Not (E), V); - else - Build_Arcs (N, State, N_States, Exprs, - Build_Bool_And (E, Expr), N_V); - Build_Arcs (N, State, N_States, Exprs, - Build_Bool_And (Build_Bool_Not (E), Expr), V); - end if; - end; - end if; - end Build_Arcs; - - function Determinize_1 (N : NFA; Nbr_States : Natural) return NFA - is - Final : Natural; - V : Bool_Vector (0 .. Nbr_States - 1); - Exprs : Expr_Vector (0 .. Nbr_States - 1); - S : NFA_State; - E : NFA_Edge; - D : Natural; - Edge_Expr : Node; - Expr : Node; - Nbr_Dest : Natural; - States : State_Vector (0 .. Nbr_States - 1); - Res : NFA; - State : NFA_State; - begin - Final := Natural (Get_State_Label (Get_Final_State (N))); - - -- FIXME: handle epsilon or final = start -> create an empty NFA. - - -- Initialize the tree. - Res := Create_NFA; - Detert.Init; - Detert.Append ((Child => (No_Tree_Id, No_Tree_Id), - Parent => No_Tree_Id, - Link => No_Tree_Id, - State => No_State)); - pragma Assert (Detert.Last = Start_Tree_Id); - Deter_Head := No_Tree_Id; - - -- Put the initial state in the tree and in the stack. - -- FIXME: ok, we know that its label is 0. - V := (0 => True, others => False); - State := Add_Vector (V, Res); - Set_Start_State (Res, State); - - -- The failure state. As there is nothing to do with this - -- state, remove it from the stack. - V := (others => False); - State := Add_Vector (V, Res); - Set_Final_State (Res, State); - Stack_Pop (V, State); - - -- Iterate on states in the result NFA that haven't yet been handled. - while not Stack_Empty loop - Stack_Pop (V, State); - - if Flag_Trace then - Put_Line ("Handle result state" - & Int32'Image (Get_State_Label (State))); - end if; - - -- Build edges vector. - Exprs := (others => Null_Node); - Expr := Null_Node; - - S := Get_First_State (N); - Nbr_Dest := 0; - while S /= No_State loop - if V (Natural (Get_State_Label (S))) then - E := Get_First_Src_Edge (S); - while E /= No_Edge loop - D := Natural (Get_State_Label (Get_Edge_Dest (E))); - Edge_Expr := Get_Edge_Expr (E); - - if False and Flag_Trace then - Put_Line (" edge" & Int32'Image (Get_State_Label (S)) - & " to" & Natural'Image (D)); - end if; - - if D = Final then - Edge_Expr := Build_Bool_Not (Edge_Expr); - if Expr = Null_Node then - Expr := Edge_Expr; - else - Expr := Build_Bool_And (Expr, Edge_Expr); - end if; - else - if Exprs (D) = Null_Node then - Exprs (D) := Edge_Expr; - States (Nbr_Dest) := D; - Nbr_Dest := Nbr_Dest + 1; - else - Exprs (D) := Build_Bool_Or (Exprs (D), - Edge_Expr); - end if; - end if; - E := Get_Next_Src_Edge (E); - end loop; - end if; - S := Get_Next_State (S); - end loop; - - if Flag_Trace then - Put (" Final: expr="); - Print_Expr (Expr); - New_Line; - for I in 0 .. Nbr_Dest - 1 loop - Put (" Dest"); - Put (Natural'Image (States (I))); - Put (" expr="); - Print_Expr (Exprs (States (I))); - New_Line; - end loop; - end if; - - -- Build arcs. - if not (Nbr_Dest = 0 and Expr = Null_Node) then - Build_Arcs (Res, State, - States (0 .. Nbr_Dest - 1), Exprs, Expr, - Bool_Vector'(0 .. Nbr_States - 1 => False)); - end if; - end loop; - - --Remove_Unreachable_States (Res); - return Res; - end Determinize_1; - - function Determinize (N : NFA) return NFA - is - Nbr_States : Natural; - begin - Labelize_States (N, Nbr_States); - - if Flag_Trace then - Put_Line ("NFA to determinize:"); - Disp_NFA (N); - Last_Label := 0; - end if; - - return Determinize_1 (N, Nbr_States); - end Determinize; - end Determinize; - - function Build_Initial_Rep (N : NFA) return NFA - is - S : constant NFA_State := Get_Start_State (N); - begin - Add_Edge (S, S, True_Node); - return N; - end Build_Initial_Rep; - - procedure Build_Strong (N : NFA) - is - S : NFA_State; - Final : constant NFA_State := Get_Final_State (N); - begin - S := Get_First_State (N); - while S /= No_State loop - -- FIXME. - if S /= Final then - Add_Edge (S, Final, EOS_Node); - end if; - S := Get_Next_State (S); - end loop; - end Build_Strong; - - procedure Build_Abort (N : NFA; Expr : Node) - is - S : NFA_State; - E : NFA_Edge; - Not_Expr : Node; - begin - Not_Expr := Build_Bool_Not (Expr); - S := Get_First_State (N); - while S /= No_State loop - E := Get_First_Src_Edge (S); - while E /= No_Edge loop - Set_Edge_Expr (E, Build_Bool_And (Not_Expr, Get_Edge_Expr (E))); - E := Get_Next_Src_Edge (E); - end loop; - S := Get_Next_State (S); - end loop; - end Build_Abort; - - function Build_Property_FA (N : Node) return NFA - is - L, R : NFA; - begin - case Get_Kind (N) is - when N_Sequences - | N_Booleans => - -- Build A(S) or A(B) - R := Build_SERE_FA (N); - return Determinize.Determinize (R); - when N_Strong => - R := Build_Property_FA (Get_Property (N)); - Build_Strong (R); - return R; - when N_Imp_Seq => - -- R |=> P --> {R; TRUE} |-> P - L := Build_SERE_FA (Get_Sequence (N)); - R := Build_Property_FA (Get_Property (N)); - return Build_Concat (L, R); - when N_Overlap_Imp_Seq => - -- S |-> P is defined as Ac(S) : A(P) - L := Build_SERE_FA (Get_Sequence (N)); - R := Build_Property_FA (Get_Property (N)); - return Build_Fusion (L, R); - when N_Log_Imp_Prop => - -- B -> P --> {B} |-> P --> Ac(B) : A(P) - L := Build_SERE_FA (Get_Left (N)); - R := Build_Property_FA (Get_Right (N)); - return Build_Fusion (L, R); - when N_And_Prop => - -- P1 && P2 --> A(P1) | A(P2) - L := Build_Property_FA (Get_Left (N)); - R := Build_Property_FA (Get_Right (N)); - return Build_Or (L, R); - when N_Never => - R := Build_SERE_FA (Get_Property (N)); - return Build_Initial_Rep (R); - when N_Always => - R := Build_Property_FA (Get_Property (N)); - return Build_Initial_Rep (R); - when N_Abort => - R := Build_Property_FA (Get_Property (N)); - Build_Abort (R, Get_Boolean (N)); - return R; - when N_Property_Instance => - declare - Decl : Node; - begin - Decl := Get_Declaration (N); - Assoc_Instance (Decl, N); - R := Build_Property_FA (Get_Property (Decl)); - Unassoc_Instance (Decl); - return R; - end; - when others => - Error_Kind ("build_property_fa", N); - end case; - end Build_Property_FA; - - function Build_FA (N : Node) return NFA - is - use PSL.NFAs.Utils; - Res : NFA; - begin - Res := Build_Property_FA (N); - if Optimize_Final then - pragma Debug (Check_NFA (Res)); - - Remove_Unreachable_States (Res); - Remove_Simple_Prefix (Res); - Merge_Identical_States (Res); - Merge_Edges (Res); - end if; - -- Clear the QM table. - PSL.QM.Reset; - return Res; - end Build_FA; -end PSL.Build; diff --git a/psl/psl-build.ads b/psl/psl-build.ads deleted file mode 100644 index d0ca26a39..000000000 --- a/psl/psl-build.ads +++ /dev/null @@ -1,7 +0,0 @@ -with PSL.Nodes; use PSL.Nodes; - -package PSL.Build is - Optimize_Final : Boolean := True; - - function Build_FA (N : Node) return NFA; -end PSL.Build; diff --git a/psl/psl-cse.adb b/psl/psl-cse.adb deleted file mode 100644 index 5d6f3df13..000000000 --- a/psl/psl-cse.adb +++ /dev/null @@ -1,201 +0,0 @@ -with Ada.Text_IO; -with PSL.Prints; -with Types; use Types; - -package body PSL.CSE is - function Is_X_And_Not_X (A, B : Node) return Boolean is - begin - return (Get_Kind (A) = N_Not_Bool - and then Get_Boolean (A) = B) - or else (Get_Kind (B) = N_Not_Bool - and then Get_Boolean (B) = A); - end Is_X_And_Not_X; - - type Hash_Table_Type is array (Uns32 range 0 .. 128) of Node; - Hash_Table : Hash_Table_Type := (others => Null_Node); - - function Compute_Hash (L, R : Node; Op : Uns32) return Uns32 - is - begin - return Shift_Left (Get_Hash (L), 12) - xor Shift_Left (Get_Hash (R), 2) - xor Op; - end Compute_Hash; - - function Compute_Hash (L: Node; Op : Uns32) return Uns32 - is - begin - return Shift_Left (Get_Hash (L), 2) xor Op; - end Compute_Hash; - - procedure Dump_Hash_Table (Level : Natural := 0) - is - use Ada.Text_IO; - Cnt : Natural; - Total : Natural; - N : Node; - begin - Total := 0; - for I in Hash_Table_Type'Range loop - Cnt := 0; - N := Hash_Table (I); - while N /= Null_Node loop - Cnt := Cnt + 1; - N := Get_Hash_Link (N); - end loop; - Put_Line ("Hash_table(" & Uns32'Image (I) - & "):" & Natural'Image (Cnt)); - Total := Total + Cnt; - if Level > 0 then - Cnt := 0; - N := Hash_Table (I); - while N /= Null_Node loop - Put (Uns32'Image (Get_Hash (N))); - if Level > 1 then - Put (": "); - PSL.Prints.Dump_Expr (N); - New_Line; - end if; - Cnt := Cnt + 1; - N := Get_Hash_Link (N); - end loop; - if Level = 1 and then Cnt > 0 then - New_Line; - end if; - end if; - end loop; - Put_Line ("Total:" & Natural'Image (Total)); - end Dump_Hash_Table; - - function Build_Bool_And (L, R : Node) return Node - is - R1 : Node; - Res : Node; - Hash : Uns32; - Head, H : Node; - begin - if L = True_Node then - return R; - elsif R = True_Node then - return L; - elsif L = False_Node or else R = False_Node then - return False_Node; - elsif L = R then - return L; - elsif Is_X_And_Not_X (L, R) then - return False_Node; - end if; - - -- More simple optimizations. - if Get_Kind (R) = N_And_Bool then - R1 := Get_Left (R); - if L = R1 then - return R; - elsif Is_X_And_Not_X (L, R1) then - return False_Node; - end if; - end if; - - Hash := Compute_Hash (L, R, 2); - Head := Hash_Table (Hash mod Hash_Table'Length); - H := Head; - while H /= Null_Node loop - if Get_Hash (H) = Hash - and then Get_Kind (H) = N_And_Bool - and then Get_Left (H) = L - and then Get_Right (H) = R - then - return H; - end if; - H := Get_Hash_Link (H); - end loop; - - Res := Create_Node (N_And_Bool); - Set_Left (Res, L); - Set_Right (Res, R); - Set_Hash_Link (Res, Head); - Set_Hash (Res, Hash); - Hash_Table (Hash mod Hash_Table'Length) := Res; - return Res; - end Build_Bool_And; - - function Build_Bool_Or (L, R : Node) return Node - is - Res : Node; - Hash : Uns32; - Head, H : Node; - begin - if L = True_Node then - return L; - elsif R = True_Node then - return R; - elsif L = False_Node then - return R; - elsif R = False_Node then - return L; - elsif L = R then - return L; - elsif Is_X_And_Not_X (L, R) then - return True_Node; - end if; - - Hash := Compute_Hash (L, R, 3); - Head := Hash_Table (Hash mod Hash_Table'Length); - H := Head; - while H /= Null_Node loop - if Get_Hash (H) = Hash - and then Get_Kind (H) = N_Or_Bool - and then Get_Left (H) = L - and then Get_Right (H) = R - then - return H; - end if; - H := Get_Hash_Link (H); - end loop; - - Res := Create_Node (N_Or_Bool); - Set_Left (Res, L); - Set_Right (Res, R); - Set_Hash_Link (Res, Head); - Set_Hash (Res, Hash); - Hash_Table (Hash mod Hash_Table'Length) := Res; - return Res; - end Build_Bool_Or; - - function Build_Bool_Not (N : Node) return Node is - Res : Node; - Hash : Uns32; - Head : Node; - H : Node; - begin - if N = True_Node then - return False_Node; - elsif N = False_Node then - return True_Node; - elsif Get_Kind (N) = N_Not_Bool then - return Get_Boolean (N); - end if; - - -- Find in hash table. - Hash := Compute_Hash (N, 1); - Head := Hash_Table (Hash mod Hash_Table'Length); - H := Head; - while H /= Null_Node loop - if Get_Hash (H) = Hash - and then Get_Kind (H) = N_Not_Bool - and then Get_Boolean (H) = N - then - return H; - end if; - H := Get_Hash_Link (H); - end loop; - - Res := Create_Node (N_Not_Bool); - Set_Boolean (Res, N); - Set_Hash_Link (Res, Head); - Set_Hash (Res, Hash); - Hash_Table (Hash mod Hash_Table'Length) := Res; - - return Res; - end Build_Bool_Not; -end PSL.CSE; diff --git a/psl/psl-cse.ads b/psl/psl-cse.ads deleted file mode 100644 index e40b0eeb2..000000000 --- a/psl/psl-cse.ads +++ /dev/null @@ -1,10 +0,0 @@ -with PSL.Nodes; use PSL.Nodes; - -package PSL.CSE is - -- Build boolean expressions while trying to make the node uniq. - function Build_Bool_And (L, R : Node) return Node; - function Build_Bool_Or (L, R : Node) return Node; - function Build_Bool_Not (N : Node) return Node; - - procedure Dump_Hash_Table (Level : Natural := 0); -end PSL.CSE; diff --git a/psl/psl-disp_nfas.adb b/psl/psl-disp_nfas.adb deleted file mode 100644 index c8f1532b9..000000000 --- a/psl/psl-disp_nfas.adb +++ /dev/null @@ -1,111 +0,0 @@ -with Ada.Text_IO; use Ada.Text_IO; -with Types; use Types; -with PSL.Prints; use PSL.Prints; - -package body PSL.Disp_NFAs is - procedure Disp_State (S : NFA_State) is - Str : constant String := Int32'Image (Get_State_Label (S)); - begin - Put (Str (2 .. Str'Last)); - end Disp_State; - - procedure Disp_Head (Name : String) is - begin - Put ("digraph "); - Put (Name); - Put_Line (" {"); - Put_Line (" rankdir=LR;"); - end Disp_Head; - - procedure Disp_Tail is - begin - Put_Line ("}"); - end Disp_Tail; - - procedure Disp_Body (N : NFA) is - S, F : NFA_State; - T : NFA_Edge; - begin - S := Get_Start_State (N); - F := Get_Final_State (N); - if S /= No_State then - if S = F then - Put (" node [shape = doublecircle, style = bold];"); - else - Put (" node [shape = circle, style = bold];"); - end if; - Put (" /* Start: */ "); - Disp_State (S); - Put_Line (";"); - end if; - if F /= No_State and then F /= S then - Put (" node [shape = doublecircle, style = solid];"); - Put (" /* Final: */ "); - Disp_State (F); - Put_Line (";"); - end if; - Put_Line (" node [shape = circle, style = solid];"); - - if Get_Epsilon_NFA (N) then - Put (" "); - Disp_State (Get_Start_State (N)); - Put (" -> "); - Disp_State (Get_Final_State (N)); - Put_Line (" [ label = ""*""]"); - end if; - - S := Get_First_State (N); - while S /= No_State loop - T := Get_First_Src_Edge (S); - if T = No_Edge then - if Get_First_Dest_Edge (S) = No_Edge then - Put (" "); - Disp_State (S); - Put_Line (";"); - end if; - else - loop - Put (" "); - Disp_State (S); - Put (" -> "); - Disp_State (Get_Edge_Dest (T)); - Put (" [ label = """); - Print_Expr (Get_Edge_Expr (T)); - Put ('"'); - if True then - Put (" /* Node ="); - Put (Node'Image (Get_Edge_Expr (T))); - Put (" */"); - end if; - if True then - Put (" /* Edge ="); - Put (NFA_Edge'Image (T)); - Put (" */"); - end if; - Put_Line (" ];"); - - T := Get_Next_Src_Edge (T); - exit when T = No_Edge; - end loop; - end if; - S := Get_Next_State (S); - end loop; - end Disp_Body; - - procedure Disp_NFA (N : NFA; Name : String := "nfa") is - begin - Disp_Head (Name); - Disp_Body (N); - Disp_Tail; - end Disp_NFA; - - procedure Debug_NFA (N : NFA) is - begin - Labelize_States_Debug (N); - Disp_Head ("nfa"); - Disp_Body (N); - Disp_Tail; - end Debug_NFA; - - pragma Unreferenced (Debug_NFA); -end PSL.Disp_NFAs; diff --git a/psl/psl-disp_nfas.ads b/psl/psl-disp_nfas.ads deleted file mode 100644 index 901eed72f..000000000 --- a/psl/psl-disp_nfas.ads +++ /dev/null @@ -1,12 +0,0 @@ -with PSL.NFAs; use PSL.NFAs; -with PSL.Nodes; use PSL.Nodes; - -package PSL.Disp_NFAs is - procedure Disp_Head (Name : String); - procedure Disp_Tail; - procedure Disp_Body (N : NFA); - - procedure Disp_State (S : NFA_State); - - procedure Disp_NFA (N : NFA; Name : String := "nfa"); -end PSL.Disp_NFAs; diff --git a/psl/psl-dump_tree.adb b/psl/psl-dump_tree.adb deleted file mode 100644 index db636dbb0..000000000 --- a/psl/psl-dump_tree.adb +++ /dev/null @@ -1,867 +0,0 @@ --- This is in fact -*- Ada -*- -with Ada.Text_IO; use Ada.Text_IO; -with Types; use Types; -with Name_Table; -with PSL.Errors; - -package body PSL.Dump_Tree is - - procedure Disp_Indent (Indent : Natural) is - begin - Put (String'(1 .. 2 * Indent => ' ')); - end Disp_Indent; - - Hex_Digits : constant array (Integer range 0 .. 15) of Character - := "0123456789abcdef"; - - procedure Disp_Uns32 (Val : Uns32) - is - Res : String (1 .. 8); - V : Uns32 := Val; - begin - for I in reverse Res'Range loop - Res (I) := Hex_Digits (Integer (V mod 16)); - V := V / 16; - end loop; - Put (Res); - end Disp_Uns32; - - procedure Disp_Int32 (Val : Int32) - is - Res : String (1 .. 8); - V : Int32 := Val; - begin - for I in reverse Res'Range loop - Res (I) := Hex_Digits (Integer (V mod 16)); - V := V / 16; - end loop; - Put (Res); - end Disp_Int32; - - procedure Disp_HDL_Node (Val : HDL_Node) - is - begin - if Dump_Hdl_Node /= null then - Dump_Hdl_Node.all (Val); - else - Disp_Int32 (Val); - end if; - end Disp_HDL_Node; - - procedure Disp_Node_Number (N : Node) is - begin - Put ('['); - Disp_Int32 (Int32 (N)); - Put (']'); - end Disp_Node_Number; - - procedure Disp_NFA (Val : NFA) is - begin - Disp_Int32 (Int32 (Val)); - end Disp_NFA; - - procedure Disp_Header (Msg : String; Indent : Natural) is - begin - Disp_Indent (Indent); - Put (Msg); - Put (": "); - end Disp_Header; - - procedure Disp_Identifier (N : Node) is - begin - Put (Name_Table.Image (Get_Identifier (N))); - New_Line; - end Disp_Identifier; - - procedure Disp_Label (N : Node) is - begin - Put (Name_Table.Image (Get_Label (N))); - New_Line; - end Disp_Label; - - procedure Disp_Boolean (Val : Boolean) is - begin - if Val then - Put ("true"); - else - Put ("false"); - end if; - end Disp_Boolean; - - procedure Disp_PSL_Presence_Kind (Pres : PSL_Presence_Kind) is - begin - case Pres is - when Present_Pos => - Put ('+'); - when Present_Neg => - Put ('-'); - when Present_Unknown => - Put ('?'); - end case; - end Disp_PSL_Presence_Kind; - - procedure Disp_Location (Loc : Location_Type) is - begin - Put (PSL.Errors.Get_Location_Str (Loc)); - end Disp_Location; - --- procedure Disp_String_Id (N : Node) is --- begin --- Put ('"'); --- Put (Str_Table.Image (Get_String_Id (N))); --- Put ('"'); --- New_Line; --- end Disp_String_Id; - - -- Subprograms. - procedure Disp_Tree (N : Node; Indent : Natural; Full : boolean := False) is - begin - Disp_Indent (Indent); - Disp_Node_Number (N); - Put (": "); - if N = Null_Node then - Put_Line ("*NULL*"); - return; - end if; - Put_Line (Nkind'Image (Get_Kind (N))); - Disp_Indent (Indent); - Put ("loc: "); - Disp_Location (Get_Location (N)); - New_Line; - case Get_Kind (N) is - when N_Error => - if not Full then - return; - end if; - null; - when N_Vmode => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Instance", Indent + 1); - New_Line; - Disp_Tree (Get_Instance (N), Indent + 1, Full); - Disp_Header ("Item_Chain", Indent + 1); - New_Line; - Disp_Tree (Get_Item_Chain (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Vunit => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Instance", Indent + 1); - New_Line; - Disp_Tree (Get_Instance (N), Indent + 1, Full); - Disp_Header ("Item_Chain", Indent + 1); - New_Line; - Disp_Tree (Get_Item_Chain (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Vprop => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Instance", Indent + 1); - New_Line; - Disp_Tree (Get_Instance (N), Indent + 1, Full); - Disp_Header ("Item_Chain", Indent + 1); - New_Line; - Disp_Tree (Get_Item_Chain (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Hdl_Mod_Name => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Prefix", Indent + 1); - New_Line; - Disp_Tree (Get_Prefix (N), Indent + 1, Full); - null; - when N_Assert_Directive => - Disp_Header ("Label", Indent + 1); - Disp_Label (N); - if not Full then - return; - end if; - Disp_Header ("String", Indent + 1); - New_Line; - Disp_Tree (Get_String (N), Indent + 1, Full); - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("NFA", Indent + 1); - Disp_NFA (Get_NFA (N)); - New_Line; - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Property_Declaration => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Global_Clock", Indent + 1); - New_Line; - Disp_Tree (Get_Global_Clock (N), Indent + 1, Full); - Disp_Header ("Parameter_List", Indent + 1); - New_Line; - Disp_Tree (Get_Parameter_List (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Sequence_Declaration => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Parameter_List", Indent + 1); - New_Line; - Disp_Tree (Get_Parameter_List (N), Indent + 1, Full); - Disp_Header ("Sequence", Indent + 1); - New_Line; - Disp_Tree (Get_Sequence (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Endpoint_Declaration => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Parameter_List", Indent + 1); - New_Line; - Disp_Tree (Get_Parameter_List (N), Indent + 1, Full); - Disp_Header ("Sequence", Indent + 1); - New_Line; - Disp_Tree (Get_Sequence (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Const_Parameter => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Actual", Indent + 1); - New_Line; - Disp_Tree (Get_Actual (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Boolean_Parameter => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Actual", Indent + 1); - New_Line; - Disp_Tree (Get_Actual (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Property_Parameter => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Actual", Indent + 1); - New_Line; - Disp_Tree (Get_Actual (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Sequence_Parameter => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Actual", Indent + 1); - New_Line; - Disp_Tree (Get_Actual (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Sequence_Instance => - if not Full then - return; - end if; - Disp_Header ("Declaration", Indent + 1); - New_Line; - Disp_Tree (Get_Declaration (N), Indent + 1, False); - Disp_Header ("Association_Chain", Indent + 1); - New_Line; - Disp_Tree (Get_Association_Chain (N), Indent + 1, Full); - null; - when N_Endpoint_Instance => - if not Full then - return; - end if; - Disp_Header ("Declaration", Indent + 1); - New_Line; - Disp_Tree (Get_Declaration (N), Indent + 1, False); - Disp_Header ("Association_Chain", Indent + 1); - New_Line; - Disp_Tree (Get_Association_Chain (N), Indent + 1, Full); - null; - when N_Property_Instance => - if not Full then - return; - end if; - Disp_Header ("Declaration", Indent + 1); - New_Line; - Disp_Tree (Get_Declaration (N), Indent + 1, False); - Disp_Header ("Association_Chain", Indent + 1); - New_Line; - Disp_Tree (Get_Association_Chain (N), Indent + 1, Full); - null; - when N_Actual => - if not Full then - return; - end if; - Disp_Header ("Actual", Indent + 1); - New_Line; - Disp_Tree (Get_Actual (N), Indent + 1, Full); - Disp_Header ("Formal", Indent + 1); - New_Line; - Disp_Tree (Get_Formal (N), Indent + 1, Full); - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Clock_Event => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Boolean", Indent + 1); - New_Line; - Disp_Tree (Get_Boolean (N), Indent + 1, Full); - null; - when N_Always => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - null; - when N_Never => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - null; - when N_Eventually => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - null; - when N_Strong => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - null; - when N_Imp_Seq => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Sequence", Indent + 1); - New_Line; - Disp_Tree (Get_Sequence (N), Indent + 1, Full); - null; - when N_Overlap_Imp_Seq => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Sequence", Indent + 1); - New_Line; - Disp_Tree (Get_Sequence (N), Indent + 1, Full); - null; - when N_Log_Imp_Prop => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_Next => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Strong_Flag", Indent + 1); - Disp_Boolean (Get_Strong_Flag (N)); - New_Line; - Disp_Header ("Number", Indent + 1); - New_Line; - Disp_Tree (Get_Number (N), Indent + 1, Full); - null; - when N_Next_A => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Strong_Flag", Indent + 1); - Disp_Boolean (Get_Strong_Flag (N)); - New_Line; - Disp_Header ("Low_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); - Disp_Header ("High_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_High_Bound (N), Indent + 1, Full); - null; - when N_Next_E => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Strong_Flag", Indent + 1); - Disp_Boolean (Get_Strong_Flag (N)); - New_Line; - Disp_Header ("Low_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); - Disp_Header ("High_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_High_Bound (N), Indent + 1, Full); - null; - when N_Next_Event => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Boolean", Indent + 1); - New_Line; - Disp_Tree (Get_Boolean (N), Indent + 1, Full); - Disp_Header ("Strong_Flag", Indent + 1); - Disp_Boolean (Get_Strong_Flag (N)); - New_Line; - Disp_Header ("Number", Indent + 1); - New_Line; - Disp_Tree (Get_Number (N), Indent + 1, Full); - null; - when N_Next_Event_A => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Boolean", Indent + 1); - New_Line; - Disp_Tree (Get_Boolean (N), Indent + 1, Full); - Disp_Header ("Strong_Flag", Indent + 1); - Disp_Boolean (Get_Strong_Flag (N)); - New_Line; - Disp_Header ("Low_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); - Disp_Header ("High_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_High_Bound (N), Indent + 1, Full); - null; - when N_Next_Event_E => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Boolean", Indent + 1); - New_Line; - Disp_Tree (Get_Boolean (N), Indent + 1, Full); - Disp_Header ("Strong_Flag", Indent + 1); - Disp_Boolean (Get_Strong_Flag (N)); - New_Line; - Disp_Header ("Low_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); - Disp_Header ("High_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_High_Bound (N), Indent + 1, Full); - null; - when N_Abort => - if not Full then - return; - end if; - Disp_Header ("Property", Indent + 1); - New_Line; - Disp_Tree (Get_Property (N), Indent + 1, Full); - Disp_Header ("Boolean", Indent + 1); - New_Line; - Disp_Tree (Get_Boolean (N), Indent + 1, Full); - null; - when N_Until => - if not Full then - return; - end if; - Disp_Header ("Strong_Flag", Indent + 1); - Disp_Boolean (Get_Strong_Flag (N)); - New_Line; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - Disp_Header ("Inclusive_Flag", Indent + 1); - Disp_Boolean (Get_Inclusive_Flag (N)); - New_Line; - null; - when N_Before => - if not Full then - return; - end if; - Disp_Header ("Strong_Flag", Indent + 1); - Disp_Boolean (Get_Strong_Flag (N)); - New_Line; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - Disp_Header ("Inclusive_Flag", Indent + 1); - Disp_Boolean (Get_Inclusive_Flag (N)); - New_Line; - null; - when N_Or_Prop => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_And_Prop => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_Braced_SERE => - if not Full then - return; - end if; - Disp_Header ("SERE", Indent + 1); - New_Line; - Disp_Tree (Get_SERE (N), Indent + 1, Full); - null; - when N_Concat_SERE => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_Fusion_SERE => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_Within_SERE => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_Match_And_Seq => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_And_Seq => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_Or_Seq => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - null; - when N_Star_Repeat_Seq => - if not Full then - return; - end if; - Disp_Header ("Sequence", Indent + 1); - New_Line; - Disp_Tree (Get_Sequence (N), Indent + 1, Full); - Disp_Header ("Low_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); - Disp_Header ("High_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_High_Bound (N), Indent + 1, Full); - null; - when N_Goto_Repeat_Seq => - if not Full then - return; - end if; - Disp_Header ("Sequence", Indent + 1); - New_Line; - Disp_Tree (Get_Sequence (N), Indent + 1, Full); - Disp_Header ("Low_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); - Disp_Header ("High_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_High_Bound (N), Indent + 1, Full); - null; - when N_Plus_Repeat_Seq => - if not Full then - return; - end if; - Disp_Header ("Sequence", Indent + 1); - New_Line; - Disp_Tree (Get_Sequence (N), Indent + 1, Full); - null; - when N_Equal_Repeat_Seq => - if not Full then - return; - end if; - Disp_Header ("Sequence", Indent + 1); - New_Line; - Disp_Tree (Get_Sequence (N), Indent + 1, Full); - Disp_Header ("Low_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); - Disp_Header ("High_Bound", Indent + 1); - New_Line; - Disp_Tree (Get_High_Bound (N), Indent + 1, Full); - null; - when N_Not_Bool => - if not Full then - return; - end if; - Disp_Header ("Boolean", Indent + 1); - New_Line; - Disp_Tree (Get_Boolean (N), Indent + 1, Full); - Disp_Header ("Presence", Indent + 1); - Disp_PSL_Presence_Kind (Get_Presence (N)); - New_Line; - Disp_Header ("Hash", Indent + 1); - Disp_Uns32 (Get_Hash (N)); - New_Line; - Disp_Header ("Hash_Link", Indent + 1); - New_Line; - Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); - null; - when N_And_Bool => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - Disp_Header ("Presence", Indent + 1); - Disp_PSL_Presence_Kind (Get_Presence (N)); - New_Line; - Disp_Header ("Hash", Indent + 1); - Disp_Uns32 (Get_Hash (N)); - New_Line; - Disp_Header ("Hash_Link", Indent + 1); - New_Line; - Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); - null; - when N_Or_Bool => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - Disp_Header ("Presence", Indent + 1); - Disp_PSL_Presence_Kind (Get_Presence (N)); - New_Line; - Disp_Header ("Hash", Indent + 1); - Disp_Uns32 (Get_Hash (N)); - New_Line; - Disp_Header ("Hash_Link", Indent + 1); - New_Line; - Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); - null; - when N_Imp_Bool => - if not Full then - return; - end if; - Disp_Header ("Left", Indent + 1); - New_Line; - Disp_Tree (Get_Left (N), Indent + 1, Full); - Disp_Header ("Right", Indent + 1); - New_Line; - Disp_Tree (Get_Right (N), Indent + 1, Full); - Disp_Header ("Presence", Indent + 1); - Disp_PSL_Presence_Kind (Get_Presence (N)); - New_Line; - Disp_Header ("Hash", Indent + 1); - Disp_Uns32 (Get_Hash (N)); - New_Line; - Disp_Header ("Hash_Link", Indent + 1); - New_Line; - Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); - null; - when N_HDL_Expr => - if not Full then - return; - end if; - Disp_Header ("Presence", Indent + 1); - Disp_PSL_Presence_Kind (Get_Presence (N)); - New_Line; - Disp_Header ("HDL_Node", Indent + 1); - Disp_HDL_Node (Get_HDL_Node (N)); - New_Line; - Disp_Header ("HDL_Index", Indent + 1); - Disp_Int32 (Get_HDL_Index (N)); - New_Line; - Disp_Header ("Hash", Indent + 1); - Disp_Uns32 (Get_Hash (N)); - New_Line; - Disp_Header ("Hash_Link", Indent + 1); - New_Line; - Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); - null; - when N_False => - if not Full then - return; - end if; - null; - when N_True => - if not Full then - return; - end if; - null; - when N_EOS => - if not Full then - return; - end if; - Disp_Header ("HDL_Index", Indent + 1); - Disp_Int32 (Get_HDL_Index (N)); - New_Line; - Disp_Header ("Hash", Indent + 1); - Disp_Uns32 (Get_Hash (N)); - New_Line; - Disp_Header ("Hash_Link", Indent + 1); - New_Line; - Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); - null; - when N_Name => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Header ("Decl", Indent + 1); - New_Line; - Disp_Tree (Get_Decl (N), Indent + 1, Full); - null; - when N_Name_Decl => - Disp_Header ("Identifier", Indent + 1); - Disp_Identifier (N); - if not Full then - return; - end if; - Disp_Tree (Get_Chain (N), Indent, Full); - null; - when N_Number => - if not Full then - return; - end if; - Disp_Header ("Value", Indent + 1); - Disp_Uns32 (Get_Value (N)); - New_Line; - null; - end case; - end Disp_Tree; - - procedure Dump_Tree (N : Node; Full : Boolean := False) is - begin - Disp_Tree (N, 0, Full); - end Dump_Tree; - -end PSL.Dump_Tree; diff --git a/psl/psl-dump_tree.ads b/psl/psl-dump_tree.ads deleted file mode 100644 index f8b2eb3ab..000000000 --- a/psl/psl-dump_tree.ads +++ /dev/null @@ -1,9 +0,0 @@ -with PSL.Nodes; use PSL.Nodes; - -package PSL.Dump_Tree is - procedure Dump_Tree (N : Node; Full : Boolean := False); - - -- Procedure to dump an HDL node. - type Dump_Hdl_Node_Acc is access procedure (N : HDL_Node); - Dump_Hdl_Node : Dump_Hdl_Node_Acc := null; -end PSL.Dump_Tree; diff --git a/psl/psl-hash.adb b/psl/psl-hash.adb deleted file mode 100644 index 62744b336..000000000 --- a/psl/psl-hash.adb +++ /dev/null @@ -1,60 +0,0 @@ -with GNAT.Table; - -package body PSL.Hash is - - type Index_Type is new Natural; - No_Index : constant Index_Type := 0; - - type Cell_Record is record - Res : Node; - Next : Index_Type; - end record; - - Hash_Size : constant Index_Type := 127; - - package Cells is new GNAT.Table - (Table_Component_Type => Cell_Record, - Table_Index_Type => Index_Type, - Table_Low_Bound => 0, - Table_Initial => 256, - Table_Increment => 100); - - procedure Init is - begin - Cells.Set_Last (Hash_Size - 1); - for I in 0 .. Hash_Size - 1 loop - Cells.Table (I) := (Res => Null_Node, Next => No_Index); - end loop; - end Init; - - function Get_PSL_Node (Hdl : Int32) return Node is - Idx : Index_Type := Index_Type (Hdl mod Int32 (Hash_Size)); - N_Idx : Index_Type; - Res : Node; - begin - -- In the primary table. - Res := Cells.Table (Idx).Res; - if Res = Null_Node then - Res := Create_Node (N_HDL_Expr); - Set_HDL_Node (Res, Hdl); - Cells.Table (Idx).Res := Res; - return Res; - end if; - - loop - if Get_HDL_Node (Res) = Hdl then - return Res; - end if; - -- Look in collisions chain - N_Idx := Cells.Table (Idx).Next; - exit when N_Idx = No_Index; - Idx := N_Idx; - Res := Cells.Table (Idx).Res; - end loop; - Res := Create_Node (N_HDL_Expr); - Set_HDL_Node (Res, Hdl); - Cells.Append ((Res => Res, Next => No_Index)); - Cells.Table (Idx).Next := Cells.Last; - return Res; - end Get_PSL_Node; -end PSL.Hash; diff --git a/psl/psl-hash.ads b/psl/psl-hash.ads deleted file mode 100644 index d1a60c971..000000000 --- a/psl/psl-hash.ads +++ /dev/null @@ -1,11 +0,0 @@ -with Types; use Types; -with PSL.Nodes; use PSL.Nodes; - -package PSL.Hash is - -- Initialize the package. - procedure Init; - - -- Get the PSL node for node HDL. - -- Only one PSL node is created for an HDL node. - function Get_PSL_Node (Hdl : Int32) return Node; -end PSL.Hash; diff --git a/psl/psl-nfas-utils.adb b/psl/psl-nfas-utils.adb deleted file mode 100644 index 06601850d..000000000 --- a/psl/psl-nfas-utils.adb +++ /dev/null @@ -1,330 +0,0 @@ -with PSL.Errors; use PSL.Errors; - -package body PSL.NFAs.Utils is - generic - with function Get_First_Edge (S : NFA_State) return NFA_Edge; - with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; - with procedure Set_First_Edge (S : NFA_State; E : NFA_Edge); - with procedure Set_Next_Edge (E : NFA_Edge; N_E : NFA_Edge); - with function Get_Edge_State (E : NFA_Edge) return NFA_State; - package Sort_Edges is - procedure Sort_Edges (S : NFA_State); - procedure Sort_Edges (N : NFA); - end Sort_Edges; - - package body Sort_Edges is - -- Use merge sort to sort a list of edges. - -- The first edge is START and the list has LEN edges. - -- RES is the head of the sorted list. - -- NEXT_EDGE is the LEN + 1 edge (not sorted). - procedure Edges_Merge_Sort (Start : NFA_Edge; - Len : Natural; - Res : out NFA_Edge; - Next_Edge : out NFA_Edge) - is - function Lt (L, R : NFA_Edge) return Boolean - is - L_Expr : constant Node := Get_Edge_Expr (L); - R_Expr : constant Node := Get_Edge_Expr (R); - begin - return L_Expr < R_Expr - or else (L_Expr = R_Expr - and then Get_Edge_State (L) < Get_Edge_State (R)); - end Lt; - - pragma Inline (Lt); - - Half : constant Natural := Len / 2; - Left_Start, Right_Start : NFA_Edge; - Left_Next, Right_Next : NFA_Edge; - L, R : NFA_Edge; - Last, E : NFA_Edge; - begin - -- With less than 2 elements, the sort is trivial. - if Len < 2 then - if Len = 0 then - Next_Edge := Start; - else - Next_Edge := Get_Next_Edge (Start); - end if; - Res := Start; - return; - end if; - - -- Sort each half. - Edges_Merge_Sort (Start, Half, Left_Start, Left_Next); - Edges_Merge_Sort (Left_Next, Len - Half, Right_Start, Right_Next); - - -- Merge. - L := Left_Start; - R := Right_Start; - Last := No_Edge; - loop - -- Take from left iff: - -- * it is not empty - -- * right is empty or else (left < right) - if L /= Left_Next and then (R = Right_Next or else Lt (L, R)) then - E := L; - L := Get_Next_Edge (L); - - -- Take from right if right is not empty. - elsif R /= Right_Next then - E := R; - R := Get_Next_Edge (R); - - -- Both left are right are empty. - else - exit; - end if; - - if Last = No_Edge then - Res := E; - else - Set_Next_Edge (Last, E); - end if; - Last := E; - end loop; - -- Let the link clean. - Next_Edge := Right_Next; - Set_Next_Edge (Last, Next_Edge); - end Edges_Merge_Sort; - - procedure Sort_Edges (S : NFA_State) - is - Nbr_Edges : Natural; - First_E, E, Res : NFA_Edge; - begin - -- Count number of edges. - Nbr_Edges := 0; - First_E := Get_First_Edge (S); - E := First_E; - while E /= No_Edge loop - Nbr_Edges := Nbr_Edges + 1; - E := Get_Next_Edge (E); - end loop; - - -- Sort edges by expression. - Edges_Merge_Sort (First_E, Nbr_Edges, Res, E); - pragma Assert (E = No_Edge); - Set_First_Edge (S, Res); - - end Sort_Edges; - - procedure Sort_Edges (N : NFA) - is - S : NFA_State; - begin - -- Iterate on states. - S := Get_First_State (N); - while S /= No_State loop - Sort_Edges (S); - S := Get_Next_State (S); - end loop; - end Sort_Edges; - end Sort_Edges; - - package Sort_Src_Edges_Pkg is new - Sort_Edges (Get_First_Edge => Get_First_Src_Edge, - Get_Next_Edge => Get_Next_Src_Edge, - Set_First_Edge => Set_First_Src_Edge, - Set_Next_Edge => Set_Next_Src_Edge, - Get_Edge_State => Get_Edge_Dest); - - procedure Sort_Src_Edges (S : NFA_State) renames - Sort_Src_Edges_Pkg.Sort_Edges; - procedure Sort_Src_Edges (N : NFA) renames - Sort_Src_Edges_Pkg.Sort_Edges; - - package Sort_Dest_Edges_Pkg is new - Sort_Edges (Get_First_Edge => Get_First_Dest_Edge, - Get_Next_Edge => Get_Next_Dest_Edge, - Set_First_Edge => Set_First_Dest_Edge, - Set_Next_Edge => Set_Next_Dest_Edge, - Get_Edge_State => Get_Edge_Src); - - procedure Sort_Dest_Edges (S : NFA_State) renames - Sort_Dest_Edges_Pkg.Sort_Edges; - procedure Sort_Dest_Edges (N : NFA) renames - Sort_Dest_Edges_Pkg.Sort_Edges; - - generic - with function Get_First_Edge_Reverse (S : NFA_State) return NFA_Edge; - with function Get_First_Edge (S : NFA_State) return NFA_Edge; - with procedure Set_First_Edge (S : NFA_State; E : NFA_Edge); - with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; - with procedure Set_Next_Edge (E : NFA_Edge; E1 : NFA_Edge); - with procedure Set_Edge_State (E : NFA_Edge; S : NFA_State); - procedure Merge_State (N : NFA; S : NFA_State; S1 : NFA_State); - - procedure Merge_State (N : NFA; S : NFA_State; S1 : NFA_State) - is - E, First_E, Next_E : NFA_Edge; - begin - pragma Assert (S /= S1); - - -- Discard outgoing edges of S1. - loop - E := Get_First_Edge_Reverse (S1); - exit when E = No_Edge; - Remove_Edge (E); - end loop; - - -- Prepend incoming edges of S1 to S. - First_E := Get_First_Edge (S); - E := Get_First_Edge (S1); - while E /= No_Edge loop - Next_E := Get_Next_Edge (E); - Set_Next_Edge (E, First_E); - Set_Edge_State (E, S); - First_E := E; - E := Next_E; - end loop; - Set_First_Edge (S, First_E); - Set_First_Edge (S1, No_Edge); - - Remove_State (N, S1); - end Merge_State; - - procedure Merge_State_Dest_1 is new Merge_State - (Get_First_Edge_Reverse => Get_First_Src_Edge, - Get_First_Edge => Get_First_Dest_Edge, - Set_First_Edge => Set_First_Dest_Edge, - Get_Next_Edge => Get_Next_Dest_Edge, - Set_Next_Edge => Set_Next_Dest_Edge, - Set_Edge_State => Set_Edge_Dest); - - procedure Merge_State_Dest (N : NFA; S : NFA_State; S1 : NFA_State) renames - Merge_State_Dest_1; - - procedure Merge_State_Src_1 is new Merge_State - (Get_First_Edge_Reverse => Get_First_Dest_Edge, - Get_First_Edge => Get_First_Src_Edge, - Set_First_Edge => Set_First_Src_Edge, - Get_Next_Edge => Get_Next_Src_Edge, - Set_Next_Edge => Set_Next_Src_Edge, - Set_Edge_State => Set_Edge_Src); - - procedure Merge_State_Src (N : NFA; S : NFA_State; S1 : NFA_State) renames - Merge_State_Src_1; - - procedure Sort_Outgoing_Edges (N : NFA; Nbr_States : Natural) - is - Last_State : constant NFA_State := NFA_State (Nbr_States) - 1; - type Edge_Array is array (0 .. Last_State) of NFA_Edge; - Edges : Edge_Array := (others => No_Edge); - S, D : NFA_State; - E, Next_E : NFA_Edge; - First_Edge, Last_Edge : NFA_Edge; - begin - -- Iterate on states. - S := Get_First_State (N); - while S /= No_State loop - - -- Create an array of edges - E := Get_First_Dest_Edge (S); - while E /= No_Edge loop - Next_E := Get_Next_Dest_Edge (E); - D := Get_Edge_Dest (E); - if Edges (D) /= No_Edge then - -- TODO: merge edges. - raise Program_Error; - end if; - Edges (D) := E; - E := Next_E; - end loop; - - -- Rebuild the edge list (sorted by destination). - Last_Edge := No_Edge; - First_Edge := No_Edge; - for I in Edge_Array'Range loop - E := Edges (I); - if E /= No_Edge then - Edges (I) := No_Edge; - if First_Edge = No_Edge then - First_Edge := E; - else - Set_Next_Dest_Edge (Last_Edge, E); - end if; - Last_Edge := E; - end if; - end loop; - Set_First_Dest_Edge (S, First_Edge); - S := Get_Next_State (S); - end loop; - end Sort_Outgoing_Edges; - pragma Unreferenced (Sort_Outgoing_Edges); - - generic - with function Get_First_Edge (S : NFA_State) return NFA_Edge; - with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; - with function Get_State_Reverse (E : NFA_Edge) return NFA_State; - with function Get_First_Edge_Reverse (S : NFA_State) return NFA_Edge; - with function Get_Next_Edge_Reverse (E : NFA_Edge) return NFA_Edge; - procedure Check_Edges_Gen (N : NFA); - - procedure Check_Edges_Gen (N : NFA) - is - S : NFA_State; - E : NFA_Edge; - R_S : NFA_State; - R_E : NFA_Edge; - begin - S := Get_First_State (N); - while S /= No_State loop - E := Get_First_Edge (S); - while E /= No_Edge loop - R_S := Get_State_Reverse (E); - R_E := Get_First_Edge_Reverse (R_S); - while R_E /= No_Edge and then R_E /= E loop - R_E := Get_Next_Edge_Reverse (R_E); - end loop; - if R_E /= E then - raise Program_Error; - end if; - E := Get_Next_Edge (E); - end loop; - S := Get_Next_State (S); - end loop; - end Check_Edges_Gen; - - procedure Check_Edges_Src is new Check_Edges_Gen - (Get_First_Edge => Get_First_Src_Edge, - Get_Next_Edge => Get_Next_Src_Edge, - Get_State_Reverse => Get_Edge_Dest, - Get_First_Edge_Reverse => Get_First_Dest_Edge, - Get_Next_Edge_Reverse => Get_Next_Dest_Edge); - - procedure Check_Edges_Dest is new Check_Edges_Gen - (Get_First_Edge => Get_First_Dest_Edge, - Get_Next_Edge => Get_Next_Dest_Edge, - Get_State_Reverse => Get_Edge_Src, - Get_First_Edge_Reverse => Get_First_Src_Edge, - Get_Next_Edge_Reverse => Get_Next_Src_Edge); - - procedure Check_NFA (N : NFA) is - begin - Check_Edges_Src (N); - Check_Edges_Dest (N); - end Check_NFA; - - function Has_EOS (N : Node) return Boolean is - begin - case Get_Kind (N) is - when N_EOS => - return True; - when N_False - | N_True - | N_HDL_Expr => - return False; - when N_Not_Bool => - return Has_EOS (Get_Boolean (N)); - when N_And_Bool - | N_Or_Bool - | N_Imp_Bool => - return Has_EOS (Get_Left (N)) or else Has_EOS (Get_Right (N)); - when others => - Error_Kind ("Has_EOS", N); - end case; - end Has_EOS; - -end PSL.NFAs.Utils; diff --git a/psl/psl-nfas-utils.ads b/psl/psl-nfas-utils.ads deleted file mode 100644 index bdbc0d013..000000000 --- a/psl/psl-nfas-utils.ads +++ /dev/null @@ -1,21 +0,0 @@ -package PSL.NFAs.Utils is - -- Sort outgoing edges by expression. - procedure Sort_Src_Edges (S : NFA_State); - procedure Sort_Src_Edges (N : NFA); - - procedure Sort_Dest_Edges (S : NFA_State); - procedure Sort_Dest_Edges (N : NFA); - - -- Move incoming edges of S1 to S, remove S1 and its outgoing edges. - procedure Merge_State_Dest (N : NFA; S : NFA_State; S1 : NFA_State); - - procedure Merge_State_Src (N : NFA; S : NFA_State; S1 : NFA_State); - - -- Return True if N or a child of N is EOS. - -- N must be a boolean expression. - function Has_EOS (N : Node) return Boolean; - - -- Raise Program_Error if N is not internally coherent. - procedure Check_NFA (N : NFA); -end PSL.NFAs.Utils; - diff --git a/psl/psl-nfas.adb b/psl/psl-nfas.adb deleted file mode 100644 index da4866e53..000000000 --- a/psl/psl-nfas.adb +++ /dev/null @@ -1,529 +0,0 @@ -with GNAT.Table; - -package body PSL.NFAs is - -- Record that describes an NFA. - type NFA_Node is record - -- Chain of States. - First_State : NFA_State; - Last_State : NFA_State; - - -- Start and final state. - Start : NFA_State; - Final : NFA_State; - - -- If true there is an epsilon transition between the start and - -- the final state. - Epsilon : Boolean; - end record; - - -- Record that describe a node. - type NFA_State_Node is record - -- States may be numbered. - Label : Int32; - - -- Edges. - First_Src : NFA_Edge; - First_Dst : NFA_Edge; - - -- State links. - Next_State : NFA_State; - Prev_State : NFA_State; - - -- User fields. - User_Link : NFA_State; - User_Flag : Boolean; - end record; - - -- Record that describe an edge between SRC and DEST. - type NFA_Edge_Node is record - Dest : NFA_State; - Src : NFA_State; - Expr : Node; - - -- Links. - Next_Src : NFA_Edge; - Next_Dst : NFA_Edge; - end record; - - -- Table of NFA. - package Nfat is new GNAT.Table - (Table_Component_Type => NFA_Node, - Table_Index_Type => NFA, - Table_Low_Bound => 1, - Table_Initial => 128, - Table_Increment => 100); - - -- List of free nodes. - Free_Nfas : NFA := No_NFA; - - -- Table of States. - package Statet is new GNAT.Table - (Table_Component_Type => NFA_State_Node, - Table_Index_Type => NFA_State, - Table_Low_Bound => 1, - Table_Initial => 128, - Table_Increment => 100); - - -- List of free states. - Free_States : NFA_State := No_State; - - -- Table of edges. - package Transt is new GNAT.Table - (Table_Component_Type => NFA_Edge_Node, - Table_Index_Type => NFA_Edge, - Table_Low_Bound => 1, - Table_Initial => 128, - Table_Increment => 100); - - -- List of free edges. - Free_Edges : NFA_Edge := No_Edge; - - function Get_First_State (N : NFA) return NFA_State is - begin - return Nfat.Table (N).First_State; - end Get_First_State; - - function Get_Last_State (N : NFA) return NFA_State is - begin - return Nfat.Table (N).Last_State; - end Get_Last_State; - - procedure Set_First_State (N : NFA; S : NFA_State) is - begin - Nfat.Table (N).First_State := S; - end Set_First_State; - - procedure Set_Last_State (N : NFA; S : NFA_State) is - begin - Nfat.Table (N).Last_State := S; - end Set_Last_State; - - function Get_Next_State (S : NFA_State) return NFA_State is - begin - return Statet.Table (S).Next_State; - end Get_Next_State; - - procedure Set_Next_State (S : NFA_State; N : NFA_State) is - begin - Statet.Table (S).Next_State := N; - end Set_Next_State; - - function Get_Prev_State (S : NFA_State) return NFA_State is - begin - return Statet.Table (S).Prev_State; - end Get_Prev_State; - - procedure Set_Prev_State (S : NFA_State; N : NFA_State) is - begin - Statet.Table (S).Prev_State := N; - end Set_Prev_State; - - function Get_State_Label (S : NFA_State) return Int32 is - begin - return Statet.Table (S).Label; - end Get_State_Label; - - procedure Set_State_Label (S : NFA_State; Label : Int32) is - begin - Statet.Table (S).Label := Label; - end Set_State_Label; - - function Get_Epsilon_NFA (N : NFA) return Boolean is - begin - return Nfat.Table (N).Epsilon; - end Get_Epsilon_NFA; - - procedure Set_Epsilon_NFA (N : NFA; Flag : Boolean) is - begin - Nfat.Table (N).Epsilon := Flag; - end Set_Epsilon_NFA; - - function Add_State (N : NFA) return NFA_State is - Res : NFA_State; - Last : NFA_State; - begin - -- Get a new state. - if Free_States = No_State then - Statet.Increment_Last; - Res := Statet.Last; - else - Res := Free_States; - Free_States := Get_Next_State (Res); - end if; - - -- Put it in N. - Last := Get_Last_State (N); - Statet.Table (Res) := (Label => 0, - First_Src => No_Edge, - First_Dst => No_Edge, - Next_State => No_State, - Prev_State => Last, - User_Link => No_State, - User_Flag => False); - if Last = No_State then - Nfat.Table (N).First_State := Res; - else - Statet.Table (Last).Next_State := Res; - end if; - Nfat.Table (N).Last_State := Res; - return Res; - end Add_State; - - procedure Delete_Detached_State (S : NFA_State) is - begin - -- Put it in front of the free_states list. - Set_Next_State (S, Free_States); - Free_States := S; - end Delete_Detached_State; - - function Create_NFA return NFA - is - Res : NFA; - begin - -- Allocate a node. - if Free_Nfas = No_NFA then - Nfat.Increment_Last; - Res := Nfat.Last; - else - Res := Free_Nfas; - Free_Nfas := NFA (Get_First_State (Res)); - end if; - - -- Fill it. - Nfat.Table (Res) := (First_State => No_State, - Last_State => No_State, - Start => No_State, Final => No_State, - Epsilon => False); - return Res; - end Create_NFA; - - procedure Set_First_Src_Edge (N : NFA_State; T : NFA_Edge) is - begin - Statet.Table (N).First_Src := T; - end Set_First_Src_Edge; - - function Get_First_Src_Edge (N : NFA_State) return NFA_Edge is - begin - return Statet.Table (N).First_Src; - end Get_First_Src_Edge; - - procedure Set_First_Dest_Edge (N : NFA_State; T : NFA_Edge) is - begin - Statet.Table (N).First_Dst := T; - end Set_First_Dest_Edge; - - function Get_First_Dest_Edge (N : NFA_State) return NFA_Edge is - begin - return Statet.Table (N).First_Dst; - end Get_First_Dest_Edge; - - function Get_State_Flag (S : NFA_State) return Boolean is - begin - return Statet.Table (S).User_Flag; - end Get_State_Flag; - - procedure Set_State_Flag (S : NFA_State; Val : Boolean) is - begin - Statet.Table (S).User_Flag := Val; - end Set_State_Flag; - - function Get_State_User_Link (S : NFA_State) return NFA_State is - begin - return Statet.Table (S).User_Link; - end Get_State_User_Link; - - procedure Set_State_User_Link (S : NFA_State; Link : NFA_State) is - begin - Statet.Table (S).User_Link := Link; - end Set_State_User_Link; - - function Add_Edge (Src : NFA_State; Dest : NFA_State; Expr : Node) - return NFA_Edge - is - Res : NFA_Edge; - begin - -- Allocate a note. - if Free_Edges /= No_Edge then - Res := Free_Edges; - Free_Edges := Get_Next_Dest_Edge (Res); - else - Transt.Increment_Last; - Res := Transt.Last; - end if; - - -- Initialize it. - Transt.Table (Res) := (Dest => Dest, - Src => Src, - Expr => Expr, - Next_Src => Get_First_Src_Edge (Src), - Next_Dst => Get_First_Dest_Edge (Dest)); - Set_First_Src_Edge (Src, Res); - Set_First_Dest_Edge (Dest, Res); - return Res; - end Add_Edge; - - procedure Add_Edge (Src : NFA_State; Dest : NFA_State; Expr : Node) is - Res : NFA_Edge; - pragma Unreferenced (Res); - begin - Res := Add_Edge (Src, Dest, Expr); - end Add_Edge; - - procedure Delete_Empty_NFA (N : NFA) is - begin - pragma Assert (Get_First_State (N) = No_State); - pragma Assert (Get_Last_State (N) = No_State); - - -- Put it in front of the free_nfas list. - Set_First_State (N, NFA_State (Free_Nfas)); - Free_Nfas := N; - end Delete_Empty_NFA; - - function Get_Start_State (N : NFA) return NFA_State is - begin - return Nfat.Table (N).Start; - end Get_Start_State; - - procedure Set_Start_State (N : NFA; S : NFA_State) is - begin - Nfat.Table (N).Start := S; - end Set_Start_State; - - function Get_Final_State (N : NFA) return NFA_State is - begin - return Nfat.Table (N).Final; - end Get_Final_State; - - procedure Set_Final_State (N : NFA; S : NFA_State) is - begin - Nfat.Table (N).Final := S; - end Set_Final_State; - - function Get_Next_Src_Edge (N : NFA_Edge) return NFA_Edge is - begin - return Transt.Table (N).Next_Src; - end Get_Next_Src_Edge; - - procedure Set_Next_Src_Edge (E : NFA_Edge; N_E : NFA_Edge) is - begin - Transt.Table (E).Next_Src := N_E; - end Set_Next_Src_Edge; - - function Get_Next_Dest_Edge (N : NFA_Edge) return NFA_Edge is - begin - return Transt.Table (N).Next_Dst; - end Get_Next_Dest_Edge; - - procedure Set_Next_Dest_Edge (E : NFA_Edge; N_E : NFA_Edge) is - begin - Transt.Table (E).Next_Dst := N_E; - end Set_Next_Dest_Edge; - - function Get_Edge_Dest (E : NFA_Edge) return NFA_State is - begin - return Transt.Table (E).Dest; - end Get_Edge_Dest; - - procedure Set_Edge_Dest (E : NFA_Edge; D : NFA_State) is - begin - Transt.Table (E).Dest := D; - end Set_Edge_Dest; - - function Get_Edge_Src (E : NFA_Edge) return NFA_State is - begin - return Transt.Table (E).Src; - end Get_Edge_Src; - - procedure Set_Edge_Src (E : NFA_Edge; D : NFA_State) is - begin - Transt.Table (E).Src := D; - end Set_Edge_Src; - - function Get_Edge_Expr (E : NFA_Edge) return Node is - begin - return Transt.Table (E).Expr; - end Get_Edge_Expr; - - procedure Set_Edge_Expr (E : NFA_Edge; N : Node) is - begin - Transt.Table (E).Expr := N; - end Set_Edge_Expr; - - procedure Remove_Unconnected_State (N : NFA; S : NFA_State) is - N_S : constant NFA_State := Get_Next_State (S); - P_S : constant NFA_State := Get_Prev_State (S); - begin - pragma Assert (Get_First_Src_Edge (S) = No_Edge); - pragma Assert (Get_First_Dest_Edge (S) = No_Edge); - - if P_S = No_State then - Set_First_State (N, N_S); - else - Set_Next_State (P_S, N_S); - end if; - if N_S = No_State then - Set_Last_State (N, P_S); - else - Set_Prev_State (N_S, P_S); - end if; - Delete_Detached_State (S); - end Remove_Unconnected_State; - - procedure Merge_NFA (L, R : NFA) is - Last_L : constant NFA_State := Get_Last_State (L); - First_R : constant NFA_State := Get_First_State (R); - Last_R : constant NFA_State := Get_Last_State (R); - begin - if First_R = No_State then - return; - end if; - if Last_L = No_State then - Set_First_State (L, First_R); - else - Set_Next_State (Last_L, First_R); - Set_Prev_State (First_R, Last_L); - end if; - Set_Last_State (L, Last_R); - Set_First_State (R, No_State); - Set_Last_State (R, No_State); - Delete_Empty_NFA (R); - end Merge_NFA; - - procedure Redest_Edges (S : NFA_State; Dest : NFA_State) is - E, N_E : NFA_Edge; - Head : NFA_Edge; - begin - E := Get_First_Dest_Edge (S); - if E = No_Edge then - return; - end if; - Set_First_Dest_Edge (S, No_Edge); - Head := Get_First_Dest_Edge (Dest); - Set_First_Dest_Edge (Dest, E); - loop - N_E := Get_Next_Dest_Edge (E); - Set_Edge_Dest (E, Dest); - exit when N_E = No_Edge; - E := N_E; - end loop; - Set_Next_Dest_Edge (E, Head); - end Redest_Edges; - - procedure Resource_Edges (S : NFA_State; Src : NFA_State) is - E, N_E : NFA_Edge; - Head : NFA_Edge; - begin - E := Get_First_Src_Edge (S); - if E = No_Edge then - return; - end if; - Set_First_Src_Edge (S, No_Edge); - Head := Get_First_Src_Edge (Src); - Set_First_Src_Edge (Src, E); - loop - N_E := Get_Next_Src_Edge (E); - Set_Edge_Src (E, Src); - exit when N_E = No_Edge; - E := N_E; - end loop; - Set_Next_Src_Edge (E, Head); - end Resource_Edges; - - procedure Disconnect_Edge_Src (N : NFA_State; E : NFA_Edge) is - N_E : constant NFA_Edge := Get_Next_Src_Edge (E); - Prev, Cur : NFA_Edge; - begin - Cur := Get_First_Src_Edge (N); - if Cur = E then - Set_First_Src_Edge (N, N_E); - else - while Cur /= E loop - Prev := Cur; - Cur := Get_Next_Src_Edge (Prev); - pragma Assert (Cur /= No_Edge); - end loop; - Set_Next_Src_Edge (Prev, N_E); - end if; - end Disconnect_Edge_Src; - - procedure Disconnect_Edge_Dest (N : NFA_State; E : NFA_Edge) is - N_E : constant NFA_Edge := Get_Next_Dest_Edge (E); - Prev, Cur : NFA_Edge; - begin - Cur := Get_First_Dest_Edge (N); - if Cur = E then - Set_First_Dest_Edge (N, N_E); - else - while Cur /= E loop - Prev := Cur; - Cur := Get_Next_Dest_Edge (Prev); - pragma Assert (Cur /= No_Edge); - end loop; - Set_Next_Dest_Edge (Prev, N_E); - end if; - end Disconnect_Edge_Dest; - - procedure Remove_Edge (E : NFA_Edge) is - begin - Disconnect_Edge_Src (Get_Edge_Src (E), E); - Disconnect_Edge_Dest (Get_Edge_Dest (E), E); - - -- Put it on the free list. - Set_Next_Dest_Edge (E, Free_Edges); - Free_Edges := E; - end Remove_Edge; - - procedure Remove_State (N : NFA; S : NFA_State) is - E, N_E : NFA_Edge; - begin - E := Get_First_Dest_Edge (S); - while E /= No_Edge loop - N_E := Get_Next_Dest_Edge (E); - Remove_Edge (E); - E := N_E; - end loop; - - E := Get_First_Src_Edge (S); - while E /= No_Edge loop - N_E := Get_Next_Src_Edge (E); - Remove_Edge (E); - E := N_E; - end loop; - - Remove_Unconnected_State (N, S); - end Remove_State; - - procedure Labelize_States (N : NFA; Nbr_States : out Natural) - is - S, Start, Final : NFA_State; - begin - S := Get_First_State (N); - Start := Get_Start_State (N); - Final := Get_Final_State (N); - pragma Assert (Start /= No_State); - Set_State_Label (Start, 0); - Nbr_States := 1; - while S /= No_State loop - if S /= Start and then S /= Final then - Set_State_Label (S, Int32 (Nbr_States)); - Nbr_States := Nbr_States + 1; - end if; - S := Get_Next_State (S); - end loop; - pragma Assert (Final /= No_State); - Set_State_Label (Final, Int32 (Nbr_States)); - Nbr_States := Nbr_States + 1; - end Labelize_States; - - procedure Labelize_States_Debug (N : NFA) - is - S : NFA_State; - begin - S := Get_First_State (N); - while S /= No_State loop - Set_State_Label (S, Int32 (S)); - S := Get_Next_State (S); - end loop; - end Labelize_States_Debug; - -end PSL.NFAs; diff --git a/psl/psl-nfas.ads b/psl/psl-nfas.ads deleted file mode 100644 index 815acf223..000000000 --- a/psl/psl-nfas.ads +++ /dev/null @@ -1,108 +0,0 @@ -with Types; use Types; -with PSL.Nodes; use PSL.Nodes; - -package PSL.NFAs is - -- Represents NFAs for PSL. - -- These NFAs have the following restrictions: - -- * 1 start state - -- * 1 final state (which can be the start state). - -- * possible epsilon transition between start and final state with the - -- meaning: A | eps - - type NFA_State is new Nat32; - type NFA_Edge is new Nat32; - - No_NFA : constant NFA := 0; - No_State : constant NFA_State := 0; - No_Edge : constant NFA_Edge := 0; - - -- Create a new NFA. - function Create_NFA return NFA; - - -- Add a new state to an NFA. - function Add_State (N : NFA) return NFA_State; - - -- Add a transition. - procedure Add_Edge (Src : NFA_State; Dest : NFA_State; Expr : Node); - function Add_Edge (Src : NFA_State; Dest : NFA_State; Expr : Node) - return NFA_Edge; - - -- Disconnect and free edge E. - procedure Remove_Edge (E : NFA_Edge); - - -- Return TRUE if there is an epsilon edge between start and final. - function Get_Epsilon_NFA (N : NFA) return Boolean; - procedure Set_Epsilon_NFA (N : NFA; Flag : Boolean); - - -- Each NFA has one start and one final state. - function Get_Start_State (N : NFA) return NFA_State; - procedure Set_Start_State (N : NFA; S : NFA_State); - - procedure Set_Final_State (N : NFA; S : NFA_State); - function Get_Final_State (N : NFA) return NFA_State; - - -- Iterate on all states. - function Get_First_State (N : NFA) return NFA_State; - function Get_Next_State (S : NFA_State) return NFA_State; - - -- Per state user flag. - -- Initialized set to false. - function Get_State_Flag (S : NFA_State) return Boolean; - procedure Set_State_Flag (S : NFA_State; Val : Boolean); - - -- Per state user link. - function Get_State_User_Link (S : NFA_State) return NFA_State; - procedure Set_State_User_Link (S : NFA_State; Link : NFA_State); - - -- Edges of a state. - -- A source edge is an edge whose source is the state. - function Get_First_Src_Edge (N : NFA_State) return NFA_Edge; - function Get_Next_Src_Edge (N : NFA_Edge) return NFA_Edge; - - -- A dest edge is an edge whose destination is the state. - function Get_First_Dest_Edge (N : NFA_State) return NFA_Edge; - function Get_Next_Dest_Edge (N : NFA_Edge) return NFA_Edge; - - function Get_State_Label (S : NFA_State) return Int32; - procedure Set_State_Label (S : NFA_State; Label : Int32); - - function Get_Edge_Dest (E: NFA_Edge) return NFA_State; - function Get_Edge_Src (E : NFA_Edge) return NFA_State; - function Get_Edge_Expr (E : NFA_Edge) return Node; - - -- Move States and edges of R to L. - procedure Merge_NFA (L, R : NFA); - - -- All edges to S are redirected to DEST. - procedure Redest_Edges (S : NFA_State; Dest : NFA_State); - - -- All edges from S are redirected from SRC. - procedure Resource_Edges (S : NFA_State; Src : NFA_State); - - -- Remove a state. The state must be unconnected. - procedure Remove_Unconnected_State (N : NFA; S : NFA_State); - - -- Deconnect and remove state S. - procedure Remove_State (N : NFA; S : NFA_State); - - procedure Delete_Empty_NFA (N : NFA); - - -- Set a label on the states of the NFA N. - -- Start state is has label 0. - -- Return the number of states. - procedure Labelize_States (N : NFA; Nbr_States : out Natural); - - -- Set state index as state label. - -- Used to debug an NFA. - procedure Labelize_States_Debug (N : NFA); - - procedure Set_Edge_Expr (E : NFA_Edge; N : Node); -private - -- Low level procedures. Shouldn't be used directly. - procedure Set_First_Dest_Edge (N : NFA_State; T : NFA_Edge); - procedure Set_Next_Dest_Edge (E : NFA_Edge; N_E : NFA_Edge); - procedure Set_First_Src_Edge (N : NFA_State; T : NFA_Edge); - procedure Set_Next_Src_Edge (E : NFA_Edge; N_E : NFA_Edge); - procedure Set_Edge_Dest (E : NFA_Edge; D : NFA_State); - procedure Set_Edge_Src (E : NFA_Edge; D : NFA_State); -end PSL.NFAs; diff --git a/psl/psl-nodes.adb b/psl/psl-nodes.adb deleted file mode 100644 index a6482a142..000000000 --- a/psl/psl-nodes.adb +++ /dev/null @@ -1,1231 +0,0 @@ --- This is in fact -*- Ada -*- -with Ada.Unchecked_Conversion; -with GNAT.Table; -with PSL.Errors; -with PSL.Hash; - -package body PSL.Nodes is - -- Suppress the access check of the table base. This is really safe to - -- suppress this check because the table base cannot be null. - pragma Suppress (Access_Check); - - -- Suppress the index check on the table. - -- Could be done during non-debug, since this may catch errors (reading - -- Null_Node. - --pragma Suppress (Index_Check); - - type Format_Type is - ( - Format_Short, - Format_Medium - ); - - pragma Unreferenced (Format_Type, Format_Short, Format_Medium); - - -- Common fields are: - -- Flag1 : Boolean - -- Flag2 : Boolean - -- Flag3 : Boolean - -- Flag4 : Boolean - -- Flag5 : Boolean - -- Flag6 : Boolean - -- Nkind : Kind_Type - -- State1 : Bit2_Type - -- State2 : Bit2_Type - -- Location : Int32 - -- Field1 : Int32 - -- Field2 : Int32 - -- Field3 : Int32 - -- Field4 : Int32 - - -- Fields of Format_Short: - -- Field5 : Int32 - -- Field6 : Int32 - - -- Fields of Format_Medium: - -- Odigit1 : Bit3_Type - -- Odigit2 : Bit3_Type - -- State3 : Bit2_Type - -- State4 : Bit2_Type - -- Field5 : Int32 - -- Field6 : Int32 - -- Field7 : Int32 (location) - -- Field8 : Int32 (field1) - -- Field9 : Int32 (field2) - -- Field10 : Int32 (field3) - -- Field11 : Int32 (field4) - -- Field12 : Int32 (field5) - - type State_Type is range 0 .. 3; - type Bit3_Type is range 0 .. 7; - - type Node_Record is record - Kind : Nkind; - Flag1 : Boolean; - Flag2 : Boolean; - Flag3 : Boolean; - Flag4 : Boolean; - Flag5 : Boolean; - Flag6 : Boolean; - Flag7 : Boolean; - Flag8 : Boolean; - Flag9 : Boolean; - Flag10 : Boolean; - Flag11 : Boolean; - Flag12 : Boolean; - Flag13 : Boolean; - Flag14 : Boolean; - Flag15 : Boolean; - Flag16 : Boolean; - State1 : State_Type; - B3_1 : Bit3_Type; - Flag17 : Boolean; - Flag18 : Boolean; - Flag19 : Boolean; - - Location : Int32; - Field1 : Int32; - Field2 : Int32; - Field3 : Int32; - Field4 : Int32; - Field5 : Int32; - Field6 : Int32; - end record; - pragma Pack (Node_Record); - for Node_Record'Size use 8 * 32; - - package Nodet is new GNAT.Table - (Table_Component_Type => Node_Record, - Table_Index_Type => Node, - Table_Low_Bound => 1, - Table_Initial => 1024, - Table_Increment => 100); - - Init_Node : constant Node_Record := (Kind => N_Error, - Flag1 => False, - Flag2 => False, - State1 => 0, - B3_1 => 0, - Location => 0, - Field1 => 0, - Field2 => 0, - Field3 => 0, - Field4 => 0, - Field5 => 0, - Field6 => 0, - others => False); - - Free_Nodes : Node := Null_Node; - - - function Get_Last_Node return Node is - begin - return Nodet.Last; - end Get_Last_Node; - - function Int32_To_Uns32 is new Ada.Unchecked_Conversion - (Source => Int32, Target => Uns32); - - function Uns32_To_Int32 is new Ada.Unchecked_Conversion - (Source => Uns32, Target => Int32); - - function Int32_To_NFA is new Ada.Unchecked_Conversion - (Source => Int32, Target => NFA); - - function NFA_To_Int32 is new Ada.Unchecked_Conversion - (Source => NFA, Target => Int32); - - procedure Set_Kind (N : Node; K : Nkind) is - begin - Nodet.Table (N).Kind := K; - end Set_Kind; - - function Get_Kind (N : Node) return Nkind is - begin - return Nodet.Table (N).Kind; - end Get_Kind; - - - procedure Set_Flag1 (N : Node; Flag : Boolean) is - begin - Nodet.Table (N).Flag1 := Flag; - end Set_Flag1; - - function Get_Flag1 (N : Node) return Boolean is - begin - return Nodet.Table (N).Flag1; - end Get_Flag1; - - procedure Set_Flag2 (N : Node; Flag : Boolean) is - begin - Nodet.Table (N).Flag2 := Flag; - end Set_Flag2; - - function Get_Flag2 (N : Node) return Boolean is - begin - return Nodet.Table (N).Flag2; - end Get_Flag2; - - - procedure Set_State1 (N : Node; S : State_Type) is - begin - Nodet.Table (N).State1 := S; - end Set_State1; - - function Get_State1 (N : Node) return State_Type is - begin - return Nodet.Table (N).State1; - end Get_State1; - - - function Get_Location (N : Node) return Location_Type is - begin - return Location_Type (Nodet.Table (N).Location); - end Get_Location; - - procedure Set_Location (N : Node; Loc : Location_Type) is - begin - Nodet.Table (N).Location := Int32 (Loc); - end Set_Location; - - - procedure Set_Field1 (N : Node; V : Int32) is - begin - Nodet.Table (N).Field1 := V; - end Set_Field1; - - function Get_Field1 (N : Node) return Int32 is - begin - return Nodet.Table (N).Field1; - end Get_Field1; - - - procedure Set_Field2 (N : Node; V : Int32) is - begin - Nodet.Table (N).Field2 := V; - end Set_Field2; - - function Get_Field2 (N : Node) return Int32 is - begin - return Nodet.Table (N).Field2; - end Get_Field2; - - - function Get_Field3 (N : Node) return Int32 is - begin - return Nodet.Table (N).Field3; - end Get_Field3; - - procedure Set_Field3 (N : Node; V : Int32) is - begin - Nodet.Table (N).Field3 := V; - end Set_Field3; - - - function Get_Field4 (N : Node) return Int32 is - begin - return Nodet.Table (N).Field4; - end Get_Field4; - - procedure Set_Field4 (N : Node; V : Int32) is - begin - Nodet.Table (N).Field4 := V; - end Set_Field4; - - - function Get_Field5 (N : Node) return Int32 is - begin - return Nodet.Table (N).Field5; - end Get_Field5; - - procedure Set_Field5 (N : Node; V : Int32) is - begin - Nodet.Table (N).Field5 := V; - end Set_Field5; - - - function Get_Field6 (N : Node) return Int32 is - begin - return Nodet.Table (N).Field6; - end Get_Field6; - - procedure Set_Field6 (N : Node; V : Int32) is - begin - Nodet.Table (N).Field6 := V; - end Set_Field6; - - procedure Set_Field7 (N : Node; V : Int32) is - begin - Nodet.Table (N + 1).Field1 := V; - end Set_Field7; - - function Get_Field7 (N : Node) return Int32 is - begin - return Nodet.Table (N + 1).Field1; - end Get_Field7; - - - function Create_Node (Kind : Nkind) return Node - is - Res : Node; - begin - if Free_Nodes /= Null_Node then - Res := Free_Nodes; - Free_Nodes := Node (Get_Field1 (Res)); - else - Nodet.Increment_Last; - Res := Nodet.Last; - end if; - Nodet.Table (Res) := Init_Node; - Set_Kind (Res, Kind); - return Res; - end Create_Node; - - procedure Free_Node (N : Node) - is - begin - Set_Kind (N, N_Error); - Set_Field1 (N, Int32 (Free_Nodes)); - Free_Nodes := N; - end Free_Node; - - procedure Failed (Msg : String; N : Node) - is - begin - Errors.Error_Kind (Msg, N); - end Failed; - - procedure Init is - begin - Nodet.Init; - if Create_Node (N_False) /= False_Node then - raise Internal_Error; - end if; - if Create_Node (N_True) /= True_Node then - raise Internal_Error; - end if; - if Create_Node (N_Number) /= One_Node then - raise Internal_Error; - end if; - Set_Value (One_Node, 1); - if Create_Node (N_EOS) /= EOS_Node then - raise Internal_Error; - end if; - Set_Hash (EOS_Node, 0); - PSL.Hash.Init; - end Init; - - function Get_Psl_Type (N : Node) return PSL_Types is - begin - case Get_Kind (N) is - when N_And_Prop - | N_Or_Prop - | N_Log_Imp_Prop - | N_Always - | N_Never - | N_Eventually - | N_Next - | N_Next_E - | N_Next_A - | N_Next_Event - | N_Next_Event_A - | N_Next_Event_E - | N_Before - | N_Until - | N_Abort - | N_Strong - | N_Property_Parameter - | N_Property_Instance => - return Type_Property; - when N_Braced_SERE - | N_Concat_SERE - | N_Fusion_SERE - | N_Within_SERE - | N_Overlap_Imp_Seq - | N_Imp_Seq - | N_And_Seq - | N_Or_Seq - | N_Match_And_Seq - | N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Equal_Repeat_Seq - | N_Plus_Repeat_Seq - | N_Clock_Event - | N_Sequence_Instance - | N_Endpoint_Instance - | N_Sequence_Parameter => - return Type_Sequence; - when N_Name => - return Get_Psl_Type (Get_Decl (N)); - when N_HDL_Expr => - -- FIXME. - return Type_Boolean; - when N_Or_Bool - | N_And_Bool - | N_Not_Bool - | N_Imp_Bool - | N_False - | N_True - | N_Boolean_Parameter => - return Type_Boolean; - when N_Number - | N_Const_Parameter => - return Type_Numeric; - when N_Vmode - | N_Vunit - | N_Vprop - | N_Hdl_Mod_Name - | N_Assert_Directive - | N_Sequence_Declaration - | N_Endpoint_Declaration - | N_Property_Declaration - | N_Actual - | N_Name_Decl - | N_Error - | N_EOS => - PSL.Errors.Error_Kind ("get_psl_type", N); - end case; - end Get_Psl_Type; - - procedure Reference_Failed (Msg : String; N : Node) is - begin - Failed (Msg, N); - end Reference_Failed; - pragma Unreferenced (Reference_Failed); - - pragma Unreferenced (Set_Field7, Get_Field7); - -- Subprograms. - procedure Check_Kind_For_Identifier (N : Node) is - begin - case Get_Kind (N) is - when N_Vmode - | N_Vunit - | N_Vprop - | N_Hdl_Mod_Name - | N_Property_Declaration - | N_Sequence_Declaration - | N_Endpoint_Declaration - | N_Const_Parameter - | N_Boolean_Parameter - | N_Property_Parameter - | N_Sequence_Parameter - | N_Name - | N_Name_Decl => - null; - when others => - Failed ("Get/Set_Identifier", N); - end case; - end Check_Kind_For_Identifier; - - function Get_Identifier (N : Node) return Name_Id is - begin - Check_Kind_For_Identifier (N); - return Name_Id (Get_Field1 (N)); - end Get_Identifier; - - procedure Set_Identifier (N : Node; Id : Name_Id) is - begin - Check_Kind_For_Identifier (N); - Set_Field1 (N, Int32 (Id)); - end Set_Identifier; - - procedure Check_Kind_For_Chain (N : Node) is - begin - case Get_Kind (N) is - when N_Vmode - | N_Vunit - | N_Vprop - | N_Assert_Directive - | N_Property_Declaration - | N_Sequence_Declaration - | N_Endpoint_Declaration - | N_Const_Parameter - | N_Boolean_Parameter - | N_Property_Parameter - | N_Sequence_Parameter - | N_Actual - | N_Name_Decl => - null; - when others => - Failed ("Get/Set_Chain", N); - end case; - end Check_Kind_For_Chain; - - function Get_Chain (N : Node) return Node is - begin - Check_Kind_For_Chain (N); - return Node (Get_Field2 (N)); - end Get_Chain; - - procedure Set_Chain (N : Node; Chain : Node) is - begin - Check_Kind_For_Chain (N); - Set_Field2 (N, Int32 (Chain)); - end Set_Chain; - - procedure Check_Kind_For_Instance (N : Node) is - begin - case Get_Kind (N) is - when N_Vmode - | N_Vunit - | N_Vprop => - null; - when others => - Failed ("Get/Set_Instance", N); - end case; - end Check_Kind_For_Instance; - - function Get_Instance (N : Node) return Node is - begin - Check_Kind_For_Instance (N); - return Node (Get_Field3 (N)); - end Get_Instance; - - procedure Set_Instance (N : Node; Instance : Node) is - begin - Check_Kind_For_Instance (N); - Set_Field3 (N, Int32 (Instance)); - end Set_Instance; - - procedure Check_Kind_For_Item_Chain (N : Node) is - begin - case Get_Kind (N) is - when N_Vmode - | N_Vunit - | N_Vprop => - null; - when others => - Failed ("Get/Set_Item_Chain", N); - end case; - end Check_Kind_For_Item_Chain; - - function Get_Item_Chain (N : Node) return Node is - begin - Check_Kind_For_Item_Chain (N); - return Node (Get_Field4 (N)); - end Get_Item_Chain; - - procedure Set_Item_Chain (N : Node; Item : Node) is - begin - Check_Kind_For_Item_Chain (N); - Set_Field4 (N, Int32 (Item)); - end Set_Item_Chain; - - procedure Check_Kind_For_Prefix (N : Node) is - begin - case Get_Kind (N) is - when N_Hdl_Mod_Name => - null; - when others => - Failed ("Get/Set_Prefix", N); - end case; - end Check_Kind_For_Prefix; - - function Get_Prefix (N : Node) return Node is - begin - Check_Kind_For_Prefix (N); - return Node (Get_Field2 (N)); - end Get_Prefix; - - procedure Set_Prefix (N : Node; Prefix : Node) is - begin - Check_Kind_For_Prefix (N); - Set_Field2 (N, Int32 (Prefix)); - end Set_Prefix; - - procedure Check_Kind_For_Label (N : Node) is - begin - case Get_Kind (N) is - when N_Assert_Directive => - null; - when others => - Failed ("Get/Set_Label", N); - end case; - end Check_Kind_For_Label; - - function Get_Label (N : Node) return Name_Id is - begin - Check_Kind_For_Label (N); - return Name_Id (Get_Field1 (N)); - end Get_Label; - - procedure Set_Label (N : Node; Id : Name_Id) is - begin - Check_Kind_For_Label (N); - Set_Field1 (N, Int32 (Id)); - end Set_Label; - - procedure Check_Kind_For_String (N : Node) is - begin - case Get_Kind (N) is - when N_Assert_Directive => - null; - when others => - Failed ("Get/Set_String", N); - end case; - end Check_Kind_For_String; - - function Get_String (N : Node) return Node is - begin - Check_Kind_For_String (N); - return Node (Get_Field3 (N)); - end Get_String; - - procedure Set_String (N : Node; Str : Node) is - begin - Check_Kind_For_String (N); - Set_Field3 (N, Int32 (Str)); - end Set_String; - - procedure Check_Kind_For_Property (N : Node) is - begin - case Get_Kind (N) is - when N_Assert_Directive - | N_Property_Declaration - | N_Clock_Event - | N_Always - | N_Never - | N_Eventually - | N_Strong - | N_Imp_Seq - | N_Overlap_Imp_Seq - | N_Next - | N_Next_A - | N_Next_E - | N_Next_Event - | N_Next_Event_A - | N_Next_Event_E - | N_Abort => - null; - when others => - Failed ("Get/Set_Property", N); - end case; - end Check_Kind_For_Property; - - function Get_Property (N : Node) return Node is - begin - Check_Kind_For_Property (N); - return Node (Get_Field4 (N)); - end Get_Property; - - procedure Set_Property (N : Node; Property : Node) is - begin - Check_Kind_For_Property (N); - Set_Field4 (N, Int32 (Property)); - end Set_Property; - - procedure Check_Kind_For_NFA (N : Node) is - begin - case Get_Kind (N) is - when N_Assert_Directive => - null; - when others => - Failed ("Get/Set_NFA", N); - end case; - end Check_Kind_For_NFA; - - function Get_NFA (N : Node) return NFA is - begin - Check_Kind_For_NFA (N); - return Int32_To_NFA (Get_Field5 (N)); - end Get_NFA; - - procedure Set_NFA (N : Node; P : NFA) is - begin - Check_Kind_For_NFA (N); - Set_Field5 (N, NFA_To_Int32 (P)); - end Set_NFA; - - procedure Check_Kind_For_Global_Clock (N : Node) is - begin - case Get_Kind (N) is - when N_Property_Declaration => - null; - when others => - Failed ("Get/Set_Global_Clock", N); - end case; - end Check_Kind_For_Global_Clock; - - function Get_Global_Clock (N : Node) return Node is - begin - Check_Kind_For_Global_Clock (N); - return Node (Get_Field3 (N)); - end Get_Global_Clock; - - procedure Set_Global_Clock (N : Node; Clock : Node) is - begin - Check_Kind_For_Global_Clock (N); - Set_Field3 (N, Int32 (Clock)); - end Set_Global_Clock; - - procedure Check_Kind_For_Parameter_List (N : Node) is - begin - case Get_Kind (N) is - when N_Property_Declaration - | N_Sequence_Declaration - | N_Endpoint_Declaration => - null; - when others => - Failed ("Get/Set_Parameter_List", N); - end case; - end Check_Kind_For_Parameter_List; - - function Get_Parameter_List (N : Node) return Node is - begin - Check_Kind_For_Parameter_List (N); - return Node (Get_Field5 (N)); - end Get_Parameter_List; - - procedure Set_Parameter_List (N : Node; E : Node) is - begin - Check_Kind_For_Parameter_List (N); - Set_Field5 (N, Int32 (E)); - end Set_Parameter_List; - - procedure Check_Kind_For_Sequence (N : Node) is - begin - case Get_Kind (N) is - when N_Sequence_Declaration - | N_Endpoint_Declaration - | N_Imp_Seq - | N_Overlap_Imp_Seq - | N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Plus_Repeat_Seq - | N_Equal_Repeat_Seq => - null; - when others => - Failed ("Get/Set_Sequence", N); - end case; - end Check_Kind_For_Sequence; - - function Get_Sequence (N : Node) return Node is - begin - Check_Kind_For_Sequence (N); - return Node (Get_Field3 (N)); - end Get_Sequence; - - procedure Set_Sequence (N : Node; S : Node) is - begin - Check_Kind_For_Sequence (N); - Set_Field3 (N, Int32 (S)); - end Set_Sequence; - - procedure Check_Kind_For_Actual (N : Node) is - begin - case Get_Kind (N) is - when N_Const_Parameter - | N_Boolean_Parameter - | N_Property_Parameter - | N_Sequence_Parameter - | N_Actual => - null; - when others => - Failed ("Get/Set_Actual", N); - end case; - end Check_Kind_For_Actual; - - function Get_Actual (N : Node) return Node is - begin - Check_Kind_For_Actual (N); - return Node (Get_Field3 (N)); - end Get_Actual; - - procedure Set_Actual (N : Node; E : Node) is - begin - Check_Kind_For_Actual (N); - Set_Field3 (N, Int32 (E)); - end Set_Actual; - - procedure Check_Kind_For_Declaration (N : Node) is - begin - case Get_Kind (N) is - when N_Sequence_Instance - | N_Endpoint_Instance - | N_Property_Instance => - null; - when others => - Failed ("Get/Set_Declaration", N); - end case; - end Check_Kind_For_Declaration; - - function Get_Declaration (N : Node) return Node is - begin - Check_Kind_For_Declaration (N); - return Node (Get_Field1 (N)); - end Get_Declaration; - - procedure Set_Declaration (N : Node; Decl : Node) is - begin - Check_Kind_For_Declaration (N); - Set_Field1 (N, Int32 (Decl)); - end Set_Declaration; - - procedure Check_Kind_For_Association_Chain (N : Node) is - begin - case Get_Kind (N) is - when N_Sequence_Instance - | N_Endpoint_Instance - | N_Property_Instance => - null; - when others => - Failed ("Get/Set_Association_Chain", N); - end case; - end Check_Kind_For_Association_Chain; - - function Get_Association_Chain (N : Node) return Node is - begin - Check_Kind_For_Association_Chain (N); - return Node (Get_Field2 (N)); - end Get_Association_Chain; - - procedure Set_Association_Chain (N : Node; Chain : Node) is - begin - Check_Kind_For_Association_Chain (N); - Set_Field2 (N, Int32 (Chain)); - end Set_Association_Chain; - - procedure Check_Kind_For_Formal (N : Node) is - begin - case Get_Kind (N) is - when N_Actual => - null; - when others => - Failed ("Get/Set_Formal", N); - end case; - end Check_Kind_For_Formal; - - function Get_Formal (N : Node) return Node is - begin - Check_Kind_For_Formal (N); - return Node (Get_Field4 (N)); - end Get_Formal; - - procedure Set_Formal (N : Node; E : Node) is - begin - Check_Kind_For_Formal (N); - Set_Field4 (N, Int32 (E)); - end Set_Formal; - - procedure Check_Kind_For_Boolean (N : Node) is - begin - case Get_Kind (N) is - when N_Clock_Event - | N_Next_Event - | N_Next_Event_A - | N_Next_Event_E - | N_Abort - | N_Not_Bool => - null; - when others => - Failed ("Get/Set_Boolean", N); - end case; - end Check_Kind_For_Boolean; - - function Get_Boolean (N : Node) return Node is - begin - Check_Kind_For_Boolean (N); - return Node (Get_Field3 (N)); - end Get_Boolean; - - procedure Set_Boolean (N : Node; B : Node) is - begin - Check_Kind_For_Boolean (N); - Set_Field3 (N, Int32 (B)); - end Set_Boolean; - - procedure Check_Kind_For_Strong_Flag (N : Node) is - begin - case Get_Kind (N) is - when N_Next - | N_Next_A - | N_Next_E - | N_Next_Event - | N_Next_Event_A - | N_Next_Event_E - | N_Until - | N_Before => - null; - when others => - Failed ("Get/Set_Strong_Flag", N); - end case; - end Check_Kind_For_Strong_Flag; - - function Get_Strong_Flag (N : Node) return Boolean is - begin - Check_Kind_For_Strong_Flag (N); - return Get_Flag1 (N); - end Get_Strong_Flag; - - procedure Set_Strong_Flag (N : Node; B : Boolean) is - begin - Check_Kind_For_Strong_Flag (N); - Set_Flag1 (N, B); - end Set_Strong_Flag; - - procedure Check_Kind_For_Number (N : Node) is - begin - case Get_Kind (N) is - when N_Next - | N_Next_Event => - null; - when others => - Failed ("Get/Set_Number", N); - end case; - end Check_Kind_For_Number; - - function Get_Number (N : Node) return Node is - begin - Check_Kind_For_Number (N); - return Node (Get_Field1 (N)); - end Get_Number; - - procedure Set_Number (N : Node; S : Node) is - begin - Check_Kind_For_Number (N); - Set_Field1 (N, Int32 (S)); - end Set_Number; - - procedure Check_Kind_For_Decl (N : Node) is - begin - case Get_Kind (N) is - when N_Name => - null; - when others => - Failed ("Get/Set_Decl", N); - end case; - end Check_Kind_For_Decl; - - function Get_Decl (N : Node) return Node is - begin - Check_Kind_For_Decl (N); - return Node (Get_Field2 (N)); - end Get_Decl; - - procedure Set_Decl (N : Node; D : Node) is - begin - Check_Kind_For_Decl (N); - Set_Field2 (N, Int32 (D)); - end Set_Decl; - - procedure Check_Kind_For_Value (N : Node) is - begin - case Get_Kind (N) is - when N_Number => - null; - when others => - Failed ("Get/Set_Value", N); - end case; - end Check_Kind_For_Value; - - function Get_Value (N : Node) return Uns32 is - begin - Check_Kind_For_Value (N); - return Int32_To_Uns32 (Get_Field1 (N)); - end Get_Value; - - procedure Set_Value (N : Node; Val : Uns32) is - begin - Check_Kind_For_Value (N); - Set_Field1 (N, Uns32_To_Int32 (Val)); - end Set_Value; - - procedure Check_Kind_For_SERE (N : Node) is - begin - case Get_Kind (N) is - when N_Braced_SERE => - null; - when others => - Failed ("Get/Set_SERE", N); - end case; - end Check_Kind_For_SERE; - - function Get_SERE (N : Node) return Node is - begin - Check_Kind_For_SERE (N); - return Node (Get_Field1 (N)); - end Get_SERE; - - procedure Set_SERE (N : Node; S : Node) is - begin - Check_Kind_For_SERE (N); - Set_Field1 (N, Int32 (S)); - end Set_SERE; - - procedure Check_Kind_For_Left (N : Node) is - begin - case Get_Kind (N) is - when N_Log_Imp_Prop - | N_Until - | N_Before - | N_Or_Prop - | N_And_Prop - | N_Concat_SERE - | N_Fusion_SERE - | N_Within_SERE - | N_Match_And_Seq - | N_And_Seq - | N_Or_Seq - | N_And_Bool - | N_Or_Bool - | N_Imp_Bool => - null; - when others => - Failed ("Get/Set_Left", N); - end case; - end Check_Kind_For_Left; - - function Get_Left (N : Node) return Node is - begin - Check_Kind_For_Left (N); - return Node (Get_Field1 (N)); - end Get_Left; - - procedure Set_Left (N : Node; S : Node) is - begin - Check_Kind_For_Left (N); - Set_Field1 (N, Int32 (S)); - end Set_Left; - - procedure Check_Kind_For_Right (N : Node) is - begin - case Get_Kind (N) is - when N_Log_Imp_Prop - | N_Until - | N_Before - | N_Or_Prop - | N_And_Prop - | N_Concat_SERE - | N_Fusion_SERE - | N_Within_SERE - | N_Match_And_Seq - | N_And_Seq - | N_Or_Seq - | N_And_Bool - | N_Or_Bool - | N_Imp_Bool => - null; - when others => - Failed ("Get/Set_Right", N); - end case; - end Check_Kind_For_Right; - - function Get_Right (N : Node) return Node is - begin - Check_Kind_For_Right (N); - return Node (Get_Field2 (N)); - end Get_Right; - - procedure Set_Right (N : Node; S : Node) is - begin - Check_Kind_For_Right (N); - Set_Field2 (N, Int32 (S)); - end Set_Right; - - procedure Check_Kind_For_Low_Bound (N : Node) is - begin - case Get_Kind (N) is - when N_Next_A - | N_Next_E - | N_Next_Event_A - | N_Next_Event_E - | N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Equal_Repeat_Seq => - null; - when others => - Failed ("Get/Set_Low_Bound", N); - end case; - end Check_Kind_For_Low_Bound; - - function Get_Low_Bound (N : Node) return Node is - begin - Check_Kind_For_Low_Bound (N); - return Node (Get_Field1 (N)); - end Get_Low_Bound; - - procedure Set_Low_Bound (N : Node; S : Node) is - begin - Check_Kind_For_Low_Bound (N); - Set_Field1 (N, Int32 (S)); - end Set_Low_Bound; - - procedure Check_Kind_For_High_Bound (N : Node) is - begin - case Get_Kind (N) is - when N_Next_A - | N_Next_E - | N_Next_Event_A - | N_Next_Event_E - | N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Equal_Repeat_Seq => - null; - when others => - Failed ("Get/Set_High_Bound", N); - end case; - end Check_Kind_For_High_Bound; - - function Get_High_Bound (N : Node) return Node is - begin - Check_Kind_For_High_Bound (N); - return Node (Get_Field2 (N)); - end Get_High_Bound; - - procedure Set_High_Bound (N : Node; S : Node) is - begin - Check_Kind_For_High_Bound (N); - Set_Field2 (N, Int32 (S)); - end Set_High_Bound; - - procedure Check_Kind_For_Inclusive_Flag (N : Node) is - begin - case Get_Kind (N) is - when N_Until - | N_Before => - null; - when others => - Failed ("Get/Set_Inclusive_Flag", N); - end case; - end Check_Kind_For_Inclusive_Flag; - - function Get_Inclusive_Flag (N : Node) return Boolean is - begin - Check_Kind_For_Inclusive_Flag (N); - return Get_Flag2 (N); - end Get_Inclusive_Flag; - - procedure Set_Inclusive_Flag (N : Node; B : Boolean) is - begin - Check_Kind_For_Inclusive_Flag (N); - Set_Flag2 (N, B); - end Set_Inclusive_Flag; - - procedure Check_Kind_For_Presence (N : Node) is - begin - case Get_Kind (N) is - when N_Not_Bool - | N_And_Bool - | N_Or_Bool - | N_Imp_Bool - | N_HDL_Expr => - null; - when others => - Failed ("Get/Set_Presence", N); - end case; - end Check_Kind_For_Presence; - - function Get_Presence (N : Node) return PSL_Presence_Kind is - begin - Check_Kind_For_Presence (N); - return PSL_Presence_Kind'Val(Get_State1 (N)); - end Get_Presence; - - procedure Set_Presence (N : Node; P : PSL_Presence_Kind) is - begin - Check_Kind_For_Presence (N); - Set_State1 (N, PSL_Presence_Kind'pos (P)); - end Set_Presence; - - procedure Check_Kind_For_HDL_Node (N : Node) is - begin - case Get_Kind (N) is - when N_HDL_Expr => - null; - when others => - Failed ("Get/Set_HDL_Node", N); - end case; - end Check_Kind_For_HDL_Node; - - function Get_HDL_Node (N : Node) return HDL_Node is - begin - Check_Kind_For_HDL_Node (N); - return Get_Field1 (N); - end Get_HDL_Node; - - procedure Set_HDL_Node (N : Node; H : HDL_Node) is - begin - Check_Kind_For_HDL_Node (N); - Set_Field1 (N, H); - end Set_HDL_Node; - - procedure Check_Kind_For_HDL_Index (N : Node) is - begin - case Get_Kind (N) is - when N_HDL_Expr - | N_EOS => - null; - when others => - Failed ("Get/Set_HDL_Index", N); - end case; - end Check_Kind_For_HDL_Index; - - function Get_HDL_Index (N : Node) return Int32 is - begin - Check_Kind_For_HDL_Index (N); - return Get_Field2 (N); - end Get_HDL_Index; - - procedure Set_HDL_Index (N : Node; Idx : Int32) is - begin - Check_Kind_For_HDL_Index (N); - Set_Field2 (N, Idx); - end Set_HDL_Index; - - procedure Check_Kind_For_Hash (N : Node) is - begin - case Get_Kind (N) is - when N_Not_Bool - | N_And_Bool - | N_Or_Bool - | N_Imp_Bool - | N_HDL_Expr - | N_EOS => - null; - when others => - Failed ("Get/Set_Hash", N); - end case; - end Check_Kind_For_Hash; - - function Get_Hash (N : Node) return Uns32 is - begin - Check_Kind_For_Hash (N); - return Int32_To_Uns32 (Get_Field5 (N)); - end Get_Hash; - - procedure Set_Hash (N : Node; E : Uns32) is - begin - Check_Kind_For_Hash (N); - Set_Field5 (N, Uns32_To_Int32 (E)); - end Set_Hash; - - procedure Check_Kind_For_Hash_Link (N : Node) is - begin - case Get_Kind (N) is - when N_Not_Bool - | N_And_Bool - | N_Or_Bool - | N_Imp_Bool - | N_HDL_Expr - | N_EOS => - null; - when others => - Failed ("Get/Set_Hash_Link", N); - end case; - end Check_Kind_For_Hash_Link; - - function Get_Hash_Link (N : Node) return Node is - begin - Check_Kind_For_Hash_Link (N); - return Node (Get_Field6 (N)); - end Get_Hash_Link; - - procedure Set_Hash_Link (N : Node; E : Node) is - begin - Check_Kind_For_Hash_Link (N); - Set_Field6 (N, Int32 (E)); - end Set_Hash_Link; - - -end PSL.Nodes; - diff --git a/psl/psl-nodes.ads b/psl/psl-nodes.ads deleted file mode 100644 index 241091805..000000000 --- a/psl/psl-nodes.ads +++ /dev/null @@ -1,563 +0,0 @@ -with Types; use Types; - -package PSL.Nodes is - type Nkind is - ( - N_Error, - - N_Vmode, - N_Vunit, - N_Vprop, - - N_Hdl_Mod_Name, - - N_Assert_Directive, - N_Property_Declaration, - N_Sequence_Declaration, - N_Endpoint_Declaration, - - -- Formal parameters - N_Const_Parameter, - N_Boolean_Parameter, - N_Property_Parameter, - N_Sequence_Parameter, - - N_Sequence_Instance, - N_Endpoint_Instance, - N_Property_Instance, - N_Actual, - - N_Clock_Event, - - -- Properties - N_Always, - N_Never, - N_Eventually, - N_Strong, -- ! - N_Imp_Seq, -- |=> - N_Overlap_Imp_Seq, -- |-> - N_Log_Imp_Prop, -- -> - N_Next, - N_Next_A, - N_Next_E, - N_Next_Event, - N_Next_Event_A, - N_Next_Event_E, - N_Abort, - N_Until, - N_Before, - N_Or_Prop, - N_And_Prop, - - -- Sequences/SERE. - N_Braced_SERE, - N_Concat_SERE, - N_Fusion_SERE, - N_Within_SERE, - - N_Match_And_Seq, -- && - N_And_Seq, - N_Or_Seq, - - N_Star_Repeat_Seq, - N_Goto_Repeat_Seq, - N_Plus_Repeat_Seq, -- [+] - N_Equal_Repeat_Seq, - - -- Boolean layer. - N_Not_Bool, - N_And_Bool, - N_Or_Bool, - N_Imp_Bool, -- -> - N_HDL_Expr, - N_False, - N_True, - N_EOS, - - N_Name, - N_Name_Decl, - N_Number - ); - for Nkind'Size use 8; - - subtype N_Booleans is Nkind range N_Not_Bool .. N_True; - subtype N_Sequences is Nkind range N_Braced_SERE .. N_Equal_Repeat_Seq; - - type PSL_Types is - ( - Type_Unknown, - Type_Boolean, - Type_Bit, - Type_Bitvector, - Type_Numeric, - Type_String, - Type_Sequence, - Type_Property - ); - - -- Within CSE, it is useful to know which sub-expression already compose - -- an expression. - -- Eg: suppose we want to build A and B. - -- Each sub-expressions of B is marked either as Present_Pos or - -- Present_Neg. - -- If A is already present, return either B or FALSE. - -- Otherwise, build the node. - type PSL_Presence_Kind is - ( - Present_Unknown, - Present_Pos, - Present_Neg - ); - - -- Start of nodes: - - -- N_Error (Short) - - -- N_Vmode (Short) - -- N_Vunit (Short) - -- N_Vprop (Short) - -- - -- Get/Set_Identifier (Field1) - -- - -- Get/Set_Chain (Field2) - -- - -- Get/Set_Instance (Field3) - -- - -- Get/Set_Item_Chain (Field4) - - -- N_Hdl_Mod_Name (Short) - -- - -- Get/Set_Identifier (Field1) - -- - -- Get/Set_Prefix (Field2) - - -- N_Assert_Directive (Short) - -- - -- Get/Set_Label (Field1) - -- - -- Get/Set_Chain (Field2) - -- - -- Get/Set_String (Field3) - -- - -- Get/Set_Property (Field4) - -- - -- Get/Set_NFA (Field5) - - -- N_Property_Declaration (Short) - -- - -- Get/Set_Identifier (Field1) - -- - -- Get/Set_Chain (Field2) - -- - -- Get/Set_Global_Clock (Field3) - -- - -- Get/Set_Property (Field4) - -- - -- Get/Set_Parameter_List (Field5) - - -- N_Sequence_Declaration (Short) - -- N_Endpoint_Declaration (Short) - -- - -- Get/Set_Identifier (Field1) - -- - -- Get/Set_Chain (Field2) - -- - -- Get/Set_Sequence (Field3) - -- - -- Get/Set_Parameter_List (Field5) - - -- N_Const_Parameter (Short) - -- N_Boolean_Parameter (Short) - -- N_Property_Parameter (Short) - -- N_Sequence_Parameter (Short) - -- - -- Get/Set_Identifier (Field1) - -- - -- Get/Set_Chain (Field2) - -- - -- -- Current actual parameter. - -- Get/Set_Actual (Field3) - - -- N_Sequence_Instance (Short) - -- N_Endpoint_Instance (Short) - -- N_Property_Instance (Short) - -- - -- Get/Set_Declaration (Field1) [Flat] - -- - -- Get/Set_Association_Chain (Field2) - - -- N_Actual (Short) - -- - -- Get/Set_Chain (Field2) - -- - -- Get/Set_Actual (Field3) - -- - -- Get/Set_Formal (Field4) - - -- N_Clock_Event (Short) - -- - -- Get/Set_Property (Field4) - -- - -- Get/Set_Boolean (Field3) - - -- N_Always (Short) - -- N_Never (Short) - -- N_Eventually (Short) - -- N_Strong (Short) - -- - -- Get/Set_Property (Field4) - - -- N_Next (Short) - -- - -- Get/Set_Strong_Flag (Flag1) - -- - -- Get/Set_Number (Field1) - -- - -- Get/Set_Property (Field4) - - -- N_Name (Short) - -- - -- Get/Set_Identifier (Field1) - -- - -- Get/Set_Decl (Field2) - - -- N_Name_Decl (Short) - -- - -- Get/Set_Identifier (Field1) - -- - -- Get/Set_Chain (Field2) - - -- N_Number (Short) - -- - -- Get/Set_Value (Field1) - - -- N_Braced_SERE (Short) - -- - -- Get/Set_SERE (Field1) - - -- N_Concat_SERE (Short) - -- N_Fusion_SERE (Short) - -- N_Within_SERE (Short) - -- - -- Get/Set_Left (Field1) - -- - -- Get/Set_Right (Field2) - - -- N_Star_Repeat_Seq (Short) - -- N_Goto_Repeat_Seq (Short) - -- N_Equal_Repeat_Seq (Short) - -- - -- Note: can be null_node for star_repeat_seq. - -- Get/Set_Sequence (Field3) - -- - -- Get/Set_Low_Bound (Field1) - -- - -- Get/Set_High_Bound (Field2) - - -- N_Plus_Repeat_Seq (Short) - -- - -- Note: can be null_node. - -- Get/Set_Sequence (Field3) - - -- N_Match_And_Seq (Short) - -- N_And_Seq (Short) - -- N_Or_Seq (Short) - -- - -- Get/Set_Left (Field1) - -- - -- Get/Set_Right (Field2) - - -- N_Imp_Seq (Short) - -- N_Overlap_Imp_Seq (Short) - -- - -- Get/Set_Sequence (Field3) - -- - -- Get/Set_Property (Field4) - - -- N_Log_Imp_Prop (Short) - -- - -- Get/Set_Left (Field1) - -- - -- Get/Set_Right (Field2) - - -- N_Next_A (Short) - -- N_Next_E (Short) - -- - -- Get/Set_Strong_Flag (Flag1) - -- - -- Get/Set_Low_Bound (Field1) - -- - -- Get/Set_High_Bound (Field2) - -- - -- Get/Set_Property (Field4) - - -- N_Next_Event (Short) - -- - -- Get/Set_Strong_Flag (Flag1) - -- - -- Get/Set_Number (Field1) - -- - -- Get/Set_Property (Field4) - -- - -- Get/Set_Boolean (Field3) - - -- N_Or_Prop (Short) - -- N_And_Prop (Short) - -- - -- Get/Set_Left (Field1) - -- - -- Get/Set_Right (Field2) - - -- N_Until (Short) - -- N_Before (Short) - -- - -- Get/Set_Strong_Flag (Flag1) - -- - -- Get/Set_Inclusive_Flag (Flag2) - -- - -- Get/Set_Left (Field1) - -- - -- Get/Set_Right (Field2) - - -- N_Next_Event_A (Short) - -- N_Next_Event_E (Short) - -- - -- Get/Set_Strong_Flag (Flag1) - -- - -- Get/Set_Low_Bound (Field1) - -- - -- Get/Set_High_Bound (Field2) - -- - -- Get/Set_Property (Field4) - -- - -- Get/Set_Boolean (Field3) - - -- N_Abort (Short) - -- - -- Get/Set_Property (Field4) - -- - -- Get/Set_Boolean (Field3) - - - -- N_HDL_Expr (Short) - -- - -- Get/Set_Presence (State1) - -- - -- Get/Set_HDL_Node (Field1) - -- - -- Get/Set_HDL_Index (Field2) - -- - -- Get/Set_Hash (Field5) - -- - -- Get/Set_Hash_Link (Field6) - - -- N_Not_Bool (Short) - -- - -- Get/Set_Presence (State1) - -- - -- Get/Set_Boolean (Field3) - -- - -- Get/Set_Hash (Field5) - -- - -- Get/Set_Hash_Link (Field6) - - -- N_And_Bool (Short) - -- N_Or_Bool (Short) - -- N_Imp_Bool (Short) - -- - -- Get/Set_Presence (State1) - -- - -- Get/Set_Left (Field1) - -- - -- Get/Set_Right (Field2) - -- - -- Get/Set_Hash (Field5) - -- - -- Get/Set_Hash_Link (Field6) - - -- N_True (Short) - -- N_False (Short) - - -- N_EOS (Short) - -- End of simulation. - -- - -- Get/Set_HDL_Index (Field2) - -- - -- Get/Set_Hash (Field5) - -- - -- Get/Set_Hash_Link (Field6) - - -- End of nodes. - - subtype Node is Types.PSL_Node; - - Null_Node : constant Node := 0; - False_Node : constant Node := 1; - True_Node : constant Node := 2; - One_Node : constant Node := 3; - EOS_Node : constant Node := 4; - - subtype NFA is Types.PSL_NFA; - - subtype HDL_Node is Types.Int32; - HDL_Null : constant HDL_Node := 0; - - procedure Init; - - -- Get the number of the last node. - -- To be used to size lateral tables. - function Get_Last_Node return Node; - - -- subtype Regs_Type_Node is Node range Reg_Type_Node .. Time_Type_Node; - - function Create_Node (Kind : Nkind) return Node; - procedure Free_Node (N : Node); - - -- Return the type of a node. - function Get_Psl_Type (N : Node) return PSL_Types; - - -- Field: Location - function Get_Location (N : Node) return Location_Type; - procedure Set_Location (N : Node; Loc : Location_Type); - - function Get_Kind (N : Node) return Nkind; - pragma Inline (Get_Kind); - --- -- Disp: None --- -- Field: Field6 --- function Get_Parent (N : Node) return Node; --- procedure Set_Parent (N : Node; Parent : Node); - - -- Disp: Special - -- Field: Field1 (conv) - function Get_Identifier (N : Node) return Name_Id; - procedure Set_Identifier (N : Node; Id : Name_Id); - - -- Disp: Special - -- Field: Field1 (conv) - function Get_Label (N : Node) return Name_Id; - procedure Set_Label (N : Node; Id : Name_Id); - - -- Disp: Chain - -- Field: Field2 (conv) - function Get_Chain (N : Node) return Node; - procedure Set_Chain (N : Node; Chain : Node); - - -- Field: Field3 (conv) - function Get_Instance (N : Node) return Node; - procedure Set_Instance (N : Node; Instance : Node); - - -- Field: Field2 (conv) - function Get_Prefix (N : Node) return Node; - procedure Set_Prefix (N : Node; Prefix : Node); - - -- Field: Field4 (conv) - function Get_Item_Chain (N : Node) return Node; - procedure Set_Item_Chain (N : Node; Item : Node); - - -- Field: Field4 (conv) - function Get_Property (N : Node) return Node; - procedure Set_Property (N : Node; Property : Node); - - -- Field: Field3 (conv) - function Get_String (N : Node) return Node; - procedure Set_String (N : Node; Str : Node); - - -- Field: Field1 (conv) - function Get_SERE (N : Node) return Node; - procedure Set_SERE (N : Node; S : Node); - - -- Field: Field1 (conv) - function Get_Left (N : Node) return Node; - procedure Set_Left (N : Node; S : Node); - - -- Field: Field2 (conv) - function Get_Right (N : Node) return Node; - procedure Set_Right (N : Node; S : Node); - - -- Field: Field3 (conv) - function Get_Sequence (N : Node) return Node; - procedure Set_Sequence (N : Node; S : Node); - - -- Field: Flag1 - function Get_Strong_Flag (N : Node) return Boolean; - procedure Set_Strong_Flag (N : Node; B : Boolean); - - -- Field: Flag2 - function Get_Inclusive_Flag (N : Node) return Boolean; - procedure Set_Inclusive_Flag (N : Node; B : Boolean); - - -- Field: Field1 (conv) - function Get_Low_Bound (N : Node) return Node; - procedure Set_Low_Bound (N : Node; S : Node); - - -- Field: Field2 (conv) - function Get_High_Bound (N : Node) return Node; - procedure Set_High_Bound (N : Node; S : Node); - - -- Field: Field1 (conv) - function Get_Number (N : Node) return Node; - procedure Set_Number (N : Node; S : Node); - - -- Field: Field1 (uc) - function Get_Value (N : Node) return Uns32; - procedure Set_Value (N : Node; Val : Uns32); - - -- Field: Field3 (conv) - function Get_Boolean (N : Node) return Node; - procedure Set_Boolean (N : Node; B : Node); - - -- Field: Field2 (conv) - function Get_Decl (N : Node) return Node; - procedure Set_Decl (N : Node; D : Node); - - -- Field: Field1 (conv) - function Get_HDL_Node (N : Node) return HDL_Node; - procedure Set_HDL_Node (N : Node; H : HDL_Node); - - -- Field: Field5 (uc) - function Get_Hash (N : Node) return Uns32; - procedure Set_Hash (N : Node; E : Uns32); - pragma Inline (Get_Hash); - - -- Field: Field6 (conv) - function Get_Hash_Link (N : Node) return Node; - procedure Set_Hash_Link (N : Node; E : Node); - pragma Inline (Get_Hash_Link); - - -- Field: Field2 - function Get_HDL_Index (N : Node) return Int32; - procedure Set_HDL_Index (N : Node; Idx : Int32); - - -- Field: State1 (pos) - function Get_Presence (N : Node) return PSL_Presence_Kind; - procedure Set_Presence (N : Node; P : PSL_Presence_Kind); - - -- Field: Field5 (uc) - function Get_NFA (N : Node) return NFA; - procedure Set_NFA (N : Node; P : NFA); - - -- Field: Field5 (conv) - function Get_Parameter_List (N : Node) return Node; - procedure Set_Parameter_List (N : Node; E : Node); - - -- Field: Field3 (conv) - function Get_Actual (N : Node) return Node; - procedure Set_Actual (N : Node; E : Node); - - -- Field: Field4 (conv) - function Get_Formal (N : Node) return Node; - procedure Set_Formal (N : Node; E : Node); - - -- Field: Field1 (conv) - function Get_Declaration (N : Node) return Node; - procedure Set_Declaration (N : Node; Decl : Node); - - -- Field: Field2 (conv) - function Get_Association_Chain (N : Node) return Node; - procedure Set_Association_Chain (N : Node; Chain : Node); - - -- Field: Field3 (conv) - function Get_Global_Clock (N : Node) return Node; - procedure Set_Global_Clock (N : Node; Clock : Node); -end PSL.Nodes; diff --git a/psl/psl-optimize.adb b/psl/psl-optimize.adb deleted file mode 100644 index 4ca62b89e..000000000 --- a/psl/psl-optimize.adb +++ /dev/null @@ -1,460 +0,0 @@ -with Types; use Types; -with PSL.NFAs.Utils; use PSL.NFAs.Utils; -with PSL.CSE; - -package body PSL.Optimize is - procedure Push (Head : in out NFA_State; S : NFA_State) is - begin - Set_State_User_Link (S, Head); - Head := S; - end Push; - - procedure Pop (Head : in out NFA_State; S : out NFA_State) is - begin - S := Head; - Head := Get_State_User_Link (S); - end Pop; - - procedure Remove_Unreachable_States (N : NFA) - is - Head : NFA_State; - Start, Final : NFA_State; - E : NFA_Edge; - S, N_S : NFA_State; - begin - -- Remove unreachable states, ie states that can't be reached from - -- start state. - Start := Get_Start_State (N); - Final := Get_Final_State (N); - - Head := No_State; - - -- The start state is reachable. - Push (Head, Start); - Set_State_Flag (Start, True); - - -- Follow edges and mark reachable states. - while Head /= No_State loop - Pop (Head, S); - E := Get_First_Src_Edge (S); - while E /= No_Edge loop - S := Get_Edge_Dest (E); - if not Get_State_Flag (S) then - Push (Head, S); - Set_State_Flag (S, True); - end if; - E := Get_Next_Src_Edge (E); - end loop; - end loop; - - -- Remove unreachable states. - S := Get_First_State (N); - while S /= No_State loop - N_S := Get_Next_State (S); - if Get_State_Flag (S) then - -- Clean-up. - Set_State_Flag (S, False); - elsif S = Final then - -- Do not remove final state! - -- FIXME: deconnect state? - null; - else - Remove_State (N, S); - end if; - S := N_S; - end loop; - - -- Remove no-where states, ie states that can't reach the final state. - Head := No_State; - - -- The final state can reach the final state. - Push (Head, Final); - Set_State_Flag (Final, True); - - -- Follow edges and mark reachable states. - while Head /= No_State loop - Pop (Head, S); - E := Get_First_Dest_Edge (S); - while E /= No_Edge loop - S := Get_Edge_Src (E); - if not Get_State_Flag (S) then - Push (Head, S); - Set_State_Flag (S, True); - end if; - E := Get_Next_Dest_Edge (E); - end loop; - end loop; - - -- Remove unreachable states. - S := Get_First_State (N); - while S /= No_State loop - N_S := Get_Next_State (S); - if Get_State_Flag (S) then - -- Clean-up. - Set_State_Flag (S, False); - elsif S = Start then - -- Do not remove start state! - -- FIXME: deconnect state? - null; - else - Remove_State (N, S); - end if; - S := N_S; - end loop; - end Remove_Unreachable_States; - - procedure Remove_Simple_Prefix (N : NFA) - is - Start : NFA_State; - D : NFA_State; - T_Start, T_D, Next_T_D : NFA_Edge; - T_Expr : Node; - Clean : Boolean := False; - begin - Start := Get_Start_State (N); - - -- Iterate on edges from the start state. - T_Start := Get_First_Src_Edge (Start); - while T_Start /= No_Edge loop - -- Edge destination. - D := Get_Edge_Dest (T_Start); - T_Expr := Get_Edge_Expr (T_Start); - - -- Iterate on destination incoming edges. - T_D := Get_First_Dest_Edge (D); - while T_D /= No_Edge loop - Next_T_D := Get_Next_Dest_Edge (T_D); - -- Remove parallel edge. - if T_D /= T_Start - and then Get_Edge_Expr (T_D) = T_Expr - then - Remove_Edge (T_D); - Clean := True; - end if; - T_D := Next_T_D; - end loop; - T_Start := Get_Next_Src_Edge (T_Start); - end loop; - if Clean then - Remove_Unreachable_States (N); - end if; - end Remove_Simple_Prefix; - - -- Return TRUE iff the outgoing or incoming edges of L and R are the same. - -- Outgoing edges must be sorted. - generic - with function Get_First_Edge (S : NFA_State) return NFA_Edge; - with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; - with function Get_Edge_State_Reverse (E : NFA_Edge) return NFA_State; - function Are_States_Identical_Gen (L, R : NFA_State) return Boolean; - - function Are_States_Identical_Gen (L, R : NFA_State) return Boolean - is - L_E, R_E : NFA_Edge; - L_S, R_S : NFA_State; - begin - L_E := Get_First_Edge (L); - R_E := Get_First_Edge (R); - loop - if L_E = No_Edge and then R_E = No_Edge then - -- End of chain for both L and R -> identical states. - return True; - elsif L_E = No_Edge or R_E = No_Edge then - -- End of chain for either L or R -> non identical states. - return False; - elsif Get_Edge_Expr (L_E) /= Get_Edge_Expr (R_E) then - -- Different edge (different expressions). - return False; - end if; - L_S := Get_Edge_State_Reverse (L_E); - R_S := Get_Edge_State_Reverse (R_E); - if L_S /= R_S and then (L_S /= L or else R_S /= R) then - -- Predecessors are differents and not loop. - return False; - end if; - L_E := Get_Next_Edge (L_E); - R_E := Get_Next_Edge (R_E); - end loop; - end Are_States_Identical_Gen; - - generic - with procedure Sort_Edges (N : NFA); - with procedure Sort_Edges_Reverse (S : NFA_State); - with function Get_First_Edge (S : NFA_State) return NFA_Edge; - with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; - with function Get_First_Edge_Reverse (S : NFA_State) return NFA_Edge; - with function Get_Next_Edge_Reverse (E : NFA_Edge) return NFA_Edge; - with function Get_Edge_State (E : NFA_Edge) return NFA_State; - with function Get_Edge_State_Reverse (E : NFA_Edge) return NFA_State; - with procedure Merge_State_Reverse (N : NFA; - S : NFA_State; S1 : NFA_State); - procedure Merge_Identical_States_Gen (N : NFA); - - procedure Merge_Identical_States_Gen (N : NFA) - is - function Are_States_Identical is new Are_States_Identical_Gen - (Get_First_Edge => Get_First_Edge, - Get_Next_Edge => Get_Next_Edge, - Get_Edge_State_Reverse => Get_Edge_State_Reverse); - - S : NFA_State; - E : NFA_Edge; - E_State, Next_E_State : NFA_State; - Next_E, Next_Next_E : NFA_Edge; - begin - Sort_Edges (N); - - -- Iterate on states. - S := Get_First_State (N); - while S /= No_State loop - Sort_Edges_Reverse (S); - - -- Iterate on incoming edges. - E := Get_First_Edge_Reverse (S); - while E /= No_Edge loop - E_State := Get_Edge_State (E); - - -- Try to merge E with its successors. - Next_E := Get_Next_Edge_Reverse (E); - while Next_E /= No_Edge - and then Get_Edge_Expr (E) = Get_Edge_Expr (Next_E) - loop - Next_E_State := Get_Edge_State (Next_E); - Next_Next_E := Get_Next_Edge_Reverse (Next_E); - if Next_E_State = E_State then - -- Identical edge: remove the duplicate. - Remove_Edge (Next_E); - elsif Are_States_Identical (E_State, Next_E_State) then - Merge_State_Reverse (N, E_State, Next_E_State); - end if; - Next_E := Next_Next_E; - end loop; - - E := Get_Next_Edge_Reverse (E); - end loop; - - S := Get_Next_State (S); - end loop; - end Merge_Identical_States_Gen; - - procedure Merge_Identical_States_Src is new Merge_Identical_States_Gen - (Sort_Edges => Sort_Src_Edges, - Sort_Edges_Reverse => Sort_Dest_Edges, - Get_First_Edge => Get_First_Src_Edge, - Get_Next_Edge => Get_Next_Src_Edge, - Get_First_Edge_Reverse => Get_First_Dest_Edge, - Get_Next_Edge_Reverse => Get_Next_Dest_Edge, - Get_Edge_State => Get_Edge_Src, - Get_Edge_State_Reverse => Get_Edge_Dest, - Merge_State_Reverse => Merge_State_Dest); - - procedure Merge_Identical_States_Dest is new Merge_Identical_States_Gen - (Sort_Edges => Sort_Dest_Edges, - Sort_Edges_Reverse => Sort_Src_Edges, - Get_First_Edge => Get_First_Dest_Edge, - Get_Next_Edge => Get_Next_Dest_Edge, - Get_First_Edge_Reverse => Get_First_Src_Edge, - Get_Next_Edge_Reverse => Get_Next_Src_Edge, - Get_Edge_State => Get_Edge_Dest, - Get_Edge_State_Reverse => Get_Edge_Src, - Merge_State_Reverse => Merge_State_Src); - - procedure Merge_Identical_States (N : NFA) is - begin - Merge_Identical_States_Src (N); - Merge_Identical_States_Dest (N); - end Merge_Identical_States; - - procedure Merge_Edges (N : NFA) - is - use PSL.CSE; - Nbr_States : Natural; - begin - Labelize_States (N, Nbr_States); - declare - Last_State : constant Int32 := Int32 (Nbr_States) - 1; - type Edge_Array is array (0 .. Last_State) of NFA_Edge; - Edges : Edge_Array; - S, D : NFA_State; - L_D : Int32; - E, Next_E : NFA_Edge; - begin - -- Iterate on states. - S := Get_First_State (N); - while S /= No_State loop - - Edges := (others => No_Edge); - E := Get_First_Src_Edge (S); - while E /= No_Edge loop - Next_E := Get_Next_Src_Edge (E); - D := Get_Edge_Dest (E); - L_D := Get_State_Label (D); - if Edges (L_D) /= No_Edge then - Set_Edge_Expr - (Edges (L_D), - Build_Bool_Or (Get_Edge_Expr (Edges (L_D)), - Get_Edge_Expr (E))); - -- FIXME: reduce expression. - Remove_Edge (E); - else - Edges (L_D) := E; - end if; - E := Next_E; - end loop; - - S := Get_Next_State (S); - end loop; - end; - end Merge_Edges; - - procedure Remove_Identical_Src_Edges (S : NFA_State) - is - Next_E, E : NFA_Edge; - begin - Sort_Src_Edges (S); - E := Get_First_Src_Edge (S); - if E = No_Edge then - return; - end if; - loop - Next_E := Get_Next_Src_Edge (E); - exit when Next_E = No_Edge; - if Get_Edge_Dest (E) = Get_Edge_Dest (Next_E) - and then Get_Edge_Expr (E) = Get_Edge_Expr (Next_E) - then - Remove_Edge (Next_E); - else - E := Next_E; - end if; - end loop; - end Remove_Identical_Src_Edges; - - procedure Remove_Identical_Dest_Edges (S : NFA_State) - is - Next_E, E : NFA_Edge; - begin - Sort_Dest_Edges (S); - E := Get_First_Dest_Edge (S); - if E = No_Edge then - return; - end if; - loop - Next_E := Get_Next_Dest_Edge (E); - exit when Next_E = No_Edge; - if Get_Edge_Src (E) = Get_Edge_Src (Next_E) - and then Get_Edge_Expr (E) = Get_Edge_Expr (Next_E) - then - Remove_Edge (Next_E); - else - E := Next_E; - end if; - end loop; - end Remove_Identical_Dest_Edges; - - procedure Find_Partitions (N : NFA; Nbr_States : Natural) - is - Last_State : constant NFA_State := NFA_State (Nbr_States) - 1; - type Part_Offset is new Int32 range -1 .. Nat32 (Nbr_States - 1); - type Part_Id is new Part_Offset range 0 .. Part_Offset'Last; - - -- State to partition id. - State_Part : array (0 .. Last_State) of Part_Id; - pragma Unreferenced (State_Part); - - -- Last partition index. - Last_Part : Part_Id; - - -- Partitions content. - - -- To get the states in a partition P, first get the offset OFF - -- (from Offsets) of P. States are in Parts (OFF ...). The - -- number of states is not known, but they all belong to P - -- (check with STATE_PART). - Parts : array (Part_Offset) of NFA_State; - type Offset_Array is array (Part_Id) of Part_Offset; - Start_Offsets : Offset_Array; - Last_Offsets : Offset_Array; - - S, Final_State : NFA_State; - First_S : NFA_State; - Off, Last_Off : Part_Offset; - - Stable, Stable1 : Boolean; - - function Is_Equivalent (L, R : NFA_State) return Boolean is - begin - raise Program_Error; - return False; - end Is_Equivalent; - begin - -- Return now for trivial cases (0 or 1 state). - if Nbr_States < 2 then - return; - end if; - - -- Partition 1 contains the final state. - -- Partition 0 contains the other states. - Final_State := Get_Final_State (N); - Last_Part := 1; - State_Part := (others => 0); - State_Part (Final_State) := 1; - S := Get_First_State (N); - Off := -1; - while S /= No_State loop - if S /= Last_State then - Off := Off + 1; - Parts (Off) := S; - end if; - S := Get_Next_State (S); - end loop; - Start_Offsets (0) := 0; - Last_Offsets (0) := Off; - Start_Offsets (1) := Off + 1; - Last_Offsets (1) := Off + 1; - Parts (Off + 1) := Final_State; - - -- Now the hard work. - loop - Stable := True; - -- For every partition - for P in 0 .. Last_Part loop - Off := Start_Offsets (P); - First_S := Parts (Off); - Off := Off + 1; - - -- For every S != First_S in P. - Last_Off := Last_Offsets (P); - Stable1 := True; - while Off <= Last_Off loop - S := Parts (Off); - - if not Is_Equivalent (First_S, S) then - -- Swap S with the last element of the partition. - Parts (Off) := Parts (Last_Off); - Parts (Last_Off) := S; - -- Reduce partition size. - Last_Off := Last_Off - 1; - Last_Offsets (P) := Last_Off; - - if Stable1 then - -- Create a new partition. - Last_Part := Last_Part + 1; - Last_Offsets (Last_Part) := Last_Off + 1; - Stable1 := False; - end if; - -- Put S in the new partition. - Start_Offsets (Last_Part) := Last_Off + 1; - State_Part (S) := Last_Part; - Stable := False; - - -- And continue with the swapped state. - else - Off := Off + 1; - end if; - end loop; - end loop; - exit when Stable; - end loop; - end Find_Partitions; - pragma Unreferenced (Find_Partitions); -end PSL.Optimize; diff --git a/psl/psl-optimize.ads b/psl/psl-optimize.ads deleted file mode 100644 index 5f36a0739..000000000 --- a/psl/psl-optimize.ads +++ /dev/null @@ -1,24 +0,0 @@ -with PSL.NFAs; use PSL.NFAs; -with PSL.Nodes; use PSL.Nodes; - -package PSL.Optimize is - -- Remove unreachable states, ie - -- * states that can't be reach from the start state. - -- * states that can't reach the final state. - -- O(N) algorithm. - procedure Remove_Unreachable_States (N : NFA); - - -- Remove single prefix, ie edges to a state S that is also from start - -- to S. - -- O(M) algorithm. - procedure Remove_Simple_Prefix (N : NFA); - - procedure Merge_Identical_States (N : NFA); - - procedure Merge_Edges (N : NFA); - - procedure Remove_Identical_Src_Edges (S : NFA_State); - procedure Remove_Identical_Dest_Edges (S : NFA_State); - - --procedure Find_Partitions (N : NFA; Nbr_States : Natural); -end PSL.Optimize; diff --git a/psl/psl-prints.adb b/psl/psl-prints.adb deleted file mode 100644 index 80da47dab..000000000 --- a/psl/psl-prints.adb +++ /dev/null @@ -1,433 +0,0 @@ -with Types; use Types; -with PSL.Errors; use PSL.Errors; -with Name_Table; use Name_Table; -with Ada.Text_IO; use Ada.Text_IO; - -package body PSL.Prints is - function Get_Priority (N : Node) return Priority is - begin - case Get_Kind (N) is - when N_Never | N_Always => - return Prio_FL_Invariance; - when N_Eventually - | N_Next - | N_Next_A - | N_Next_E - | N_Next_Event - | N_Next_Event_A - | N_Next_Event_E => - return Prio_FL_Occurence; - when N_Braced_SERE => - return Prio_SERE_Brace; - when N_Concat_SERE => - return Prio_Seq_Concat; - when N_Fusion_SERE => - return Prio_Seq_Fusion; - when N_Within_SERE => - return Prio_Seq_Within; - when N_Match_And_Seq - | N_And_Seq => - return Prio_Seq_And; - when N_Or_Seq => - return Prio_Seq_Or; - when N_Until - | N_Before => - return Prio_FL_Bounding; - when N_Abort => - return Prio_FL_Abort; - when N_Or_Prop => - return Prio_Seq_Or; - when N_And_Prop => - return Prio_Seq_And; - when N_Imp_Seq - | N_Overlap_Imp_Seq - | N_Log_Imp_Prop - | N_Imp_Bool => - return Prio_Bool_Imp; - when N_Name_Decl - | N_Number - | N_True - | N_False - | N_EOS - | N_HDL_Expr => - return Prio_HDL; - when N_Or_Bool => - return Prio_Seq_Or; - when N_And_Bool => - return Prio_Seq_And; - when N_Not_Bool => - return Prio_Bool_Not; - when N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Equal_Repeat_Seq - | N_Plus_Repeat_Seq => - return Prio_SERE_Repeat; - when N_Strong => - return Prio_Strong; - when others => - Error_Kind ("get_priority", N); - end case; - end Get_Priority; - - procedure Print_HDL_Expr (N : HDL_Node) is - begin - Put (Image (Get_Identifier (Node (N)))); - end Print_HDL_Expr; - - procedure Dump_Expr (N : Node) - is - begin - case Get_Kind (N) is - when N_HDL_Expr => - if HDL_Expr_Printer = null then - Put ("Expr"); - else - HDL_Expr_Printer.all (Get_HDL_Node (N)); - end if; - when N_True => - Put ("TRUE"); - when N_False => - Put ("FALSE"); - when N_Not_Bool => - Put ("!"); - Dump_Expr (Get_Boolean (N)); - when N_And_Bool => - Put ("("); - Dump_Expr (Get_Left (N)); - Put (" && "); - Dump_Expr (Get_Right (N)); - Put (")"); - when N_Or_Bool => - Put ("("); - Dump_Expr (Get_Left (N)); - Put (" || "); - Dump_Expr (Get_Right (N)); - Put (")"); - when others => - PSL.Errors.Error_Kind ("dump_expr", N); - end case; - end Dump_Expr; - - procedure Print_Expr (N : Node; Parent_Prio : Priority := Prio_Lowest) - is - Prio : Priority; - begin - if N = Null_Node then - Put ("."); - return; - end if; - Prio := Get_Priority (N); - if Prio < Parent_Prio then - Put ("("); - end if; - case Get_Kind (N) is - when N_Number => - declare - Str : constant String := Uns32'Image (Get_Value (N)); - begin - Put (Str (2 .. Str'Last)); - end; - when N_Name_Decl => - Put (Image (Get_Identifier (N))); - when N_HDL_Expr => - if HDL_Expr_Printer = null then - Put ("HDL_Expr"); - else - HDL_Expr_Printer.all (Get_HDL_Node (N)); - end if; - -- FIXME: this is true only when using the scanner. - -- Print_Expr (Node (Get_HDL_Node (N))); - when N_True => - Put ("TRUE"); - when N_False => - Put ("FALSE"); - when N_EOS => - Put ("EOS"); - when N_Not_Bool => - Put ("!"); - Print_Expr (Get_Boolean (N), Prio); - when N_And_Bool => - Print_Expr (Get_Left (N), Prio); - Put (" && "); - Print_Expr (Get_Right (N), Prio); - when N_Or_Bool => - Print_Expr (Get_Left (N), Prio); - Put (" || "); - Print_Expr (Get_Right (N), Prio); - when N_Imp_Bool => - Print_Expr (Get_Left (N), Prio); - Put (" -> "); - Print_Expr (Get_Right (N), Prio); - when others => - Error_Kind ("print_expr", N); - end case; - if Prio < Parent_Prio then - Put (")"); - end if; - end Print_Expr; - - procedure Print_Sequence (Seq : Node; Parent_Prio : Priority); - - procedure Print_Count (N : Node) is - B : Node; - begin - B := Get_Low_Bound (N); - if B = Null_Node then - return; - end if; - Print_Expr (B); - B := Get_High_Bound (N); - if B = Null_Node then - return; - end if; - Put (":"); - Print_Expr (B); - end Print_Count; - - procedure Print_Binary_Sequence (Name : String; N : Node; Prio : Priority) - is - begin - Print_Sequence (Get_Left (N), Prio); - Put (Name); - Print_Sequence (Get_Right (N), Prio); - end Print_Binary_Sequence; - - procedure Print_Repeat_Sequence (Name : String; N : Node) is - S : Node; - begin - S := Get_Sequence (N); - if S /= Null_Node then - Print_Sequence (S, Prio_SERE_Repeat); - end if; - Put (Name); - Print_Count (N); - Put ("]"); - end Print_Repeat_Sequence; - - procedure Print_Sequence (Seq : Node; Parent_Prio : Priority) - is - Prio : constant Priority := Get_Priority (Seq); - Add_Paren : constant Boolean := Prio < Parent_Prio - or else Parent_Prio <= Prio_FL_Paren; - begin - if Add_Paren then - Put ("{"); - end if; - case Get_Kind (Seq) is - when N_Braced_SERE => - Put ("{"); - Print_Sequence (Get_SERE (Seq), Prio_Lowest); - Put ("}"); - when N_Concat_SERE => - Print_Binary_Sequence (";", Seq, Prio); - when N_Fusion_SERE => - Print_Binary_Sequence (":", Seq, Prio); - when N_Within_SERE => - Print_Binary_Sequence (" within ", Seq, Prio); - when N_Match_And_Seq => - Print_Binary_Sequence (" && ", Seq, Prio); - when N_Or_Seq => - Print_Binary_Sequence (" | ", Seq, Prio); - when N_And_Seq => - Print_Binary_Sequence (" & ", Seq, Prio); - when N_Star_Repeat_Seq => - Print_Repeat_Sequence ("[*", Seq); - when N_Goto_Repeat_Seq => - Print_Repeat_Sequence ("[->", Seq); - when N_Equal_Repeat_Seq => - Print_Repeat_Sequence ("[=", Seq); - when N_Plus_Repeat_Seq => - Print_Sequence (Get_Sequence (Seq), Prio); - Put ("[+]"); - when N_Booleans - | N_Name_Decl => - Print_Expr (Seq); - when others => - Error_Kind ("print_sequence", Seq); - end case; - if Add_Paren then - Put ("}"); - end if; - end Print_Sequence; - - procedure Print_Binary_Property (Name : String; N : Node; Prio : Priority) - is - begin - Print_Property (Get_Left (N), Prio); - Put (Name); - Print_Property (Get_Right (N), Prio); - end Print_Binary_Property; - - procedure Print_Binary_Property_SI (Name : String; - N : Node; Prio : Priority) - is - begin - Print_Property (Get_Left (N), Prio); - Put (Name); - if Get_Strong_Flag (N) then - Put ('!'); - end if; - if Get_Inclusive_Flag (N) then - Put ('_'); - end if; - Put (' '); - Print_Property (Get_Right (N), Prio); - end Print_Binary_Property_SI; - - procedure Print_Range_Property (Name : String; N : Node) is - begin - Put (Name); - Put ("["); - Print_Count (N); - Put ("]("); - Print_Property (Get_Property (N), Prio_FL_Paren); - Put (")"); - end Print_Range_Property; - - procedure Print_Boolean_Range_Property (Name : String; N : Node) is - begin - Put (Name); - Put ("("); - Print_Expr (Get_Boolean (N)); - Put (")["); - Print_Count (N); - Put ("]("); - Print_Property (Get_Property (N), Prio_FL_Paren); - Put (")"); - end Print_Boolean_Range_Property; - - procedure Print_Property (Prop : Node; - Parent_Prio : Priority := Prio_Lowest) - is - Prio : constant Priority := Get_Priority (Prop); - begin - if Prio < Parent_Prio then - Put ("("); - end if; - case Get_Kind (Prop) is - when N_Never => - Put ("never "); - Print_Property (Get_Property (Prop), Prio); - when N_Always => - Put ("always ("); - Print_Property (Get_Property (Prop), Prio); - Put (")"); - when N_Eventually => - Put ("eventually! ("); - Print_Property (Get_Property (Prop), Prio); - Put (")"); - when N_Strong => - Print_Property (Get_Property (Prop), Prio); - Put ("!"); - when N_Next => - Put ("next"); --- if Get_Strong_Flag (Prop) then --- Put ('!'); --- end if; - Put (" ("); - Print_Property (Get_Property (Prop), Prio); - Put (")"); - when N_Next_A => - Print_Range_Property ("next_a", Prop); - when N_Next_E => - Print_Range_Property ("next_e", Prop); - when N_Next_Event => - Put ("next_event"); - Put ("("); - Print_Expr (Get_Boolean (Prop)); - Put (")("); - Print_Property (Get_Property (Prop), Prio); - Put (")"); - when N_Next_Event_A => - Print_Boolean_Range_Property ("next_event_a", Prop); - when N_Next_Event_E => - Print_Boolean_Range_Property ("next_event_e", Prop); - when N_Until => - Print_Binary_Property_SI (" until", Prop, Prio); - when N_Abort => - Print_Property (Get_Property (Prop), Prio); - Put (" abort "); - Print_Expr (Get_Boolean (Prop)); - when N_Before => - Print_Binary_Property_SI (" before", Prop, Prio); - when N_Or_Prop => - Print_Binary_Property (" || ", Prop, Prio); - when N_And_Prop => - Print_Binary_Property (" && ", Prop, Prio); - when N_Imp_Seq => - Print_Property (Get_Sequence (Prop), Prio); - Put (" |=> "); - Print_Property (Get_Property (Prop), Prio); - when N_Overlap_Imp_Seq => - Print_Property (Get_Sequence (Prop), Prio); - Put (" |-> "); - Print_Property (Get_Property (Prop), Prio); - when N_Log_Imp_Prop => - Print_Binary_Property (" -> ", Prop, Prio); - when N_Booleans - | N_Name_Decl => - Print_Expr (Prop); - when N_Sequences => - Print_Sequence (Prop, Parent_Prio); - when others => - Error_Kind ("print_property", Prop); - end case; - if Prio < Parent_Prio then - Put (")"); - end if; - end Print_Property; - - procedure Print_Assert (N : Node) is - Label : Name_Id; - begin - Put (" "); - Label := Get_Label (N); - if Label /= Null_Identifier then - Put (Image (Label)); - Put (": "); - end if; - Put ("assert "); - Print_Property (Get_Property (N)); - Put_Line (";"); - end Print_Assert; - - procedure Print_Property_Declaration (N : Node) is - begin - Put (" "); - Put ("property "); - Put (Image (Get_Identifier (N))); - Put (" = "); - Print_Property (Get_Property (N)); - Put_Line (";"); - end Print_Property_Declaration; - - procedure Print_Unit (Unit : Node) is - Item : Node; - begin - case Get_Kind (Unit) is - when N_Vunit => - Put ("vunit"); - when others => - Error_Kind ("disp_unit", Unit); - end case; - Put (' '); - Put (Image (Get_Identifier (Unit))); - Put_Line (" {"); - Item := Get_Item_Chain (Unit); - while Item /= Null_Node loop - case Get_Kind (Item) is - when N_Name_Decl => - null; - when N_Assert_Directive => - Print_Assert (Item); - when N_Property_Declaration => - Print_Property_Declaration (Item); - when others => - Error_Kind ("disp_unit", Item); - end case; - Item := Get_Chain (Item); - end loop; - Put_Line ("}"); - end Print_Unit; -end PSL.Prints; - diff --git a/psl/psl-prints.ads b/psl/psl-prints.ads deleted file mode 100644 index 18a36f78f..000000000 --- a/psl/psl-prints.ads +++ /dev/null @@ -1,20 +0,0 @@ -with PSL.Nodes; use PSL.Nodes; -with PSL.Priorities; use PSL.Priorities; - -package PSL.Prints is - procedure Print_Unit (Unit : Node); - procedure Print_Property (Prop : Node; - Parent_Prio : Priority := Prio_Lowest); - procedure Print_Expr (N : Node; Parent_Prio : Priority := Prio_Lowest); - - -- Procedure to display HDL_Expr nodes. - type HDL_Expr_Printer_Acc is access procedure (N : HDL_Node); - HDL_Expr_Printer : HDL_Expr_Printer_Acc; - - procedure Print_HDL_Expr (N : HDL_Node); - - -- Like Print_Expr but always put parenthesis. - procedure Dump_Expr (N : Node); - -end PSL.Prints; - diff --git a/psl/psl-priorities.ads b/psl/psl-priorities.ads deleted file mode 100644 index cb49239e4..000000000 --- a/psl/psl-priorities.ads +++ /dev/null @@ -1,63 +0,0 @@ -package PSL.Priorities is - -- Operator priorities, defined by PSL1.1 4.2.3.2 - type Priority is - ( - Prio_Lowest, - - -- always, never, G - Prio_FL_Invariance, - - -- ->, <-> - Prio_Bool_Imp, - - -- |->, |=> - Prio_Seq_Imp, - - -- U, W, until*, before* - Prio_FL_Bounding, - - -- next*, eventually!, X, X!, F - Prio_FL_Occurence, - - -- abort - Prio_FL_Abort, - - -- ( ) - Prio_FL_Paren, - - -- ; - Prio_Seq_Concat, - - -- : - Prio_Seq_Fusion, - - -- | - Prio_Seq_Or, - - -- &, && - Prio_Seq_And, - - -- within - Prio_Seq_Within, - - -- [*], [+], [=], [->] - Prio_SERE_Repeat, - - -- { } - Prio_SERE_Brace, - - -- @ - Prio_Clock_Event, - - -- ! - Prio_Strong, - - -- union - Prio_Union, - - -- ! - Prio_Bool_Not, - - Prio_HDL - ); -end PSL.Priorities; diff --git a/psl/psl-qm.adb b/psl/psl-qm.adb deleted file mode 100644 index f5b5e1db3..000000000 --- a/psl/psl-qm.adb +++ /dev/null @@ -1,318 +0,0 @@ -with Ada.Text_IO; -with Types; use Types; -with PSL.Errors; use PSL.Errors; -with PSL.Prints; -with PSL.CSE; - -package body PSL.QM is - procedure Reset is - begin - for I in 1 .. Nbr_Terms loop - Set_HDL_Index (Term_Assoc (I), 0); - end loop; - Nbr_Terms := 0; - Term_Assoc := (others => Null_Node); - end Reset; - - function Term (P : Natural) return Vector_Type is - begin - return Shift_Left (1, P - 1); - end Term; - - procedure Disp_Primes_Set (Ps : Primes_Set) - is - use Ada.Text_IO; - use PSL.Prints; - Prime : Prime_Type; - T : Vector_Type; - First_Term : Boolean; - begin - if Ps.Nbr = 0 then - Put ("FALSE"); - return; - end if; - for I in 1 .. Ps.Nbr loop - Prime := Ps.Set (I); - if I /= 1 then - Put (" | "); - end if; - if Prime.Set = 0 then - Put ("TRUE"); - else - First_Term := True; - for J in 1 .. Max_Terms loop - T := Term (J); - if (Prime.Set and T) /= 0 then - if First_Term then - First_Term := False; - else - Put ('.'); - end if; - if (Prime.Val and T) = 0 then - Put ('!'); - end if; - Print_Expr (Term_Assoc (J)); - end if; - end loop; - end if; - end loop; - end Disp_Primes_Set; - - -- Return TRUE iff L includes R, ie - -- for all x, x in L => x in R. - function Included (L, R : Prime_Type) return Boolean is - begin - return ((L.Set or R.Set) = L.Set) - and then ((L.Val and R.Set) = (R.Val and R.Set)); - end Included; - - -- Return TRUE iff L and R have the same don't care set - -- and L and R can be merged into a new prime with a new don't care. - function Is_One_Change_Same (L, R : Prime_Type) return Boolean - is - V : Vector_Type; - begin - if L.Set /= R.Set then - return False; - end if; - V := L.Val xor R.Val; - return (V and -V) = V; - end Is_One_Change_Same; - - -- Return true iff L can add a new DC in R. - function Is_One_Change (L, R : Prime_Type) return Boolean - is - V : Vector_Type; - begin - if (L.Set or R.Set) /= R.Set then - return False; - end if; - V := (L.Val xor R.Val) and L.Set; - return (V and -V) = V; - end Is_One_Change; - - procedure Merge (Ps : in out Primes_Set; P : Prime_Type) - is - Do_Append : Boolean := True; - T : Prime_Type; - begin - for I in 1 .. Ps.Nbr loop - T := Ps.Set (I); - if Included (P, T) then - -- Already in the set. - return; - end if; - if Included (T, P) then - Ps.Set (I) := P; - Do_Append := False; - else - if Is_One_Change_Same (P, T) then - declare - V : constant Vector_Type := T.Val xor P.Val; - begin - Ps.Set (I).Set := T.Set and not V; - Ps.Set (I).Val := T.Val and not V; - end; - Do_Append := False; - end if; - if Is_One_Change (P, T) then - declare - V : constant Vector_Type := (T.Val xor P.Val) and P.Set; - begin - Ps.Set (I).Set := T.Set and not V; - Ps.Set (I).Val := T.Val and not V; - end; - -- continue. - end if; - end if; - end loop; - if Do_Append then - Ps.Nbr := Ps.Nbr + 1; - Ps.Set (Ps.Nbr) := P; - end if; - end Merge; - - function Build_Primes_And (L, R : Primes_Set) return Primes_Set - is - Res : Primes_Set (L.Nbr * R.Nbr); - L_P, R_P : Prime_Type; - P : Prime_Type; - begin - for I in 1 .. L.Nbr loop - L_P := L.Set (I); - for J in 1 .. R.Nbr loop - R_P := R.Set (J); - -- In case of conflict, discard. - if ((L_P.Val xor R_P.Val) and (L_P.Set and R_P.Set)) /= 0 then - null; - else - P.Set := L_P.Set or R_P.Set; - P.Val := (R_P.Set and R_P.Val) - or ((L_P.Set and not R_P.Set) and L_P.Val); - Merge (Res, P); - end if; - end loop; - end loop; - - return Res; - end Build_Primes_And; - - - function Build_Primes_Or (L, R : Primes_Set) return Primes_Set - is - Res : Primes_Set (L.Nbr + R.Nbr); - L_P, R_P : Prime_Type; - begin - for I in 1 .. L.Nbr loop - L_P := L.Set (I); - Merge (Res, L_P); - end loop; - for J in 1 .. R.Nbr loop - R_P := R.Set (J); - Merge (Res, R_P); - end loop; - - return Res; - end Build_Primes_Or; - - function Build_Primes (N : Node; Negate : Boolean) return Primes_Set is - begin - case Get_Kind (N) is - when N_HDL_Expr - | N_EOS => - declare - Res : Primes_Set (1); - Index : Int32; - T : Vector_Type; - begin - Index := Get_HDL_Index (N); - if Index = 0 then - Nbr_Terms := Nbr_Terms + 1; - if Nbr_Terms > Max_Terms then - raise Program_Error; - end if; - Term_Assoc (Nbr_Terms) := N; - Index := Int32 (Nbr_Terms); - Set_HDL_Index (N, Index); - else - if Index not in 1 .. Int32 (Nbr_Terms) - or else Term_Assoc (Natural (Index)) /= N - then - raise Internal_Error; - end if; - end if; - T := Term (Natural (Index)); - Res.Nbr := 1; - Res.Set (1).Set := T; - if Negate then - Res.Set (1).Val := 0; - else - Res.Set (1).Val := T; - end if; - return Res; - end; - when N_False => - declare - Res : Primes_Set (0); - begin - return Res; - end; - when N_True => - declare - Res : Primes_Set (1); - begin - Res.Nbr := 1; - Res.Set (1).Set := 0; - Res.Set (1).Val := 0; - return Res; - end; - when N_Not_Bool => - return Build_Primes (Get_Boolean (N), not Negate); - when N_And_Bool => - if Negate then - -- !(a & b) <-> !a || !b - return Build_Primes_Or (Build_Primes (Get_Left (N), True), - Build_Primes (Get_Right (N), True)); - else - return Build_Primes_And (Build_Primes (Get_Left (N), False), - Build_Primes (Get_Right (N), False)); - end if; - when N_Or_Bool => - if Negate then - -- !(a || b) <-> !a && !b - return Build_Primes_And (Build_Primes (Get_Left (N), True), - Build_Primes (Get_Right (N), True)); - else - return Build_Primes_Or (Build_Primes (Get_Left (N), False), - Build_Primes (Get_Right (N), False)); - end if; - when N_Imp_Bool => - if not Negate then - -- a -> b <-> !a || b - return Build_Primes_Or (Build_Primes (Get_Left (N), True), - Build_Primes (Get_Right (N), False)); - else - -- !(a -> b) <-> a && !b - return Build_Primes_And (Build_Primes (Get_Left (N), False), - Build_Primes (Get_Right (N), True)); - end if; - when others => - Error_Kind ("build_primes", N); - end case; - end Build_Primes; - - function Build_Primes (N : Node) return Primes_Set is - begin - return Build_Primes (N, False); - end Build_Primes; - - function Build_Node (P : Prime_Type) return Node - is - Res : Node := Null_Node; - N : Node; - S : Vector_Type := P.Set; - T : Vector_Type; - begin - if S = 0 then - return True_Node; - end if; - for I in Natural range 1 .. Vector_Type'Modulus loop - T := Term (I); - if (S and T) /= 0 then - N := Term_Assoc (I); - if (P.Val and T) = 0 then - N := PSL.CSE.Build_Bool_Not (N); - end if; - if Res = Null_Node then - Res := N; - else - Res := PSL.CSE.Build_Bool_And (Res, N); - end if; - S := S and not T; - exit when S = 0; - end if; - end loop; - return Res; - end Build_Node; - - function Build_Node (Ps : Primes_Set) return Node - is - Res : Node; - begin - if Ps.Nbr = 0 then - return False_Node; - else - Res := Build_Node (Ps.Set (1)); - for I in 2 .. Ps.Nbr loop - Res := PSL.CSE.Build_Bool_Or (Res, Build_Node (Ps.Set (I))); - end loop; - return Res; - end if; - end Build_Node; - - -- FIXME: finish the work: do a real Quine-McKluskey minimization. - function Reduce (N : Node) return Node is - begin - return Build_Node (Build_Primes (N)); - end Reduce; -end PSL.QM; diff --git a/psl/psl-qm.ads b/psl/psl-qm.ads deleted file mode 100644 index 85f1e3cf4..000000000 --- a/psl/psl-qm.ads +++ /dev/null @@ -1,49 +0,0 @@ -with PSL.Nodes; use PSL.Nodes; -with Interfaces; use Interfaces; - -package PSL.QM is - type Primes_Set (<>) is private; - - function Build_Primes (N : Node) return Primes_Set; - - function Build_Node (Ps : Primes_Set) return Node; - - function Reduce (N : Node) return Node; - - -- The maximum number of terms that this package can handle. - -- The algorithm is in O(2**n) - Max_Terms : constant Natural := 12; - - type Term_Assoc_Type is array (1 .. Max_Terms) of Node; - Term_Assoc : Term_Assoc_Type := (others => Null_Node); - Nbr_Terms : Natural := 0; - - procedure Reset; - - procedure Disp_Primes_Set (Ps : Primes_Set); -private - -- Scalar type used to represent a vector of booleans for terms. - subtype Vector_Type is Unsigned_16; - pragma Assert (Vector_Type'Modulus >= 2 ** Max_Terms); - - -- States of a vector of term. - -- If SET is 0, this is a don't care: the term has no influence. - -- If SET is 1, the value of the term is in VAL. - type Prime_Type is record - Val : Unsigned_16; - Set : Unsigned_16; - end record; - - subtype Len_Type is Natural range 0 .. 2 ** Max_Terms; - - type Set_Type is array (Natural range <>) of Prime_Type; - - -- A set of primes is a collection of at most MAX prime. - type Primes_Set (Max : Len_Type) is record - Nbr : Len_Type := 0; - Set : Set_Type (1 .. Max); - end record; -end PSL.QM; - - - diff --git a/psl/psl-rewrites.adb b/psl/psl-rewrites.adb deleted file mode 100644 index 6ba5b1026..000000000 --- a/psl/psl-rewrites.adb +++ /dev/null @@ -1,604 +0,0 @@ -with Types; use Types; -with PSL.Errors; use PSL.Errors; -with PSL.CSE; use PSL.CSE; - -package body PSL.Rewrites is --- procedure Location_Copy (Dst, Src : Node) is --- begin --- Set_Location (Dst, Get_Location (Src)); --- end Location_Copy; - - -- Return [*0] - function Build_Empty return Node is - Res, Tmp : Node; - begin - Res := Create_Node (N_Star_Repeat_Seq); - Tmp := Create_Node (N_Number); - Set_Value (Tmp, 0); - Set_Low_Bound (Res, Tmp); - return Res; - end Build_Empty; - - -- Return N[*] - function Build_Star (N : Node) return Node is - Res : Node; - begin - Res := Create_Node (N_Star_Repeat_Seq); - Set_Sequence (Res, N); - return Res; - end Build_Star; - - -- Return N[+] - function Build_Plus (N : Node) return Node is - Res : Node; - begin - Res := Create_Node (N_Plus_Repeat_Seq); - Set_Sequence (Res, N); - return Res; - end Build_Plus; - - -- Return N! - function Build_Strong (N : Node) return Node is - Res : Node; - begin - Res := Create_Node (N_Strong); - Set_Property (Res, N); - return Res; - end Build_Strong; - - -- Return T[*] - function Build_True_Star return Node is - begin - return Build_Star (True_Node); - end Build_True_Star; - - function Build_Binary (K : Nkind; L, R : Node) return Node is - Res : Node; - begin - Res := Create_Node (K); - Set_Left (Res, L); - Set_Right (Res, R); - return Res; - end Build_Binary; - - function Build_Concat (L, R : Node) return Node is - begin - return Build_Binary (N_Concat_SERE, L, R); - end Build_Concat; - - function Build_Repeat (N : Node; Cnt : Uns32) return Node is - Res : Node; - begin - if Cnt = 0 then - raise Internal_Error; - end if; - Res := N; - for I in 2 .. Cnt loop - Res := Build_Concat (Res, N); - end loop; - return Res; - end Build_Repeat; - - function Build_Overlap_Imp_Seq (S : Node; P : Node) return Node - is - Res : Node; - begin - Res := Create_Node (N_Overlap_Imp_Seq); - Set_Sequence (Res, S); - Set_Property (Res, P); - return Res; - end Build_Overlap_Imp_Seq; - - function Rewrite_Boolean (N : Node) return Node - is - Res : Node; - begin - case Get_Kind (N) is - when N_Name => - Res := Get_Decl (N); - pragma Assert (Res /= Null_Node); - return Res; - when N_Not_Bool => - Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); - return N; - when N_And_Bool - | N_Or_Bool - | N_Imp_Bool => - Set_Left (N, Rewrite_Boolean (Get_Left (N))); - Set_Right (N, Rewrite_Boolean (Get_Right (N))); - return N; - when N_HDL_Expr => - return N; - when others => - Error_Kind ("rewrite_boolean", N); - end case; - end Rewrite_Boolean; - - function Rewrite_Star_Repeat_Seq (Seq : Node; - Lo, Hi : Uns32) return Node - is - Res : Node; - begin - pragma Assert (Lo <= Hi); - - if Lo = Hi then - - if Lo = 0 then - -- r[*0] --> [*0] - return Build_Empty; - elsif Lo = 1 then - -- r[*1] --> r - return Seq; - end if; - -- r[*c+] --> r;r;r...;r (c times) - return Build_Repeat (Seq, Lo); - end if; - - -- r[*0:1] --> [*0] | r - -- r[*0:2] --> [*0] | r;{[*0]|r} - - -- r[*0:n] --> [*0] | r;r[*0:n-1] - -- r[*l:h] --> r[*l] ; r[*0:h-l] - Res := Build_Binary (N_Or_Seq, Build_Empty, Seq); - for I in Lo + 2 .. Hi loop - Res := Build_Concat (Seq, Res); - Res := Build_Binary (N_Or_Seq, Build_Empty, Res); - end loop; - if Lo > 0 then - Res := Build_Concat (Build_Repeat (Seq, Lo), Res); - end if; - - return Res; - end Rewrite_Star_Repeat_Seq; - - function Rewrite_Star_Repeat_Seq (Seq : Node; - Lo, Hi : Node) return Node - is - Cnt_Lo : Uns32; - Cnt_Hi : Uns32; - begin - if Lo = Null_Node then - -- r[*] - raise Program_Error; - end if; - - Cnt_Lo := Get_Value (Lo); - if Hi = Null_Node then - Cnt_Hi := Cnt_Lo; - else - Cnt_Hi := Get_Value (Hi); - end if; - return Rewrite_Star_Repeat_Seq (Seq, Cnt_Lo, Cnt_Hi); - end Rewrite_Star_Repeat_Seq; - - function Rewrite_Star_Repeat_Seq (N : Node) return Node - is - Seq : constant Node := Get_Sequence (N); - Lo : constant Node := Get_Low_Bound (N); - begin - if Lo = Null_Node then - -- r[*] --> r[*] - return N; - else - return Rewrite_Star_Repeat_Seq (Seq, Lo, Get_High_Bound (N)); - end if; - end Rewrite_Star_Repeat_Seq; - - function Rewrite_Goto_Repeat_Seq (Seq : Node; - Lo, Hi : Node) return Node is - Res : Node; - begin - -- b[->] --> {(~b)[*];b} - Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq); - - if Lo = Null_Node then - return Res; - end if; - - -- b[->l:h] --> {b[->]}[*l:h] - return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); - end Rewrite_Goto_Repeat_Seq; - - function Rewrite_Goto_Repeat_Seq (Seq : Node; - Lo, Hi : Uns32) return Node is - Res : Node; - begin - -- b[->] --> {(~b)[*];b} - Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq); - - -- b[->l:h] --> {b[->]}[*l:h] - return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); - end Rewrite_Goto_Repeat_Seq; - - function Rewrite_Equal_Repeat_Seq (N : Node) return Node - is - Seq : constant Node := Get_Sequence (N); - Lo : constant Node := Get_Low_Bound (N); - Hi : constant Node := Get_High_Bound (N); - begin - -- b[=l:h] --> {b[->l:h]};(~b)[*] - return Build_Concat (Rewrite_Goto_Repeat_Seq (Seq, Lo, Hi), - Build_Star (Build_Bool_Not (Seq))); - end Rewrite_Equal_Repeat_Seq; - - function Rewrite_Within (N : Node) return Node is - Res : Node; - begin - Res := Build_Concat (Build_Concat (Build_True_Star, Get_Left (N)), - Build_True_Star); - return Build_Binary (N_Match_And_Seq, Res, Get_Right (N)); - end Rewrite_Within; - - function Rewrite_And_Seq (L : Node; R : Node) return Node is - begin - return Build_Binary (N_Or_Seq, - Build_Binary (N_Match_And_Seq, - L, - Build_Concat (R, Build_True_Star)), - Build_Binary (N_Match_And_Seq, - Build_Concat (L, Build_True_Star), - R)); - end Rewrite_And_Seq; - pragma Unreferenced (Rewrite_And_Seq); - - procedure Rewrite_Instance (N : Node) - is - Assoc : Node := Get_Association_Chain (N); - begin - while Assoc /= Null_Node loop - case Get_Kind (Get_Formal (Assoc)) is - when N_Const_Parameter => - null; - when N_Boolean_Parameter => - Set_Actual (Assoc, Rewrite_Boolean (Get_Actual (Assoc))); - when N_Sequence_Parameter => - Set_Actual (Assoc, Rewrite_SERE (Get_Actual (Assoc))); - when N_Property_Parameter => - Set_Actual (Assoc, Rewrite_Property (Get_Actual (Assoc))); - when others => - Error_Kind ("rewrite_instance", - Get_Formal (Assoc)); - end case; - Assoc := Get_Chain (Assoc); - end loop; - end Rewrite_Instance; - - function Rewrite_SERE (N : Node) return Node is - S : Node; - begin - case Get_Kind (N) is - when N_Star_Repeat_Seq => - S := Get_Sequence (N); - if S = Null_Node then - S := True_Node; - else - S := Rewrite_SERE (S); - end if; - Set_Sequence (N, S); - return Rewrite_Star_Repeat_Seq (N); - when N_Plus_Repeat_Seq => - S := Get_Sequence (N); - if S = Null_Node then - S := True_Node; - else - S := Rewrite_SERE (S); - end if; - Set_Sequence (N, S); - return N; - when N_Goto_Repeat_Seq => - return Rewrite_Goto_Repeat_Seq - (Rewrite_SERE (Get_Sequence (N)), - Get_Low_Bound (N), Get_High_Bound (N)); - when N_Equal_Repeat_Seq => - Set_Sequence (N, Rewrite_SERE (Get_Sequence (N))); - return Rewrite_Equal_Repeat_Seq (N); - when N_Braced_SERE => - return Rewrite_SERE (Get_SERE (N)); - when N_Within_SERE => - Set_Left (N, Rewrite_SERE (Get_Left (N))); - Set_Right (N, Rewrite_SERE (Get_Right (N))); - return Rewrite_Within (N); --- when N_And_Seq => --- return Rewrite_And_Seq (Rewrite_SERE (Get_Left (N)), --- Rewrite_SERE (Get_Right (N))); - when N_Concat_SERE - | N_Fusion_SERE - | N_Match_And_Seq - | N_And_Seq - | N_Or_Seq => - Set_Left (N, Rewrite_SERE (Get_Left (N))); - Set_Right (N, Rewrite_SERE (Get_Right (N))); - return N; - when N_Booleans => - return Rewrite_Boolean (N); - when N_Name => - return Get_Decl (N); - when N_Sequence_Instance - | N_Endpoint_Instance => - Rewrite_Instance (N); - return N; - when N_Boolean_Parameter - | N_Sequence_Parameter - | N_Const_Parameter => - return N; - when others => - Error_Kind ("rewrite_SERE", N); - end case; - end Rewrite_SERE; - - function Rewrite_Until (N : Node) return Node - is - Res : Node; - B : Node; - L : Node; - S : Node; - begin - if Get_Inclusive_Flag (N) then - -- B1 until_ B2 --> {B1[+]:B2} - Res := Build_Binary (N_Fusion_SERE, - Build_Plus (Rewrite_Boolean (Get_Left (N))), - Rewrite_Boolean (Get_Right (N))); - if Get_Strong_Flag (N) then - Res := Build_Strong (Res); - end if; - else - -- P until B --> {(!B)[+]} |-> P - B := Rewrite_Boolean (Get_Right (N)); - L := Build_Plus (Build_Bool_Not (B)); - Res := Build_Overlap_Imp_Seq (L, Rewrite_Property (Get_Left (N))); - - if Get_Strong_Flag (N) then - -- p until! b --> (p until b) && ({b[->]}!) - S := Build_Strong - (Rewrite_Goto_Repeat_Seq (B, Null_Node, Null_Node)); - Res := Build_Binary (N_And_Prop, Res, S); - end if; - end if; - return Res; - end Rewrite_Until; - - function Rewrite_Next_Event_A (B : Node; - Lo, Hi : Uns32; - P : Node; - Strong : Boolean) return Node - is - Res : Node; - begin - Res := Rewrite_Goto_Repeat_Seq (B, Lo, Hi); - Res := Build_Overlap_Imp_Seq (Res, P); - - if Strong then - Res := Build_Binary - (N_And_Prop, - Res, - Build_Strong (Rewrite_Goto_Repeat_Seq (B, Lo, Lo))); - end if; - - return Res; - end Rewrite_Next_Event_A; - - function Rewrite_Next_Event (B : Node; - N : Uns32; - P : Node; - Strong : Boolean) return Node is - begin - return Rewrite_Next_Event_A (B, N, N, P, Strong); - end Rewrite_Next_Event; - - function Rewrite_Next_Event (B : Node; - Num : Node; - P : Node; - Strong : Boolean) return Node - is - N : Uns32; - begin - if Num = Null_Node then - N := 1; - else - N := Get_Value (Num); - end if; - return Rewrite_Next_Event (B, N, P, Strong); - end Rewrite_Next_Event; - - function Rewrite_Next (Num : Node; P : Node; Strong : Boolean) return Node - is - N : Uns32; - begin - if Num = Null_Node then - N := 1; - else - N := Get_Value (Num); - end if; - return Rewrite_Next_Event (True_Node, N + 1, P, Strong); - end Rewrite_Next; - - function Rewrite_Next_A (Lo, Hi : Uns32; - P : Node; Strong : Boolean) return Node - is - begin - return Rewrite_Next_Event_A (True_Node, Lo + 1, Hi + 1, P, Strong); - end Rewrite_Next_A; - - function Rewrite_Next_Event_E (B1 : Node; - Lo, Hi : Uns32; - B2 : Node; Strong : Boolean) return Node - is - Res : Node; - begin - Res := Build_Binary (N_Fusion_SERE, - Rewrite_Goto_Repeat_Seq (B1, Lo, Hi), - B2); - if Strong then - Res := Build_Strong (Res); - end if; - return Res; - end Rewrite_Next_Event_E; - - function Rewrite_Next_E (Lo, Hi : Uns32; - B : Node; Strong : Boolean) return Node - is - begin - return Rewrite_Next_Event_E (True_Node, Lo + 1, Hi + 1, B, Strong); - end Rewrite_Next_E; - - function Rewrite_Before (N : Node) return Node - is - Res : Node; - R : Node; - B1, B2 : Node; - N_B2 : Node; - begin - B1 := Rewrite_Boolean (Get_Left (N)); - B2 := Rewrite_Boolean (Get_Right (N)); - N_B2 := Build_Bool_Not (B2); - Res := Build_Star (Build_Bool_And (Build_Bool_Not (B1), N_B2)); - - if Get_Inclusive_Flag (N) then - R := B2; - else - R := Build_Bool_And (B1, N_B2); - end if; - Res := Build_Concat (Res, R); - if Get_Strong_Flag (N) then - Res := Build_Strong (Res); - end if; - return Res; - end Rewrite_Before; - - function Rewrite_Or (L, R : Node) return Node - is - B, P : Node; - begin - if Get_Kind (L) in N_Booleans then - if Get_Kind (R) in N_Booleans then - return Build_Bool_Or (L, R); - else - B := L; - P := R; - end if; - elsif Get_Kind (R) in N_Booleans then - B := R; - P := L; - else - -- Not in the simple subset. - raise Program_Error; - end if; - - -- B || P --> (~B) -> P - return Build_Binary (N_Log_Imp_Prop, Build_Bool_Not (B), P); - end Rewrite_Or; - - function Rewrite_Property (N : Node) return Node is - begin - case Get_Kind (N) is - when N_Star_Repeat_Seq - | N_Plus_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Sequence_Instance - | N_Endpoint_Instance - | N_Braced_SERE => - return Rewrite_SERE (N); - when N_Imp_Seq - | N_Overlap_Imp_Seq => - Set_Sequence (N, Rewrite_Property (Get_Sequence (N))); - Set_Property (N, Rewrite_Property (Get_Property (N))); - return N; - when N_Log_Imp_Prop => - -- b -> p --> {b} |-> p - return Build_Overlap_Imp_Seq - (Rewrite_Boolean (Get_Left (N)), - Rewrite_Property (Get_Right (N))); - when N_Eventually => - return Build_Strong - (Build_Binary (N_Fusion_SERE, - Build_Plus (True_Node), - Rewrite_SERE (Get_Property (N)))); - when N_Until => - return Rewrite_Until (N); - when N_Next => - return Rewrite_Next (Get_Number (N), - Rewrite_Property (Get_Property (N)), - Get_Strong_Flag (N)); - when N_Next_Event => - return Rewrite_Next_Event (Rewrite_Boolean (Get_Boolean (N)), - Get_Number (N), - Rewrite_Property (Get_Property (N)), - Get_Strong_Flag (N)); - when N_Next_A => - return Rewrite_Next_A (Get_Value (Get_Low_Bound (N)), - Get_Value (Get_High_Bound (N)), - Rewrite_Property (Get_Property (N)), - Get_Strong_Flag (N)); - when N_Next_Event_A => - return Rewrite_Next_Event_A - (Rewrite_Boolean (Get_Boolean (N)), - Get_Value (Get_Low_Bound (N)), - Get_Value (Get_High_Bound (N)), - Rewrite_Property (Get_Property (N)), - Get_Strong_Flag (N)); - when N_Next_E => - return Rewrite_Next_E (Get_Value (Get_Low_Bound (N)), - Get_Value (Get_High_Bound (N)), - Rewrite_Property (Get_Property (N)), - Get_Strong_Flag (N)); - when N_Next_Event_E => - return Rewrite_Next_Event_E - (Rewrite_Boolean (Get_Boolean (N)), - Get_Value (Get_Low_Bound (N)), - Get_Value (Get_High_Bound (N)), - Rewrite_Property (Get_Property (N)), - Get_Strong_Flag (N)); - when N_Before => - return Rewrite_Before (N); - when N_Booleans => - return Rewrite_Boolean (N); - when N_Name => - return Get_Decl (N); - when N_Never - | N_Always - | N_Strong => - -- Fully handled by psl.build - Set_Property (N, Rewrite_Property (Get_Property (N))); - return N; - when N_Clock_Event => - Set_Property (N, Rewrite_Property (Get_Property (N))); - Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); - return N; - when N_And_Prop => - Set_Left (N, Rewrite_Property (Get_Left (N))); - Set_Right (N, Rewrite_Property (Get_Right (N))); - return N; - when N_Or_Prop => - return Rewrite_Or (Rewrite_Property (Get_Left (N)), - Rewrite_Property (Get_Right (N))); - when N_Abort => - Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); - Set_Property (N, Rewrite_Property (Get_Property (N))); - return N; - when N_Property_Instance => - Rewrite_Instance (N); - return N; - when others => - Error_Kind ("rewrite_property", N); - end case; - end Rewrite_Property; - - procedure Rewrite_Unit (N : Node) is - Item : Node; - begin - Item := Get_Item_Chain (N); - while Item /= Null_Node loop - case Get_Kind (Item) is - when N_Name_Decl => - null; - when N_Assert_Directive => - Set_Property (Item, Rewrite_Property (Get_Property (Item))); - when N_Property_Declaration => - Set_Property (Item, Rewrite_Property (Get_Property (Item))); - when others => - Error_Kind ("rewrite_unit", Item); - end case; - Item := Get_Chain (Item); - end loop; - end Rewrite_Unit; -end PSL.Rewrites; diff --git a/psl/psl-rewrites.ads b/psl/psl-rewrites.ads deleted file mode 100644 index ac76b7805..000000000 --- a/psl/psl-rewrites.ads +++ /dev/null @@ -1,7 +0,0 @@ -with PSL.Nodes; use PSL.Nodes; - -package PSL.Rewrites is - function Rewrite_SERE (N : Node) return Node; - function Rewrite_Property (N : Node) return Node; - procedure Rewrite_Unit (N : Node); -end PSL.Rewrites; diff --git a/psl/psl-subsets.adb b/psl/psl-subsets.adb deleted file mode 100644 index f322eafda..000000000 --- a/psl/psl-subsets.adb +++ /dev/null @@ -1,177 +0,0 @@ -with PSL.Errors; use PSL.Errors; -with Types; use Types; - -package body PSL.Subsets is - procedure Check_Simple (N : Node) - is - begin - case Get_Kind (N) is - when N_Not_Bool => - if Get_Psl_Type (Get_Boolean (N)) /= Type_Boolean then - Error_Msg_Sem - ("operand of a negation operator must be a boolean", N); - end if; - when N_Never => - case Get_Psl_Type (Get_Property (N)) is - when Type_Sequence | Type_Boolean => - null; - when others => - Error_Msg_Sem ("operand of a 'never' operator must be " - & "a boolean or a sequence", N); - end case; - when N_Eventually => - case Get_Psl_Type (Get_Property (N)) is - when Type_Sequence | Type_Boolean => - null; - when others => - Error_Msg_Sem ("operand of an 'eventually!' operator must be" - & " a boolean or a sequence", N); - end case; - when N_And_Bool => - if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then - Error_Msg_Sem ("left-hand side operand of logical 'and' must be" - & " a boolean", N); - end if; - when N_Or_Bool => - if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then - Error_Msg_Sem ("left-hand side operand of logical 'or' must be" - & " a boolean", N); - end if; - when N_Log_Imp_Prop => - if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then - Error_Msg_Sem ("left-hand side operand of logical '->' must be" - & " a boolean", N); - end if; - -- FIXME: <-> - when N_Until => - if not Get_Inclusive_Flag (N) then - if Get_Psl_Type (Get_Right (N)) /= Type_Boolean then - Error_Msg_Sem ("right-hand side of a non-overlapping " - & "'until*' operator must be a boolean", N); - end if; - else - if Get_Psl_Type (Get_Right (N)) /= Type_Boolean - or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean - then - Error_Msg_Sem ("both operands of an overlapping 'until*'" - & " operator are boolean", N); - end if; - end if; - when N_Before => - if Get_Psl_Type (Get_Right (N)) /= Type_Boolean - or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean - then - Error_Msg_Sem ("both operands of a 'before*'" - & " operator are boolean", N); - end if; - when others => - null; - end case; - - -- Recursion. - case Get_Kind (N) is - when N_Error => - null; - when N_Hdl_Mod_Name => - null; - when N_Vunit - | N_Vmode - | N_Vprop => - declare - Item : Node; - begin - Item := Get_Item_Chain (N); - while Item /= Null_Node loop - Check_Simple (Item); - Item := Get_Chain (Item); - end loop; - end; - when N_Name_Decl => - null; - when N_Assert_Directive - | N_Property_Declaration => - Check_Simple (Get_Property (N)); - when N_Endpoint_Declaration - | N_Sequence_Declaration => - Check_Simple (Get_Sequence (N)); - when N_Clock_Event => - Check_Simple (Get_Property (N)); - Check_Simple (Get_Boolean (N)); - when N_Always - | N_Never - | N_Eventually - | N_Strong => - Check_Simple (Get_Property (N)); - when N_Braced_SERE => - Check_Simple (Get_SERE (N)); - when N_Concat_SERE - | N_Fusion_SERE - | N_Within_SERE => - Check_Simple (Get_Left (N)); - Check_Simple (Get_Right (N)); - when N_Name => - null; - when N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Equal_Repeat_Seq => - declare - N2 : constant Node := Get_Sequence (N); - begin - if N2 /= Null_Node then - Check_Simple (N2); - end if; - end; - when N_Plus_Repeat_Seq => - Check_Simple (Get_Sequence (N)); - when N_Match_And_Seq - | N_And_Seq - | N_Or_Seq => - Check_Simple (Get_Left (N)); - Check_Simple (Get_Right (N)); - when N_Imp_Seq - | N_Overlap_Imp_Seq => - Check_Simple (Get_Sequence (N)); - Check_Simple (Get_Property (N)); - when N_Log_Imp_Prop - | N_Until - | N_Before - | N_Or_Prop - | N_And_Prop - | N_And_Bool - | N_Or_Bool - | N_Imp_Bool => - Check_Simple (Get_Left (N)); - Check_Simple (Get_Right (N)); - when N_Next - | N_Next_A - | N_Next_E => - Check_Simple (Get_Property (N)); - when N_Next_Event - | N_Next_Event_A - | N_Next_Event_E - | N_Abort => - Check_Simple (Get_Boolean (N)); - Check_Simple (Get_Property (N)); - when N_Not_Bool => - Check_Simple (Get_Boolean (N)); - when N_Const_Parameter - | N_Sequence_Parameter - | N_Boolean_Parameter - | N_Property_Parameter => - null; - when N_Actual => - null; - when N_Sequence_Instance - | N_Endpoint_Instance - | N_Property_Instance => - null; - when N_True - | N_False - | N_Number - | N_EOS - | N_HDL_Expr => - null; - end case; - end Check_Simple; -end PSL.Subsets; - diff --git a/psl/psl-subsets.ads b/psl/psl-subsets.ads deleted file mode 100644 index c3bae09ef..000000000 --- a/psl/psl-subsets.ads +++ /dev/null @@ -1,23 +0,0 @@ -with PSL.Nodes; use PSL.Nodes; - -package PSL.Subsets is - -- Check that N (a property) follows the simple subset rules from - -- PSL v1.1 4.4.4 Simple subset. - -- Ie: - -- - The operand of a negation operator is a Boolean. - -- - The operand of a 'never' operator is a Boolean or a Sequence. - -- - The operand of an 'eventually!' operator is a Boolean or a Sequence. - -- - The left-hand side operand of a logical 'and' operator is a Boolean. - -- - The left-hand side operand of a logical 'or' operator is a Boolean. - -- - The left-hand side operand of a logical implication '->' operator - -- is a Boolean. - -- - Both operands of a logical iff '<->' operator are Boolean. - -- - The right-hand side operand of a non-overlapping 'until*' operator is - -- a Boolean. - -- - Both operands of an overlapping 'until*' operator are Boolean. - -- - Both operands of a 'before*' operator are Boolean. - -- - -- All other operators not mentioned above are supported in the simple - -- subset without restriction. - procedure Check_Simple (N : Node); -end PSL.Subsets; diff --git a/psl/psl-tprint.adb b/psl/psl-tprint.adb deleted file mode 100644 index eabe8bd28..000000000 --- a/psl/psl-tprint.adb +++ /dev/null @@ -1,255 +0,0 @@ -with Types; use Types; -with PSL.Errors; use PSL.Errors; -with PSL.Prints; -with Ada.Text_IO; use Ada.Text_IO; -with Name_Table; use Name_Table; - -package body PSL.Tprint is - procedure Disp_Expr (N : Node) is - begin - case Get_Kind (N) is - when N_Number => - declare - Str : constant String := Uns32'Image (Get_Value (N)); - begin - Put (Str (2 .. Str'Last)); - end; - when others => - Error_Kind ("disp_expr", N); - end case; - end Disp_Expr; - - procedure Disp_Count (N : Node) is - B : Node; - begin - B := Get_Low_Bound (N); - if B = Null_Node then - return; - end if; - Disp_Expr (B); - B := Get_High_Bound (N); - if B = Null_Node then - return; - end if; - Put (":"); - Disp_Expr (B); - end Disp_Count; - - procedure Put_Node (Prefix : String; Name : String) is - begin - Put (Prefix); - Put ("-+ "); - Put (Name); - end Put_Node; - - procedure Put_Node_Line (Prefix : String; Name : String) is - begin - Put_Node (Prefix, Name); - New_Line; - end Put_Node_Line; - - function Down (Str : String) return String is - L : constant Natural := Str'Last; - begin - if Str (L) = '\' then - return Str (Str'First .. L - 1) & " \"; - elsif Str (L) = '/' then - return Str (Str'First .. L - 1) & "| \"; - else - raise Program_Error; - end if; - end Down; - - function Up (Str : String) return String is - L : constant Natural := Str'Last; - begin - if Str (L) = '/' then - return Str (Str'First .. L - 1) & " /"; - elsif Str (L) = '\' then - return Str (Str'First .. L - 1) & "| /"; - else - raise Program_Error; - end if; - end Up; - - procedure Disp_Repeat_Sequence (Prefix : String; Name : String; N : Node) is - S : Node; - begin - Put_Node (Prefix, Name); - Disp_Count (N); - Put_Line ("]"); - S := Get_Sequence (N); - if S /= Null_Node then - Disp_Property (Down (Prefix), S); - end if; - end Disp_Repeat_Sequence; - - procedure Disp_Binary_Sequence (Prefix : String; Name : String; N : Node) is - begin - Disp_Property (Up (Prefix), Get_Left (N)); - Put_Node_Line (Prefix, Name); - Disp_Property (Down (Prefix), Get_Right (N)); - end Disp_Binary_Sequence; - - procedure Disp_Range_Property (Prefix : String; Name : String; N : Node) is - begin - Put_Node (Prefix, Name); - Put ("["); - Disp_Count (N); - Put_Line ("]"); - Disp_Property (Down (Prefix), Get_Property (N)); - end Disp_Range_Property; - - procedure Disp_Boolean_Range_Property (Prefix : String; - Name : String; N : Node) is - begin - Disp_Property (Up (Prefix), Get_Boolean (N)); - Put_Node (Prefix, Name); - Put ("["); - Disp_Count (N); - Put_Line ("]"); - Disp_Property (Down (Prefix), Get_Property (N)); - end Disp_Boolean_Range_Property; - - procedure Disp_Property (Prefix : String; Prop : Node) is - begin - case Get_Kind (Prop) is - when N_Never => - Put_Node_Line (Prefix, "never"); - Disp_Property (Down (Prefix), Get_Property (Prop)); - when N_Always => - Put_Node_Line (Prefix, "always"); - Disp_Property (Down (Prefix), Get_Property (Prop)); - when N_Eventually => - Put_Node_Line (Prefix, "eventually!"); - Disp_Property (Down (Prefix), Get_Property (Prop)); - when N_Next => - Put_Node_Line (Prefix, "next"); --- if Get_Strong_Flag (Prop) then --- Put ('!'); --- end if; - Disp_Property (Down (Prefix), Get_Property (Prop)); - when N_Next_A => - Disp_Range_Property (Prefix, "next_a", Prop); - when N_Next_E => - Disp_Range_Property (Prefix, "next_e", Prop); - when N_Next_Event => - Disp_Property (Up (Prefix), Get_Boolean (Prop)); - Put_Node_Line (Prefix, "next_event"); - Disp_Property (Down (Prefix), Get_Property (Prop)); - when N_Next_Event_A => - Disp_Boolean_Range_Property (Prefix, "next_event_a", Prop); - when N_Next_Event_E => - Disp_Boolean_Range_Property (Prefix, "next_event_e", Prop); - when N_Braced_SERE => - Put_Node_Line (Prefix, "{} (braced_SERE)"); - Disp_Property (Down (Prefix), Get_SERE (Prop)); - when N_Concat_SERE => - Disp_Binary_Sequence (Prefix, "; (concat)", Prop); - when N_Fusion_SERE => - Disp_Binary_Sequence (Prefix, ": (fusion)", Prop); - when N_Within_SERE => - Disp_Binary_Sequence (Prefix, "within", Prop); - when N_Match_And_Seq => - Disp_Binary_Sequence (Prefix, "&& (sequence matching len)", Prop); - when N_Or_Seq => - Disp_Binary_Sequence (Prefix, "| (sequence or)", Prop); - when N_And_Seq => - Disp_Binary_Sequence (Prefix, "& (sequence and)", Prop); - when N_Imp_Seq => - Disp_Property (Up (Prefix), Get_Sequence (Prop)); - Put_Node_Line (Prefix, "|=> (sequence implication)"); - Disp_Property (Down (Prefix), Get_Property (Prop)); - when N_Overlap_Imp_Seq => - Disp_Property (Up (Prefix), Get_Sequence (Prop)); - Put_Node_Line (Prefix, "|->"); - Disp_Property (Down (Prefix), Get_Property (Prop)); - when N_Or_Prop => - Disp_Binary_Sequence (Prefix, "|| (property or)", Prop); - when N_And_Prop => - Disp_Binary_Sequence (Prefix, "&& (property and)", Prop); - when N_Log_Imp_Prop => - Disp_Binary_Sequence (Prefix, "-> (property impliciation)", Prop); - when N_Until => - Disp_Binary_Sequence (Prefix, "until", Prop); - when N_Before => - Disp_Binary_Sequence (Prefix, "before", Prop); - when N_Abort => - Disp_Property (Up (Prefix), Get_Property (Prop)); - Put_Node_Line (Prefix, "abort"); - Disp_Property (Down (Prefix), Get_Boolean (Prop)); - when N_Not_Bool => - Put_Node_Line (Prefix, "! (boolean not)"); - Disp_Property (Down (Prefix), Get_Boolean (Prop)); - when N_Or_Bool => - Disp_Binary_Sequence (Prefix, "|| (boolean or)", Prop); - when N_And_Bool => - Disp_Binary_Sequence (Prefix, "&& (boolean and)", Prop); - when N_Name_Decl => - Put_Node_Line (Prefix, - "Name_Decl: " & Image (Get_Identifier (Prop))); - when N_Name => - Put_Node_Line (Prefix, "Name: " & Image (Get_Identifier (Prop))); - Disp_Property (Down (Prefix), Get_Decl (Prop)); - when N_True => - Put_Node_Line (Prefix, "TRUE"); - when N_False => - Put_Node_Line (Prefix, "FALSE"); - when N_HDL_Expr => - Put_Node (Prefix, "HDL_Expr: "); - PSL.Prints.HDL_Expr_Printer.all (Get_HDL_Node (Prop)); - New_Line; - when N_Star_Repeat_Seq => - Disp_Repeat_Sequence (Prefix, "[*", Prop); - when N_Goto_Repeat_Seq => - Disp_Repeat_Sequence (Prefix, "[->", Prop); - when N_Equal_Repeat_Seq => - Disp_Repeat_Sequence (Prefix, "[=", Prop); - when N_Plus_Repeat_Seq => - Put_Node_Line (Prefix, "[+]"); - Disp_Property (Down (Prefix), Get_Sequence (Prop)); - when others => - Error_Kind ("disp_property", Prop); - end case; - end Disp_Property; - - procedure Disp_Assert (N : Node) is - Label : constant Name_Id := Get_Label (N); - begin - Put (" "); - if Label /= Null_Identifier then - Put (Image (Label)); - Put (": "); - end if; - Put_Line ("assert "); - Disp_Property (" \", Get_Property (N)); - end Disp_Assert; - - procedure Disp_Unit (Unit : Node) is - Item : Node; - begin - case Get_Kind (Unit) is - when N_Vunit => - Put ("vunit"); - when others => - Error_Kind ("disp_unit", Unit); - end case; - Put (' '); - Put (Image (Get_Identifier (Unit))); - Put_Line (" {"); - Item := Get_Item_Chain (Unit); - while Item /= Null_Node loop - case Get_Kind (Item) is - when N_Assert_Directive => - Disp_Assert (Item); - when N_Name_Decl => - null; - when others => - Error_Kind ("disp_unit", Item); - end case; - Item := Get_Chain (Item); - end loop; - Put_Line ("}"); - end Disp_Unit; -end PSL.Tprint; - diff --git a/psl/psl-tprint.ads b/psl/psl-tprint.ads deleted file mode 100644 index 1b06ebf1a..000000000 --- a/psl/psl-tprint.ads +++ /dev/null @@ -1,6 +0,0 @@ -with PSL.Nodes; use PSL.Nodes; - -package PSL.Tprint is - procedure Disp_Unit (Unit : Node); - procedure Disp_Property (Prefix : String; Prop : Node); -end PSL.Tprint; diff --git a/psl/psl.ads b/psl/psl.ads deleted file mode 100644 index a2f4bdce0..000000000 --- a/psl/psl.ads +++ /dev/null @@ -1,3 +0,0 @@ -package PSL is - pragma Pure (PSL); -end PSL; |