spat_1.3.0_4ad4ab14/src/core/spat-entity-tree.ads

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
------------------------------------------------------------------------------
--  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;