Refactor of Terms that causes GNAT to STORAGE_ERROR

4 files changed, 132 insertions, 165 deletions

diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 7ecbb75..8739af8 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -62,25 +62,25 @@ package body Kompsos.Pretty_Print is
                (Item : in Term)
             return String is
         begin
-            case Item.Actual.Kind is
+            case Item.Kind is
+            when Null_Term =>
+                return "()";
             when Atom_Term =>
-                return Element_Image (Item.Actual.Value);
+                return Element_Image (Item.Atom);
             when Var_Term =>
-                return Image (Item.Actual.Refer);
+                return Image (Item.Var);
             when Pair_Term =>
-                if Item.Actual.Right.Actual = null then
-                    return Image (Item.Actual.Left);
-                elsif Item.Actual.Right.Actual.Kind /= Pair_Term then
-                    return Image (Item.Actual.Left) & " . " & Bare (Item.Actual.Right);
+                if Item.Right.Kind = Null_Term then
+                    return Image (Item.Left);
+                elsif Item.Right.Kind /= Pair_Term then
+                    return Image (Item.Left) & " . " & Bare (Item.Right);
                 else
-                    return Image (Item.Actual.Left) & " " & Bare (Item.Actual.Right);
+                    return Image (Item.Left) & " " & Bare (Item.Right);
                 end if;
             end case;
         end Bare;
     begin
-        if Item.Actual = null then
-            return "()";
-        elsif Item.Actual.Kind = Pair_Term then
+        if Item.Kind = Pair_Term then
             return "(" & Bare (Item) & ")";
         else
             return Bare (Item);
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
index ed9509a..bf0b9d7 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -14,6 +14,11 @@ package Kompsos.Pretty_Print is
 
 
     function Image
+           (Item : in Variable)
+        return String;
+
+
+    function Image
            (Item : in Term)
         return String;
 
@@ -37,11 +42,6 @@ private
 
 
     function Image
-           (Item : in Variable)
-        return String;
-
-
-    function Image
            (Item : in State)
         return String;
 
diff --git a/src/kompsos.adb b/src/kompsos.adb
index c1d63da..22f0eb9 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -18,43 +18,6 @@ package body Kompsos is
     --  Memory Management  --
     -------------------------
 
-    --  Terms  --
-
-    procedure Free is new Ada.Unchecked_Deallocation (Term_Component, Term_Component_Access);
-
-
-    procedure Initialize
-           (This : in out Term) is
-    begin
-        --  For some reason, under some circumstances this is needed to ensure
-        --  the access value is actually null. Not sure why.
-        --  Seems to occur when constructing arrays with the & operator?
-        This.Actual := null;
-    end Initialize;
-
-
-    procedure Adjust
-           (This : in out Term) is
-    begin
-        if This.Actual /= null then
-            This.Actual.Count := This.Actual.Count + 1;
-        end if;
-    end Adjust;
-
-
-    procedure Finalize
-           (This : in out Term) is
-    begin
-        if This.Actual /= null then
-            This.Actual.Count := This.Actual.Count - 1;
-            if This.Actual.Count = 0 then
-                Free (This.Actual);
-            end if;
-        end if;
-    end Finalize;
-
-
-
     --  World_Holders  --
 
     procedure Free is new Ada.Unchecked_Deallocation (World'Class, World_Access);
@@ -107,40 +70,21 @@ package body Kompsos is
 
     --  Terms  --
 
-    function "="
-           (Left, Right : in Term)
-        return Boolean is
+    function Kind
+           (This : in Term)
+        return Term_Kind is
     begin
-        if Left.Actual = null and Right.Actual = null then
-            return True;
-        end if;
-        if Left.Actual = null or Right.Actual = null then
-            return False;
-        end if;
-        if Left.Actual.Kind /= Right.Actual.Kind then
-            return False;
-        end if;
-        case Left.Actual.Kind is
-        when Atom_Term =>
-            return Left.Actual.Value = Right.Actual.Value;
-        when Var_Term =>
-            return Left.Actual.Refer = Right.Actual.Refer;
-        when Pair_Term =>
-            return Left.Actual.Left = Right.Actual.Left and Left.Actual.Right = Right.Actual.Right;
-        end case;
-    end "=";
+        return Term_Component (This.Actual.Constant_Reference.Element.all).Kind;
+    end Kind;
 
 
     function T
            (Item : in Element_Type)
         return Term is
     begin
-        return My_Term : Term do
-            My_Term.Actual := new Term_Component'(
-                Kind  => Atom_Term,
-                Count => 1,
-                Value => Item);
-        end return;
+        return (Actual => Term_Holders.To_Holder (Term_Component'(
+            Kind  => Atom_Term,
+            Value => Item)));
     end T;
 
 
