From b097dd18b74878528cd53014a1173d3434d1e052 Mon Sep 17 00:00:00 2001
From: Colin <ricec2@rpi.edu>
Date: Tue, 8 May 2012 11:14:56 -0400
Subject: [PATCH] Fixed problems with unification

---
 prolog_+/Interpreter.py |  1 -
 prolog_+/Search.py      | 29 ++++++++++++++++++++--
 prolog_+/Types.py       | 53 +++++++++++++++++++++++++++++++++--------
 3 files changed, 70 insertions(+), 13 deletions(-)

diff --git a/prolog_+/Interpreter.py b/prolog_+/Interpreter.py
index b12715d..b9ef40f 100644
--- a/prolog_+/Interpreter.py
+++ b/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
diff --git a/prolog_+/Search.py b/prolog_+/Search.py
index c543097..9a319fd 100644
--- a/prolog_+/Search.py
+++ b/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'
     
+
+    
     
     
     
diff --git a/prolog_+/Types.py b/prolog_+/Types.py
index 1c2c09f..b2af6c0 100644
--- a/prolog_+/Types.py
+++ b/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