with Ada.Iterator_Interfaces; private with Ada.Containers.Ordered_Maps, Ada.Containers.Vectors; generic type Label_Enum is (<>); type Element is private; type Element_Array is array (Positive range <>) of Element; package Packrat.Graphs is type Node is private; type Node_Reference (Data : not null access Node) is limited null record with Implicit_Dereference => Data; type Cursor is private; type Graph is tagged private with Default_Iterator => Iterate, Iterator_Element => Node_Reference, Variable_Indexing => Node_At; No_Position : constant Cursor; Empty_Graph : constant Graph; function Leaf (New_Item : in Element_Array; Start : in Positive; Finish : in Natural) return Node with Pre => Finish + 1 >= Start, Post => Is_Leaf (Leaf'Result); function Branch (Label : in Label_Enum; Start : in Positive; Finish : in Natural) return Node with Pre => Finish + 1 >= Start, Post => Is_Branch (Branch'Result); function Is_Leaf (This : in Node) return Boolean; function Is_Branch (This : in Node) return Boolean; function Label (This : in Node) return Label_Enum with Pre => Is_Branch (This); function Elements (This : in Node) return Element_Array with Pre => Is_Leaf (This); function Start (This : in Node) return Positive; function Finish (This : in Node) return Natural; function Is_Nothing (Position : in Cursor) return Boolean; function Depth (Position : in Cursor) return Natural; function Is_Node (Position : in Cursor) return Boolean with Post => (if Is_Node'Result then not Is_Nothing (Position)); function Is_Root (Position : in Cursor) return Boolean with Post => (if Is_Root'Result then not Is_Nothing (Position) and Is_Nothing (Parent (Position)) and Depth (Position) = 0); function Is_Branch (Position : in Cursor) return Boolean with Post => (if Is_Branch'Result then not Is_Nothing (Position)); function Is_Leaf (Position : in Cursor) return Boolean with Post => (if Is_Leaf'Result then not Is_Nothing (Position)); function Label (Position : in Cursor) return Label_Enum with Pre => Is_Branch (Position); function Elements (Position : in Cursor) return Element_Array with Pre => Is_Leaf (Position); function Start (Position : in Cursor) return Positive with Pre => not Is_Nothing (Position); function Finish (Position : in Cursor) return Natural with Pre => not Is_Nothing (Position); function Choices (Position : in Cursor) return Natural; function Parent (Position : in Cursor) return Cursor; function Child_Count (Position : in Cursor; Choice : in Positive) return Natural with Pre => Choice <= Choices (Position); function Child_Count (Position : in Cursor) return Natural; function All_Child_Count (Position : in Cursor) return Natural; function First_Child (Position : in Cursor; Choice : in Positive) return Cursor with Pre => Choice <= Choices (Position), Post => Parent (First_Child'Result) = Position; function Last_Child (Position : in Cursor; Choice : in Positive) return Cursor with Pre => Choice <= Choices (Position), Post => Parent (Last_Child'Result) = Position; function First_Child (Position : in Cursor) return Cursor with Post => Parent (First_Child'Result) = Position; function Last_Child (Position : in Cursor) return Cursor with Post => Parent (Last_Child'Result) = Position; function Next_Sibling (Position : in Cursor) return Cursor with Post => Parent (Next_Sibling'Result) = Parent (Position); function Prev_Sibling (Position : in Cursor) return Cursor with Post => Parent (Prev_Sibling'Result) = Parent (Position); procedure Delete_Children (Position : in out Cursor; Choice : in Positive) with Pre => Choice <= Choices (Position), Post => Child_Count (Position, Choice) = 0; procedure Delete_Children (Position : in out Cursor) with Post => Child_Count (Position) = 0; procedure Delete_All_Children (Position : in out Cursor) with Post => All_Child_Count (Position) = 0; function Equal_Subgraph (Left, Right : in Cursor) return Boolean with Pre => Is_Node (Left) and Is_Node (Right); function Subgraph_Node_Count (Position : in Cursor) return Natural; function Find_In_Subgraph (Position : in Cursor; Item : in Element_Array) return Cursor with Post => Is_Nothing (Find_In_Subgraph'Result) or Is_Leaf (Find_In_Subgraph'Result); function Contains (Container : in Graph; Position : in Cursor) return Boolean with Post => (if Contains'Result then not Is_Nothing (Position)); function Singleton (Input : in Node) return Graph with Post => Singleton'Result.Node_Count = 1; function Node_At (Container : in Graph; Position : in Cursor) return Node_Reference with Pre => Contains (Container, Position); function Is_Empty (Container : in Graph) return Boolean with Post => (if Is_Empty'Result then Container.Node_Count = 0 else Container.Node_Count /= 0); function Is_Ambiguous (Container : in Graph) return Boolean; function Node_Count (Container : in Graph) return Natural; function Root_Count (Container : in Graph) return Natural with Post => (if Container.Is_Empty then Root_Count'Result = 0 else Root_Count'Result > 0); function Root (Container : in Graph; Index : in Positive) return Cursor with Pre => Index <= Container.Root_Count; procedure Append (Container : in out Graph; Addition : in Graph) with Pre => Container.Is_Empty or else Addition.Is_Empty or else Finish (Container.Root (Container.Root_Count)) < Start (Addition.Root (1)); procedure Prepend (Container : in out Graph; Addition : in Graph) with Pre => Container.Is_Empty or else Addition.Is_Empty or else Start (Container.Root (1)) > Finish (Addition.Root (Addition.Root_Count)); procedure Attach_Choice (Container : in out Graph; Position : in Cursor; Addition : in Graph) with Pre => Container.Contains (Position) and Is_Branch (Position) and (Addition.Is_Empty or else (Start (Position) <= Start (Addition.Root (1)) and Finish (Position) >= Finish (Addition.Root (Addition.Root_Count)))); procedure Clear (Container : in out Graph) with Post => Container.Is_Empty; procedure Delete_Position (Container : in out Graph; Position : in out Cursor) with Pre'Class => Container.Contains (Position), Post'Class => not Container.Contains (Position); function Find (Container : in Graph; Item : in Element_Array) return Cursor with Post => Is_Leaf (Find'Result) or Is_Nothing (Find'Result); package Graph_Iterators is new Ada.Iterator_Interfaces (Cursor, Is_Node); -- Note that if the given Cursor doesn't point to any position, -- then the function should assume that the choice is of what root to -- select and return that value. type Choosing_Function is access function (Container : in Graph; Position : in Cursor) return Natural; -- This function returns True if a Node pointed to by a Cursor should -- be returned, and False if it should be ignored. An example of a -- filter that will probably see a decent amount of use would be Is_Leaf. type Filter_Function is access function (Position : in Cursor) return Boolean; function Default_Choices (Container : in Graph; Position : in Cursor) return Natural; function Accept_All (Position : in Cursor) return Boolean; function Iterate (Container : in Graph; Start_At : in Cursor := No_Position; Choose : in Choosing_Function := Default_Choices'Access; Filter : in Filter_Function := Accept_All'Access) return Graph_Iterators.Reversible_Iterator'Class with Pre => Container.Contains (Start_At) or Is_Nothing (Start_At); function Iterate_All (Container : in Graph; Start_At : in Cursor := No_Position; Filter : in Filter_Function := Accept_All'Access) return Graph_Iterators.Reversible_Iterator'Class with Pre => Container.Contains (Start_At) or Is_Nothing (Start_At); private subtype Node_Index is Positive; subtype Extended_Node_Index is Natural; function Choices (My_Graph : in Graph; My_Index : in Node_Index) return Natural with Pre => My_Index <= My_Graph.Node_List.Last_Index; procedure Delete_Loose_Subgraph (Container : in out Graph; Index : in Node_Index) with Pre => Index <= Container.Node_List.Last_Index and then Container.Node_List.Element (Index).Kind /= Null_Node; procedure Delete_Up_Edge (Container : in out Graph; Current, Parent : in Node_Index) with Pre => Container.Up_Edges.Contains (Current) and then Container.Up_Edges.Reference (Current).Contains (Parent); procedure Delete_Down_Edges (Container : in out Graph; From : in Node_Index; Choice : in Positive) with Pre => Container.Choices.Contains (From) and then Container.Choices.Element (From) > 0 and then Container.Down_Edges.Contains ((From, Choice)), Post => not Container.Down_Edges.Contains ((From, Choice)); function Equal_Subgraph (Left_Graph, Right_Graph : in Graph; Left_Index, Right_Index : in Node_Index) return Boolean with Pre => Left_Index <= Left_Graph.Node_List.Last_Index and Right_Index <= Right_Graph.Node_List.Last_Index; package Index_Vectors is new Ada.Containers.Vectors (Index_Type => Positive, Element_Type => Node_Index); package Index_Maps is new Ada.Containers.Ordered_Maps (Key_Type => Node_Index, Element_Type => Node_Index); function Node_Count (Container : in Graph; Root_List : in Index_Vectors.Vector) return Natural; type Choice_Down is record From : Extended_Node_Index; Choice : Natural; end record; function "<" (Left, Right : in Choice_Down) return Boolean; package Choice_Down_Vectors is new Ada.Containers.Vectors (Index_Type => Positive, Element_Type => Choice_Down); package Choice_Maps is new Ada.Containers.Ordered_Maps (Key_Type => Node_Index, Element_Type => Natural); package Edge_Down_Maps is new Ada.Containers.Ordered_Maps (Key_Type => Choice_Down, Element_Type => Index_Vectors.Vector, "=" => Index_Vectors."="); package Edge_Up_Maps is new Ada.Containers.Ordered_Maps (Key_Type => Node_Index, Element_Type => Index_Vectors.Vector, "=" => Index_Vectors."="); type Element_Array_Access is access Element_Array; type Elem_Wrapper is new Ada.Finalization.Controlled with record Data : Element_Array_Access; end record; overriding procedure Adjust (This : in out Elem_Wrapper); overriding procedure Finalize (This : in out Elem_Wrapper); function Wrap (Data : in Element_Array) return Elem_Wrapper; Empty_Wrapper : constant Elem_Wrapper := (Ada.Finalization.Controlled with Data => null); type Node_Kind is (Null_Node, Branch_Node, Leaf_Node); type Node is record Kind : Node_Kind; Ident : Label_Enum; Content : Elem_Wrapper; Start : Positive; Finish : Natural; end record; package Node_Vectors is new Ada.Containers.Vectors (Index_Type => Node_Index, Element_Type => Node); type Cursor is record My_Graph : access Graph; Index : Extended_Node_Index; Track : Choice_Down_Vectors.Vector; end record; type Graph is tagged record Root_List : Index_Vectors.Vector; Node_List : Node_Vectors.Vector; Add_Place : Node_Index; Choices : Choice_Maps.Map; Down_Edges : Edge_Down_Maps.Map; Up_Edges : Edge_Up_Maps.Map; end record; No_Node : constant Node := (Kind => Null_Node, Ident => Label_Enum'First, Content => Empty_Wrapper, Start => 1, Finish => 0); No_Position : constant Cursor := (My_Graph => null, Index => 0, Track => Choice_Down_Vectors.Empty_Vector); Empty_Graph : constant Graph := (Root_List => Index_Vectors.Empty_Vector, Node_List => Node_Vectors.Empty_Vector, Add_Place => 1, Choices => Choice_Maps.Empty_Map, Down_Edges => Edge_Down_Maps.Empty_Map, Up_Edges => Edge_Up_Maps.Empty_Map); type Iterate_Kind is (Specific_Branch, All_Nodes); type Reversible_Iterator is new Graph_Iterators.Reversible_Iterator with record My_Graph : access Graph; Start_Pos : Cursor; Rule : Iterate_Kind; Choose_Func : Choosing_Function; Filter_Func : Filter_Function; end record; overriding function First (Object : in Reversible_Iterator) return Cursor; overriding function Next (Object : in Reversible_Iterator; Place : in Cursor) return Cursor; overriding function Last (Object : in Reversible_Iterator) return Cursor; overriding function Previous (Object : in Reversible_Iterator; Place : in Cursor) return Cursor; end Packrat.Graphs;