@@ -148,12 +92,9 @@ package body Kompsos is
            (Item : in Variable)
         return Term is
     begin
-        return My_Term : Term do
-            My_Term.Actual := new Term_Component'(
-                Kind  => Var_Term,
-                Count => 1,
-                Refer => Item);
-        end return;
+        return (Actual => Term_Holders.To_Holder (Term_Component'(
+            Kind  => Var_Term,
+            Refer => Item)));
     end T;
 
 
@@ -161,13 +102,10 @@ package body Kompsos is
            (Item1, Item2 : in Term'Class)
         return Term is
     begin
-        return My_Term : Term do
-            My_Term.Actual := new Term_Component'(
-                Kind  => Pair_Term,
-                Count => 1,
-                Left  => Term (Item1),
-                Right => Term (Item2));
-        end return;
+        return (Actual => Term_Holders.To_Holder (Term_Component'(
+            Kind  => Pair_Term,
+            Left  => Term (Item1),
+            Right => Term (Item2))));
     end T;
 
 
@@ -176,18 +114,45 @@ package body Kompsos is
         return Term is
     begin
         if Items'Length = 0 then
-            return My_Term : Term;
+            return Empty_Term;
+        else
+            return T (Items (Items'First), T (Items (Items'First + 1 .. Items'Last)));
         end if;
-        return My_Term : Term do
-            My_Term.Actual := new Term_Component'(
-                Kind  => Pair_Term,
-                Count => 1,
-                Left  => Items (Items'First),
-                Right => T (Items (Items'First + 1 .. Items'Last)));
-        end return;
     end T;
 
 
+    function Atom
+           (This : in Term)
+        return Element_Type is
+    begin
+        return Term_Component (This.Actual.Constant_Reference.Element.all).Value;
+    end Atom;
+
+
+    function Var
+           (This : in Term)
+        return Variable is
+    begin
+        return Term_Component (This.Actual.Constant_Reference.Element.all).Refer;
+    end Var;
+
+
+    function Left
+           (This : in Term)
+        return Term is
+    begin
+        return Term_Component (This.Actual.Constant_Reference.Element.all).Left;
+    end Left;
+
+
+    function Right
+           (This : in Term)
+        return Term is
+    begin
+        return Term_Component (This.Actual.Constant_Reference.Element.all).Right;
+    end Right;
+
+
 
 
     ------------------------
@@ -213,17 +178,13 @@ package body Kompsos is
             Item : in Term'Class)
         return Boolean is
     begin
-        if Item.Actual = null then
-            return True;
-        end if;
-        case Item.Actual.Kind is
-        when Atom_Term =>
+        case Item.Kind is
+        when Null_Term | Atom_Term =>
             return True;
         when Var_Term =>
-            return Has_Var (This, Item.Actual.Refer);
+            return Has_Var (This, Item.Var);
         when Pair_Term =>
-            return Fully_Contains (This, Item.Actual.Left) and then
-                Fully_Contains (This, Item.Actual.Right);
+            return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right);
         end case;
     end Fully_Contains;
 
@@ -233,11 +194,8 @@ package body Kompsos is
             Item : in Term'Class)
         return Term'Class is
     begin
-        if  Item.Actual /= null and then
-            Item.Actual.Kind = Var_Term and then
-            This.Subst.Contains (Item.Actual.Refer.Ident)
-        then
-            return Walk (This, This.Subst.Constant_Reference (Item.Actual.Refer.Ident));
+        if Item.Kind = Var_Term and then This.Subst.Contains (Item.Var.Ident) then
+            return Walk (This, This.Subst.Constant_Reference (Item.Var.Ident));
         else
             return Item;
         end if;
@@ -254,30 +212,30 @@ package body Kompsos is
         Real_Right : Term'Class := Right;
     begin
         --  Resolve Variable substitution
-        if Left.Actual /= null and then Left.Actual.Kind = Var_Term then
-            if Has_Var (Potential, Left.Actual.Refer) then
+        if Left.Kind = Var_Term then
+            if Has_Var (Potential, Left.Var) then
                 Real_Left := Walk (Potential, Left);
             else
                 return False;
             end if;
         end if;
-        if Right.Actual /= null and then Right.Actual.Kind = Var_Term then
-            if Has_Var (Potential, Right.Actual.Refer) then
+        if Right.Kind = Var_Term then
+            if Has_Var (Potential, Right.Var) then
                 Real_Right := Walk (Potential, Right);
             else
                 return False;
             end if;
         end if;
 
-        --  Check for equal null Terms
-        if Real_Left.Actual = null and Real_Right.Actual = null then
+        --  Check for equal Null Terms
+        if Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term then
             Extended := Potential;
             return True;
         end if;
 
         --  Unify equal Variable Terms
-        if  Real_Left.Actual /= null and then Real_Left.Actual.Kind = Var_Term and then
-            Real_Right.Actual /= null and then Real_Right.Actual.Kind = Var_Term and then
+        if  Real_Left.Kind = Var_Term and then
+            Real_Right.Kind = Var_Term and then
             Real_Left = Real_Right
         then
             Extended := Potential;
@@ -285,35 +243,30 @@ package body Kompsos is
         end if;
 
         --  Unify Variable and other Terms by introducing a new substitution
-        if Real_Left.Actual /= null and then Real_Left.Actual.Kind = Var_Term then
-            if  Real_Right.Actual /= null and then Real_Right.Actual.Kind = Pair_Term and then
+        if Real_Left.Kind = Var_Term then
+            if  Real_Right.Kind = Pair_Term and then
                 not Fully_Contains (Potential, Real_Right)
             then
                 return False;
             end if;
             Extended := Potential;
-            Extended.Subst.Insert (Real_Left.Actual.Refer.Ident, Term (Real_Right));
+            Extended.Subst.Insert (Real_Left.Var.Ident, Term (Real_Right));
             return True;
         end if;
-        if Real_Right.Actual /= null and then Real_Right.Actual.Kind = Var_Term then
-            if  Real_Left.Actual /= null and then Real_Left.Actual.Kind = Pair_Term and then
+        if Real_Right.Kind = Var_Term then
+            if  Real_Left.Kind = Pair_Term and then
                 not Fully_Contains (Potential, Real_Left)
             then
                 return False;
             end if;
             Extended := Potential;
-            Extended.Subst.Insert (Real_Right.Actual.Refer.Ident, Term (Real_Left));
+            Extended.Subst.Insert (Real_Right.Var.Ident, Term (Real_Left));
             return True;
         end if;
 
-        --  Don't want any null terms beyond here
-        if Real_Left.Actual = null or Real_Right.Actual = null then
-            return False;
-        end if;
-
         --  Unify equal Atom Terms
-        if  Real_Left.Actual.Kind = Atom_Term and then
-            Real_Right.Actual.Kind = Atom_Term and then
+        if  Real_Left.Kind = Atom_Term and then
+            Real_Right.Kind = Atom_Term and then
             Real_Left = Real_Right
         then
             Extended := Potential;
@@ -321,18 +274,16 @@ package body Kompsos is
         end if;
 
         --  Unify Pair Terms by unifying each corresponding part
-        if  Real_Left.Actual.Kind = Pair_Term and then
-            Real_Right.Actual.Kind = Pair_Term and then
+        if  Real_Left.Kind = Pair_Term and then
+            Real_Right.Kind = Pair_Term and then
             Fully_Contains (Potential, Real_Left) and then
             Fully_Contains (Potential, Real_Right)
         then
             declare
                 Middle : State;
             begin
-                return
-                    Do_Unify (Potential, Real_Left.Actual.Left, Real_Right.Actual.Left, Middle)
-                    and then
-                    Do_Unify (Middle, Real_Left.Actual.Right, Real_Right.Actual.Right, Extended);
+                return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Middle) and then
+                    Do_Unify (Middle, Real_Left.Right, Real_Right.Right, Extended);
             end;
         end if;
 
