summaryrefslogtreecommitdiff
path: root/src/kompsos.adb
diff options
context:
space:
mode:
Diffstat (limited to 'src/kompsos.adb')
-rw-r--r--src/kompsos.adb75
1 files changed, 46 insertions, 29 deletions
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