Bugfixes in Unify and Term Image, query function for World failure

4 files changed, 54 insertions, 29 deletions

diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 62f27fa..87131e1 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -68,6 +68,8 @@ package body Kompsos.Pretty_Print is
             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);
                 else
                     return Image (Item.Actual.Left) & " " & Bare (Item.Actual.Right);
                 end if;
diff --git a/src/kompsos.adb b/src/kompsos.adb
index d018c27..3981005 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -235,7 +235,10 @@ package body Kompsos is
             Item : in Term'Class)
         return Term'Class is
     begin
-        if This.Subst.Contains (Item.Actual.Refer.Ident) then
+        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));
         else
             return Item;
@@ -268,24 +271,48 @@ package body Kompsos is
             end if;
         end if;
 
-        --  Check for null Terms
+        --  Check for equal null Terms
         if Real_Left.Actual = null and Real_Right.Actual = null then
             Extended := Potential;
             return True;
         end if;
-        if Real_Left.Actual = null or Real_Right.Actual = null then
-            return False;
-        end if;
 
         --  Unify equal Variable Terms
-        if  Real_Left.Actual.Kind = Var_Term and then
-            Real_Right.Actual.Kind = Var_Term and then
+        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
             Real_Left = Real_Right
         then
             Extended := Potential;
             return True;
         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
+                not Fully_Contains (Potential, Real_Right)
+            then
+                return False;
+            end if;
+            Extended := Potential;
+            Extended.Subst.Insert (Real_Left.Actual.Refer.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
+                not Fully_Contains (Potential, Real_Left)
+            then
+                return False;
+            end if;
+            Extended := Potential;
+            Extended.Subst.Insert (Real_Right.Actual.Refer.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
@@ -311,28 +338,6 @@ package body Kompsos is
             end;
         end if;
 
-        --  Unify Variable and other Terms by introducing a new substitution
-        if Real_Left.Actual.Kind = Var_Term then
-            if  Real_Right.Actual.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));
-            return True;
-        end if;
-        if Real_Right.Actual.Kind = Var_Term then
-            if  Real_Left.Actual.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));
-            return True;
-        end if;
-
         --  Not sure how things get here, but if all else fails
         return False;
     end Do_Unify;
@@ -491,6 +496,18 @@ package body Kompsos is
     --  Public API Operations  --
     -----------------------------
 
+    --  Query  --
+
+    function Failed
+           (This : in out World)
+        return Boolean is
+    begin
+        return not This.Has_State (1);
+    end Failed;
+
+
+
+
     --  Fresh  --
 
     function Fresh
diff --git a/src/kompsos.ads b/src/kompsos.ads
index d229eb3..bed3d26 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -61,6 +61,10 @@ package Kompsos is
 
     Empty_World : constant World;
 
+    function Failed
+           (This : in out World)
+        return Boolean;
+
 
 
 
diff --git a/test/pprint.adb b/test/pprint.adb
index 6d05cba..b34f255 100644
--- a/test/pprint.adb
+++ b/test/pprint.adb
@@ -34,6 +34,7 @@ procedure PPrint is
     Term_Two   : constant Term := T (T (+"One") & T (+"Two") & T (+"Three"));
     Term_Three : constant Term := T (Term_One & Term_Two & T (+"World"));
     Term_Four  : constant Term := T (Null_Term & Null_Term);
+    Term_Five  : constant Term := T (T (+"Goodbye"), T (+"World"));
 
 begin
 
@@ -45,6 +46,7 @@ begin
     TIO.Put_Line (Image (Term_Two));
     TIO.Put_Line (Image (Term_Three));
     TIO.Put_Line (Image (Term_Four));
+    TIO.Put_Line (Image (Term_Five));
 
     TIO.New_Line;