@@ -927,7 +878,7 @@ package body Kompsos is
         return World is
     begin
         return Result : World := This do
-            Result.Unify (Null_Term, Nil_Term);
+            Result.Unify (Empty_Term, Nil_Term);
         end return;
     end Nil;
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index 0463f6f..37533be 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -27,14 +27,15 @@ package Kompsos is
     --  Datatypes  --
     -----------------
 
+    type Variable is private;
+
+
+    type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term);
+
     type Term is tagged private;
     type Term_Array is array (Positive range <>) of Term;
 
-    Null_Term : constant Term;
-
-    function "="
-           (Left, Right : in Term)
-        return Boolean;
+    Empty_Term : constant Term;
 
     function T
            (Item : in Element_Type)
@@ -48,7 +49,29 @@ package Kompsos is
            (Items : in Term_Array)
         return Term;
 
-    --  Might include subprograms to retrieve Term contents later?
+    function Kind
+           (This : in Term)
+        return Term_Kind;
+
+    function Atom
+           (This : in Term)
+        return Element_Type
+    with Pre => This.Kind = Atom_Term;
+
+    function Var
+           (This : in Term)
+        return Variable
+    with Pre => This.Kind = Var_Term;
+
+    function Left
+           (This : in Term)
+        return Term
+    with Pre => This.Kind = Pair_Term;
+
+    function Right
+           (This : in Term)
+        return Term
+    with Pre => This.Kind = Pair_Term;
 
 
     type World is tagged private;
