Performance #10 (#15)

* All concerned entities are now derived from Entity.T.
* Less ugly template file names.
* All entities are in the same tree now
* Enable Assertion checks.
* Enabled paralled compilation ('-j0' switch).

spat.gpr

@@ -8,11 +8,15 @@ project SPAT is
    for Main use ("run_spat");
 
    package Compiler is
-      for Switches ("ada") use ("-gnatwa", "-gnatyaAbcdefhiklM128noOprsStux3", "-gnato", "-fstack-check", "-gnat12", "-g", "-O2");
+      for Switches ("ada") use ("-gnatwa", "-gnatyaAbcdefhiklM128noOprsStux3", "-gnata", "-gnato", "-fstack-check", "-gnat12", "-g", "-O2");
    end Compiler;
 
    package Linker is
       for Switches ("ada") use ("-g");
    end Linker;
 
+   package Builder is
+      for Switches ("ada") use ("-j0");
+   end Builder;
+
 end SPAT;

src/spat-entity-tree.ads

@@ -0,0 +1,54 @@
+------------------------------------------------------------------------------
+--  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 Cursor is Implementation.Trees.Cursor;
+
+   No_Element : Cursor renames Implementation.Trees.No_Element;
+
+   function Child_Count (Parent : in Cursor) return Ada.Containers.Count_Type
+                         renames Implementation.Trees.Child_Count;
+
+   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 Next_Sibling (Position : in Cursor) return Cursor
+                          renames Implementation.Trees.Next_Sibling;
+
+   procedure Next_Sibling (Position : in out Cursor)
+                           renames Implementation.Trees.Next_Sibling;
+
+private
+
+   type T is new Implementation.Trees.Tree with null record;
+
+end SPAT.Entity.Tree;

src/spat-entity_line-list.ads → src/spat-entity.ads

@@ -11,26 +11,16 @@ pragma License (Unrestricted);
 --
 --  SPARK Proof Analysis Tool
 --
---  S.P.A.T. - A list of Entity_Line objects.
+--  S.P.A.T. - Abstract object representing some kind of Entity.
 --
 ------------------------------------------------------------------------------
 
-limited with Ada.Containers.Vectors;
+package SPAT.Entity is
 
-package SPAT.Entity_Line.List is
-
-   package Implementation is
-
-      package Vectors is
-        new Ada.Containers.Vectors (Index_Type   => Positive,
-                                    Element_Type => T);
-
-   end Implementation;
-
-   type T is new Implementation.Vectors.Vector with private;
+   type T is abstract tagged private;
 
 private
 
-   type T is new Implementation.Vectors.Vector with null record;
+   type T is abstract tagged null record;
 
-end SPAT.Entity_Line.List;
+end SPAT.Entity;

src/spat-entity_line.adb

@@ -15,8 +15,9 @@ package body SPAT.Entity_Line is
    --  Create
    ---------------------------------------------------------------------------
    function Create (Object : in JSON_Value) return T is
-     (T'(File => Object.Get (Field => Field_Names.File),
-         Line => Object.Get (Field => Field_Names.Line)));
+     (T'(Entity.T with
+           File => Object.Get (Field => Field_Names.File),
+           Line => Object.Get (Field => Field_Names.Line)));
 
    ---------------------------------------------------------------------------
    --  Image

src/spat-entity_line.ads

@@ -16,6 +16,7 @@ pragma License (Unrestricted);
 --
 ------------------------------------------------------------------------------
 
+with SPAT.Entity;
 with SPAT.Field_Names;
 with SPAT.Preconditions;
 
@@ -34,7 +35,7 @@ package SPAT.Entity_Line is
                                   Field  => Field_Names.Line,
                                   Kind   => JSON_Int_Type));
 
-   type T is tagged private;
+   type T is new Entity.T with private;
 
    ---------------------------------------------------------------------------
    --  Create
@@ -63,7 +64,7 @@ package SPAT.Entity_Line is
 
 private
 
-   type T is tagged
+   type T is new Entity.T with
       record
          File : Subject_Name;
          Line : Natural;

src/spat-flow_item-list.ads

@@ -17,7 +17,7 @@ pragma License (Unrestricted);
 
 limited with Ada.Containers.Vectors;
 
