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;

    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);

    type Choosing_Function is access function
           (Position : in Cursor)
        return Natural;




    function Iterate
           (This : in Graph)
        return Graph_Iterators.Reversible_Iterator'Class;

    function Iterate_Subtree
           (This     : in Graph;
            Position : in Cursor)
        return Graph_Iterators.Reversible_Iterator'Class;

    function Iterate_Choice
           (This : in Graph;
            Func : in Choosing_Function)
        return Graph_Iterators.Forward_Iterator'Class;




private


    subtype Node_Index is Positive;
    subtype Extended_Node_Index is Natural;

    package Index_Vectors is new Ada.Containers.Vectors
       (Index_Type   => Positive,
        Element_Type => Node_Index);




    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 Forward_Iterator is new Graph_Iterators.Forward_Iterator with record
        Position : Cursor;
    end record;

    overriding function First
           (Object : in Forward_Iterator)
        return Cursor;

    overriding function Next
           (Object : in Forward_Iterator;
            Place  : in Cursor)
        return Cursor;




    type Reversible_Iterator is new Graph_Iterators.Reversible_Iterator with record
        Position : Cursor;
    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;