@@ -392,11 +415,14 @@ private
 
 
 
-    type Term_Kind is (Atom_Term, Var_Term, Pair_Term);
+    type Term_Root is abstract tagged null record;
 
-    type Term_Component (Kind : Term_Kind) is record
-        Count : Long_Integer;
+    package Term_Holders is new Ada.Containers.Indefinite_Holders (Term_Root'Class);
+
+    type Term_Component (Kind : Term_Kind) is new Term_Root with record
         case Kind is
+        when Null_Term =>
+            null;
         when Atom_Term =>
             Value : Element_Type;
         when Var_Term =>
@@ -406,22 +432,12 @@ private
         end case;
     end record;
 
-    type Term_Component_Access is access Term_Component;
-
-    type Term is new Ada.Finalization.Controlled with record
-        Actual : Term_Component_Access;
+    type Term is tagged record
+        Actual : Term_Holders.Holder := Term_Holders.To_Holder (Term_Component'(Kind => Null_Term));
     end record;
 
-    overriding procedure Initialize
-           (This : in out Term);
-
-    overriding procedure Adjust
-           (This : in out Term);
-
-    overriding procedure Finalize
-           (This : in out Term);
-
-    Null_Term : constant Term := (Ada.Finalization.Controlled with Actual => null);
+    Empty_Term : constant Term :=
+        (Actual => Term_Holders.To_Holder (Term_Component'(Kind => Null_Term)));
 
     package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array);