Minor tidyup and some more comments

6 files changed, 67 insertions, 40 deletions

diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
index 2c52160..b8fc205 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -171,6 +171,7 @@ package body Kompsos.Collector is
             return;
         end if;
 
+        --  Delete cache
         if Book.Cache /= null then
             for Item of Book.Cache.Data loop
                 Free (Item.Data);
@@ -178,6 +179,7 @@ package body Kompsos.Collector is
             Free (Book.Cache);
         end if;
 
+        --  Delete all bookkeeping for lower nodes
         case Book.Data.Kind is
         when Unify_Node =>
             Do_Reset (Ptr.Uni_Goal.Actual, Book.Next1, Extra);
@@ -195,6 +197,7 @@ package body Kompsos.Collector is
             Do_Reset (Ptr.Rec_Goal.Actual, Book.Next1, Extra);
         end case;
 
+        --  Set aside common nodes to be deleted later
         if Ptr.Counter > 1 then
             if not Extra.Contains (Book) then
                 Extra.Append (Book);
@@ -212,7 +215,10 @@ package body Kompsos.Collector is
         Extra : Book_Node_Vectors.Vector;
     begin
         Do_Reset (Ptr, Book, Extra);
+
+        --  Handle common nodes
         for Item of Extra loop
+            --  Ensure that Book doesn't end up dangling
             if Item = Book then
                 Free (Book);
             else
@@ -226,6 +232,8 @@ package body Kompsos.Collector is
            (Kind : in Node_Kind)
         return Book_Node_Access is
     begin
+        --  This is needed because Ada does not allow declaring an object using
+        --  a discriminant that is not statically known.
         case Kind is
         when Unify_Node =>
             return new Book_Node'(Data => (Kind => Unify_Node,    others => <>), others => <>);
@@ -435,6 +443,9 @@ package body Kompsos.Collector is
                 Book.Next1 := Connect_Loose (Ptr.Rec_Goal.Actual);
             end if;
             if Ptr.Rec_Goal.Actual /= null then
+                --  Reach forwards to ensure the next node has cached results
+                --  even if it normally wouldn't have and that those results
+                --  are not discarded, so we can loop through them as needed.
                 if Book.Next1 = null then
                     Book.Next1 := New_Book (Ptr.Rec_Goal.Actual);
                     Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
@@ -476,7 +487,10 @@ package body Kompsos.Collector is
     begin
         if Ptr = null then
             return False;
-        elsif Ptr.Actual = null then
+        end if;
+
+        --  Lowest node in the graph always returns the Base State
+        if Ptr.Actual = null then
             if Index = 1 then
                 Result := Base;
                 Use_New_Node := True;
@@ -484,9 +498,14 @@ package body Kompsos.Collector is
             else
                 return False;
             end if;
-        elsif Book = null then
+        end if;
+
+        --  Attempt to connect common bookkeeping branches
+        if Book = null then
             Book := Connect_Loose (Ptr.Actual);
         end if;
+
+        --  If cached results exist, use those
         if Book /= null and then Book.Cache /= null and then
             Index <= Book.Cache.Data.Last_Index
         then
@@ -497,25 +516,27 @@ package body Kompsos.Collector is
             end if;
             Use_New_Node := True;
             return True;
