到目前为止，这适用于我提出的所有情况（除了一个需要发生检查的情况，我还没有完成）：
def unify_var(self, var, val, subst):
# print "var> ", var, val, subst
if var in subst :
return self.unify(subst[var], val, subst)
elif isinstance(val, str) and val in subst :
return self.unify(var, subst[val], subst)
#elif (var occurs anywhere in x) then return failure
else :
#print "%s := %s" % (var, val)
subst[var] = val ; return subst
def unify(self, sym1, sym2, subst):
#print 'unify>', sym1, sym2, subst
if subst is False : return False
#when both symbols match
elif isinstance(sym1, str) and isinstance(sym2, str) and sym1 == sym2 : return subst
#variable cases
elif isinstance(sym1, str) and is_var(sym1) : return self.unify_var(sym1, sym2, subst)
elif isinstance(sym2, str) and is_var(sym2) : return self.unify_var(sym2, sym1, subst)
elif isinstance(sym1, tuple) and isinstance(sym2, tuple) : #predicate case
if len(sym1) == 0 and len(sym2) == 0 : return subst
#Functors of structures have to match
if isinstance(sym1[0], str) and isinstance(sym2[0],str) and not (is_var(sym1[0]) or is_var(sym2[0])) and sym1[0] != sym2[0] : return False
return self.unify(sym1[1:],sym2[1:], self.unify(sym1[0], sym2[0], subst))
elif isinstance(sym1, list) and isinstance(sym2, list) : #list-case
if len(sym1) == 0 and len(sym2) == 0 : return subst
return self.unify(sym1[1:],sym2[1:], self.unify(sym1[0], sym2[0], subst))
else: return False
FAIL 案例应该是失败的：
OK: a <=> a : {}
OK: X <=> a : {'X': 'a'}
OK: ['a'] <=> ['a'] : {}
OK: ['X'] <=> ['a'] : {'X': 'a'}
OK: ['a'] <=> ['X'] : {'X': 'a'}
OK: ['X'] <=> ['X'] : {}
OK: ['X'] <=> ['Z'] : {'X': 'Z'}
OK: ['p', 'a'] <=> ['p', 'a'] : {}
OK: ['p', 'X'] <=> ['p', 'a'] : {'X': 'a'}
OK: ['p', 'X'] <=> ['p', 'X'] : {}
OK: ['p', 'X'] <=> ['p', 'Z'] : {'X': 'Z'}
OK: ['X', 'X'] <=> ['p', 'X'] : {'X': 'p'}
OK: ['p', 'X', 'Y'] <=> ['p', 'Y', 'X'] : {'X': 'Y'}
OK: ['p', 'X', 'Y', 'a'] <=> ['p', 'Y', 'X', 'X'] : {'Y': 'a', 'X': 'Y'}
================= STRUCT cases ===================
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('p', 'a')] : {'X': 'Y'}
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('p', 'Z')] : {'X': 'Y', 'Z': 'a'}
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('P', 'Z')] : {'X': 'Y', 'Z': 'a', 'P': 'p'}
OK: [('p', 'a', 'X')] <=> [('p', 'Y', 'b')] : {'Y': 'a', 'X': 'b'}
OK: ['X', 'Y'] <=> [('p', 'a'), 'X'] : {'Y': ('p', 'a'), 'X': ('p', 'a')}
OK: [('p', 'a')] <=> ['X'] : {'X': ('p', 'a')}
-----
FAIL: ['e', 'X', ('p1', 'a')] <=> ['e', 'Y', ('p2', 'Z')] : False
FAIL: ['e', 'X', ('p1', 'a')] <=> ['e', 'Y', ('p1', 'b')] : False
FAIL: [('p', 'a', 'X', 'X')] <=> [('p', 'a', 'a', 'b')] : False
(should fail, occurs) OK: [('p1', 'X', 'X')] <=> [('p1', 'Y', ('p2', 'Y'))] : {'Y': ('p2', 'Y'), 'X': 'Y'}
================= LIST cases ===================
OK: ['e', 'X', ['e', 'a']] <=> ['e', 'Y', ['e', 'a']] : {'X': 'Y'}
OK: ['e', 'X', ['a', 'a']] <=> ['e', 'Y', ['a', 'Z']] : {'X': 'Y', 'Z': 'a'}
OK: ['e', 'X', ['e', 'a']] <=> ['e', 'Y', ['E', 'Z']] : {'X': 'Y', 'Z': 'a', 'E': 'e'}
OK: ['e', 'X', ['e1', 'a']] <=> ['e', 'Y', ['e1', 'a']] : {'X': 'Y'}
OK: [['e', 'a']] <=> ['X'] : {'X': ['e', 'a']}
OK: ['X'] <=> [['e', 'a']] : {'X': ['e', 'a']}
================= FAIL cases ===================
FAIL: ['a'] <=> ['b'] : False
FAIL: ['p', 'a'] <=> ['p', 'b'] : False
FAIL: ['X', 'X'] <=> ['p', 'b'] : False