------------------------------------------------------------------------------
--  Copyright (C) 2020 by Heisenbug Ltd. (gh+spat@heisenbug.eu)
--
--  This work is free. You can redistribute it and/or modify it under the
--  terms of the Do What The Fuck You Want To Public License, Version 2,
--  as published by Sam Hocevar. See the LICENSE file for more details.
------------------------------------------------------------------------------
pragma License (Unrestricted);

------------------------------------------------------------------------------
--
--  SPARK Proof Analysis Tool
--
--  S.P.A.T. - A tree holding descendant objects of Entity.T.
--
------------------------------------------------------------------------------

with Ada.Containers.Indefinite_Multiway_Trees;

package SPAT.Entity.Tree is

   package Implementation is

      package Trees is new
        Ada.Containers.Indefinite_Multiway_Trees (Element_Type => T'Class);

   end Implementation;

   type T is new Implementation.Trees.Tree with private;

   subtype Forward_Iterator is
     Implementation.Trees.Tree_Iterator_Interfaces.Forward_Iterator;

   subtype Cursor is Implementation.Trees.Cursor;

   No_Element : Cursor renames Implementation.Trees.No_Element;

   function "=" (Left  : in Cursor;
                 Right : in Cursor) return Boolean
                 renames Implementation.Trees."=";

   function Child_Count (Parent : in Cursor) return Ada.Containers.Count_Type
                         renames Implementation.Trees.Child_Count;

   function Child_Depth (Parent : in Cursor;
                         Child  : in Cursor) return Ada.Containers.Count_Type
                         renames Implementation.Trees.Child_Depth;

   function Element (Position : in Cursor) return Entity.T'Class
                     renames Implementation.Trees.Element;

   function First_Child (Position : in Cursor) return Cursor
                         renames Implementation.Trees.First_Child;

   function Last_Child (Position : in Cursor) return Cursor
                        renames Implementation.Trees.Last_Child;

   function Next_Sibling (Position : in Cursor) return Cursor
                          renames Implementation.Trees.Next_Sibling;

   procedure Next_Sibling (Position : in out Cursor)
                           renames Implementation.Trees.Next_Sibling;

   function Previous_Sibling (Position : in Cursor) return Cursor
                              renames Implementation.Trees.Previous_Sibling;

   procedure Previous_Sibling (Position : in out Cursor)
                               renames Implementation.Trees.Previous_Sibling;

   function Iterate_Subtree (Position : Cursor) return Forward_Iterator'Class
                             renames Implementation.Trees.Iterate_Subtree;

   --  Sort a subtree by sorting criteria of elements contained.
   generic
      with function Before (Left  : in Entity.T'Class;
                            Right : in Entity.T'Class) return Boolean;
   package Generic_Sorting is

      procedure Sort (Tree   : in out T;
                      Parent : in     Cursor);

   end Generic_Sorting;

private

   type T is new Implementation.Trees.Tree with null record;

end SPAT.Entity.Tree;