-        else
-            return Found : constant Boolean :=
-                Do_Get_Next (Ptr.Actual, Book, Base, Index, Result)
-            do
-                if Found then
-                    if Ptr.Actual.Counter > 1 and then
-                        Ptr.Actual /= Relation.Graph.Actual and then
-                        Book.Cache = null
-                    then
-                        Book.Cache := new Cache_Entry'(False, State_Vectors.Empty_Vector);
-                    end if;
-                    if Book.Cache /= null then
-                        pragma Assert (Index = Book.Cache.Data.Last_Index + 1);
-                        Book.Cache.Data.Append ((1, new State'(Result)));
-                        Use_New_Node := True;
-                    end if;
-                end if;
-            end return;
         end if;
+
+        --  Otherwise, actual result calculation
+        return Found : constant Boolean :=
+            Do_Get_Next (Ptr.Actual, Book, Base, Index, Result)
+        do
+            if Found then
+                --  Cache results as needed
+                if Ptr.Actual.Counter > 1 and then
+                    Ptr.Actual /= Relation.Graph.Actual and then
+                    Book.Cache = null
+                then
+                    Book.Cache := new Cache_Entry'(False, State_Vectors.Empty_Vector);
+                end if;
+                if Book.Cache /= null then
+                    pragma Assert (Index = Book.Cache.Data.Last_Index + 1);
+                    Book.Cache.Data.Append ((1, new State'(Result)));
+                    Use_New_Node := True;
+                end if;
+            end if;
+        end return;
     end Get_Next;
 
 
diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads
index 93fd6d4..ac451c2 100644
--- a/src/kompsos-collector.ads
+++ b/src/kompsos-collector.ads
@@ -100,6 +100,10 @@ private
 
 
 
+    --  Used to keep track of and connect up bookkeeping nodes corresponding to
+    --  graph nodes with more than one parent, so as to avoid ending up with an
+    --  exponential tree instead of the desired directed acyclic graph.
+
     type Loose_Book is record
         Used : Positive               := 1;
         Ptr  : Graph_Component_Access := null;
diff --git a/src/kompsos-math.ads b/src/kompsos-math.ads
index adf48d2..d834df3 100644
--- a/src/kompsos-math.ads
+++ b/src/kompsos-math.ads
@@ -338,6 +338,8 @@ package Kompsos.Math is
 
 
     --  repeated-mul  --
+    --  Should be faster than Exponential for calculating powers.
+
     --  Inputs = Base_Term & Exponent_Term & Power_Term
     function Repeated_Multiply
            (This   : in Goal;
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
index 5f388b9..5b443f9 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -43,6 +43,8 @@ package Kompsos.Pretty_Print is
 
     --  Graphviz DAG Of Tomorrow  --
 
+    --  Currently only shows general structure, not specific Terms for a Unify
+    --  or the specific function and arguments for a Conjunct.
     function Structure_DOT
            (This : in Goal;
             Name : in String := "")
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 97e8ce6..4513706 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -384,18 +384,9 @@ package body Kompsos is
         elsif Inputs'Length = 1 then
             return Inputs (Inputs'First);
         else
-            declare
-                Rest : constant Goal := Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last));
-            begin
-                return Result : constant Goal :=
-                   (Graph    => (Ada.Finalization.Controlled with
-                        Actual => new Graph_Component'(
-                           (Kind      => Disjunct_Node,
-                            Counter   => 1,
-                            Dis_Goal1 => Inputs (Inputs'First).Graph,
-                            Dis_Goal2 => Rest.Graph))),
-                    Next_Var => Variable'Max (Inputs (Inputs'First).Next_Var, Rest.Next_Var));
-            end;
+            return Disjunct
+               (Inputs (Inputs'First),
+                Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)));
         end if;
     end Disjunct;
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index b8629fb..dc9341f 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -34,21 +34,24 @@ package Kompsos is
            (Left, Right : in Term)
         return Boolean;
 
+    function Kind
+           (This : in Term)
+        return Term_Kind;
+
     function T
            (Item : in Element_Type)
-        return Term;
+        return Term
+    with Post => T'Result.Kind = Atom_Term;
 
     function T
            (Item1, Item2 : in Term'Class)
-        return Term;
+        return Term
+    with Post => T'Result.Kind = Pair_Term;
 
     function T
            (Items : in Term_Array)
-        return Term;
-
-    function Kind
-           (This : in Term)
-        return Term_Kind;
+        return Term
+    with Post => T'Result.Kind = Pair_Term or else T'Result.Kind = Null_Term;
 
     function Atom
            (This : in Term)
@@ -405,13 +408,15 @@ package Kompsos is
 private
 
 
-    --  around 2^31 possible Variables should be enough for anybody, right?
+    --  Variables  --
+    --  Around 2^31 possible Variables per Goal should be enough for anybody, right?
     subtype Long_Natural  is Long_Integer range 0 .. Long_Integer'Last;
     subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last;
 
     type Variable is new Long_Natural;
 
 
+    --  Terms  --
 
     subtype Not_Null_Term_Kind is Term_Kind range Atom_Term .. Pair_Term;
 
@@ -458,6 +463,7 @@ private
     package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array);
 
 
+    --  States  --
 
     type Binding is record
         Key   : Variable;
@@ -508,6 +514,7 @@ private
     Empty_State : constant State := (Ctrl => (Ada.Finalization.Controlled with Actual => null));
 
 
+    --  Goals  --
 
     type Graph_Component;