-package SPAT.Flow_Item.List is
+private package SPAT.Flow_Item.List is
 
    package Implementation is
 

src/spat-flow_item.adb

@@ -8,6 +8,7 @@
 pragma License (Unrestricted);
 
 with SPAT.Field_Names;
+with SPAT.Flow_Item.List;
 
 package body SPAT.Flow_Item is
 
@@ -19,4 +20,47 @@ package body SPAT.Flow_Item is
         Rule     => Object.Get (Field => Field_Names.Rule),
         Severity => Object.Get (Field => Field_Names.Severity));
 
+   ---------------------------------------------------------------------------
+   --  Sort_By_Location
+   ---------------------------------------------------------------------------
+   procedure Sort_By_Location (This   : in out Entity.Tree.T;
+                               Parent : in     Entity.Tree.Cursor) is
+      The_List : List.T;
+      use type Entity.Tree.Cursor;
+   begin
+      if Parent = Entity.Tree.No_Element then
+         --  No elements to sort.
+         --  TODO: If we have only one item in the tree, we should probably
+         --        bail out, too, because then there's nothing to sort.
+         return;
+      end if;
+
+      --  Copy the tree's children into The_List.
+      for C in This.Iterate_Children (Parent => Parent) loop
+         The_List.Append
+           (New_Item => Flow_Item.T (Entity.Tree.Element (Position => C)));
+         --  If the children do not contain elements of Flow_Item.T then this
+         --  will raise an exception.
+      end loop;
+
+      --  Sort the list.
+      The_List.Sort_By_Location;
+
+      --  Update the elements in the Tree.
+      declare
+         Position : Entity.Tree.Cursor :=
+           Entity.Tree.First_Child (Position => Parent);
+      begin
+         for E of The_List loop
+            This.Replace_Element (Position => Position,
+                                  New_Item => E);
+            Entity.Tree.Next_Sibling (Position);
+         end loop;
+
+         --  At this point we should have no children left.
+         pragma Assert (Position = Entity.Tree.No_Element);
+      end;
+
+   end Sort_By_Location;
+
 end SPAT.Flow_Item;

src/spat-flow_item.ads

@@ -15,6 +15,7 @@ pragma License (Unrestricted);
 --
 ------------------------------------------------------------------------------
 
+with SPAT.Entity.Tree;
 with SPAT.Entity_Location;
 with SPAT.Preconditions;
 
@@ -36,6 +37,12 @@ package SPAT.Flow_Item is
    function Create (Object : in JSON_Value) return T with
      Pre => Has_Required_Fields (Object => Object);
 
+   ---------------------------------------------------------------------------
+   --  Sort_By_Location
+   ---------------------------------------------------------------------------
+   procedure Sort_By_Location (This   : in out Entity.Tree.T;
+                               Parent : in     Entity.Tree.Cursor);
+
 private
 
    type T is new Entity_Location.T with

src/spat-proof_attempt.adb

@@ -18,19 +18,20 @@ package body SPAT.Proof_Attempt is
       Time_Field : constant JSON_Value :=
                      Object.Get (Field => Field_Names.Time);
    begin
