Fixed problems with unification

prolog_+/Interpreter.py

@@ -27,7 +27,6 @@ def default(self, line):
         except:
             print traceback.format_exc()
 
-
     def do_EOF(self, line):
         print 'EOF'
         return True

prolog_+/Search.py

@@ -10,14 +10,18 @@ def search(CE, term):
 
 def find_unify(Pred, Statement):
     return Statement.find_unify()
-
-def search_true(CE, Pred):
+    
+def determination_list(CE, Pred):
     poss = []
     for Statement in CE:
         det = Statement.determines(Pred)
         if det is not None:
             for mapping in det:
                 poss.append((Statement, mapping))
+    return poss
+
+def search_true(CE, Pred, return_mapping=False):
+    poss = determination_list(CE, Pred)
 
     for state, mapping in poss:
         if mapping == {}:
@@ -26,6 +30,8 @@ def search_true(CE, Pred):
                 nCE.remove(state)
            # print nCE, CE, state
             if state.true(nCE):
+                if return_mapping:
+                    return mapping
                 return True
 
     for state, mapping in poss:
@@ -36,6 +42,8 @@ def search_true(CE, Pred):
                 nCE.remove(state)
             #print nCE, CE, state
             if new_state.true(nCE):
+                if return_mapping:
+                    return mapping
                 return True
 
     return False
@@ -96,6 +104,21 @@ def test_search_compl_neg():
 
     assert search(CE, Pred) == True
 
+def test_search_unknown_not_true():
+    import Parser
+    source = "A(X):B(X).\n A(c):."
+    Pred = Parser._parse_pred('A(a)')
+    CE = Parser._parse(source)
+    assert search(CE, Pred) == 'Unknown'
+
+def test_search_and_unify():
+    import Parser
+    source = "A(a):B(X),C(X).\nB(c):.\nC(d):."
+    Pred = Parser._parse_pred('A(a)')
+    CE = Parser._parse(source)
+    assert search(CE, Pred) is not True
+    assert search(CE, Pred) is not False
+
 def test_search_time():
     import Parser
     source = "A(X):B(b)|C(X).\nB(b):."
@@ -138,6 +161,8 @@ def test_search_chaining_sub():
     assert search(CE, Parser._parse_pred('C(b)')) == 'Unknown'
     assert search(CE, Parser._parse_pred('!C(b)')) == 'Unknown'
 
+
+
 
 
 

prolog_+/Types.py

@@ -31,9 +31,33 @@ def unify(self, mapping):
         return new_self
 
 
-    def true(self, CE):
-        #print 'Searching for %s' % self
-        return Search.search_true(CE, self) is True
+    def true(self, CE, mapping_list):
+        assert len(mapping_list) >0
+
+        nmapping_list = []
+        for mapping in mapping_list:
+            new_self = deepcopy(self)
+            assert new_self == self
+            for i in range(len(self.args)):
+                new_self.args[i] = self.args[i].unify(mapping)
+
+            #print 'Searching for %s' % self
+            if len(Search.determination_list(CE, new_self)) == 0:
+                continue
+
+            if Search.search_true(CE, self) is True:
+                nmapping_uf = Search.search_true(CE, self, return_mapping=True)
+                nmapping = {}
+                for a,b in nmapping_uf.items():
+                    print a,b
+                    if isinstance(a, Atom):
+                        nmapping[b]=a
+                    else:
+                        nmapping[a]=b
+
+                nmapping_list.append(dict(mapping.items() + nmapping.items()))
+        print self, mapping_list, nmapping_list
+        return len(nmapping_list) > 0, nmapping_list
 
     def determines(self, other):
         if other is None:
@@ -130,8 +154,14 @@ def unify(self, mapping):
         new_self.right = self.right.unify(mapping)
         return new_self
 
-    def true(self, CE):
-        return self.left.true(CE) or self.right.true(CE)
+    def true(self, CE, mapping):
+        val, nmapping = self.left.true(CE, mapping) 
+        if val == True:
+            return True, nmapping
+
+        val, mapping = self.right.true(CE, mapping)
+
+        return val, mapping
 
     def __eq__(self, other):
         if other is None:
@@ -170,8 +200,12 @@ def unify(self, mapping):
         new_self.right = self.right.unify(mapping)
         return new_self
 
-    def true(self, CE):
-        return self.left.true(CE) and self.right.true(CE)
+    def true(self, CE, mapping):
+        val, mapping = self.left.true(CE, mapping) 
+        if val != True:
+            return False, mapping
+        val, mapping = self.right.true(CE, mapping)
+        return val, mapping
 
     def __eq__(self, other):
         if other is None:
@@ -213,9 +247,8 @@ def true(self, CE):
         if self.right == None:
             return True
 
-        if self.right.true(CE):
-            return True
-        return False
+        val, mapping = self.right.true(CE, [{}])
+        return val
 
     def __eq__(self, other):
         return self.left == other.left and self.right == other.right