-      return T'(Prover => Prover,
-                Result => Object.Get (Field => Field_Names.Result),
-                Time   =>
-                  (case Time_Field.Kind is
-                      when JSON_Float_Type =>
-                        Duration (Time_Field.Get_Long_Float),
-                      when JSON_Int_Type   =>
-                        Duration (Long_Long_Integer'(Time_Field.Get)),
-                      when others          =>
-                         raise Program_Error
-                           with
-                             "Fatal: Impossible Kind """ &
-                             Time_Field.Kind'Image & """ of JSON object!"));
+      return T'(Entity.T with
+                  Prover => Prover,
+                  Result => Object.Get (Field => Field_Names.Result),
+                  Time   =>
+                    (case Time_Field.Kind is
+                        when JSON_Float_Type =>
+                          Duration (Time_Field.Get_Long_Float),
+                        when JSON_Int_Type   =>
+                          Duration (Long_Long_Integer'(Time_Field.Get)),
+                        when others          =>
+                           raise Program_Error
+                             with
+                               "Fatal: Impossible Kind """ &
+                               Time_Field.Kind'Image & """ of JSON object!"));
    end Create;
 
 end SPAT.Proof_Attempt;

src/spat-proof_attempt.ads

@@ -15,6 +15,7 @@ pragma License (Unrestricted);
 --
 ------------------------------------------------------------------------------
 
+with SPAT.Entity;
 with SPAT.Field_Names;
 with SPAT.Preconditions;
 
@@ -33,7 +34,7 @@ package SPAT.Proof_Attempt is
                                   Field         => Field_Names.Time,
                                   Kinds_Allowed => Preconditions.Number_Kind));
 
-   type T is tagged private;
+   type T is new Entity.T with private;
 
    ---------------------------------------------------------------------------
    --  Create
@@ -80,17 +81,18 @@ package SPAT.Proof_Attempt is
 
 private
 
-   type T is tagged
+   type T is new Entity.T with
       record
          Prover     : Subject_Name; --  Prover involved.
          Result     : Subject_Name; --  "Valid", "Unknown", etc.
          Time       : Duration;     --  time spent during proof
          --  Steps -- part of the JSON data, but we don't care.
       end record;
 
-   Trivial_True : constant T := T'(Prover => To_Name ("Trivial"),
-                                   Result => To_Name ("Valid"),
-                                   Time   => 0.0);
+   Trivial_True : constant T := T'(Entity.T with
+                                     Prover => To_Name ("Trivial"),
+                                     Result => To_Name ("Valid"),
+                                     Time   => 0.0);
 
    ---------------------------------------------------------------------------
    --  Slower_Than

src/spat-proof_item.adb

@@ -7,6 +7,8 @@
 ------------------------------------------------------------------------------
 pragma License (Unrestricted);
 
+with SPAT.Proof_Item.List;
+
 package body SPAT.Proof_Item is
 
    ---------------------------------------------------------------------------
@@ -136,4 +138,47 @@ package body SPAT.Proof_Item is
       return (for some C of This.Check_Tree => C.Is_Unproved);
    end Has_Unproved_Attempts;
 
+   ---------------------------------------------------------------------------
+   --  Sort_By_Duration
+   ---------------------------------------------------------------------------
+   procedure Sort_By_Duration (This   : in out Entity.Tree.T;
+                               Parent : in     Entity.Tree.Cursor) is
+      The_List : List.T;
+      use type Entity.Tree.Cursor;
+   begin
+      if Parent = Entity.Tree.No_Element then
+         --  No elements to sort.
+         --  TODO: If we have only one item in the tree, we should probably
+         --        bail out, too, because then there's nothing to sort.
+         return;
+      end if;
+
+      --  Copy the tree's children into The_List.
+      for C in This.Iterate_Children (Parent => Parent) loop
+         The_List.Append
+           (New_Item => Proof_Item.T (Entity.Tree.Element (Position => C)));
+         --  If the children do not contain elements of Proof_Item.T then this
+         --  will raise an exception.
+      end loop;
+
+      --  Sort the list.
+      The_List.Sort_By_Duration;
+
+      --  Update the elements in the Tree.
+      declare
+         Position : Entity.Tree.Cursor :=
+           Entity.Tree.First_Child (Position => Parent);
+      begin
+         for E of The_List loop
+            This.Replace_Element (Position => Position,
+                                  New_Item => E);
+            Entity.Tree.Next_Sibling (Position);
+         end loop;
+
+         --  At this point we should have no children left.
+         pragma Assert (Position = Entity.Tree.No_Element);
+      end;
+
+   end Sort_By_Duration;
+
 end SPAT.Proof_Item;

src/spat-proof_item.ads

@@ -17,6 +17,7 @@ pragma License (Unrestricted);
 
 limited with Ada.Containers.Vectors;
 with SPAT.Entity_Location;
+with SPAT.Entity.Tree;
 with SPAT.Field_Names;
 with SPAT.Preconditions;
 with SPAT.Proof_Attempt.List;
@@ -100,6 +101,12 @@ package SPAT.Proof_Item is
    not overriding
    function Suppressed (This : in T) return Subject_Name;
 
+   ---------------------------------------------------------------------------
+   --  Sort_By_Duration
+   ---------------------------------------------------------------------------
+   procedure Sort_By_Duration (This   : in out Entity.Tree.T;
+                               Parent : in     Entity.Tree.Cursor);
+
 private
 
    type T is new Entity_Location.T with