misc/prolog4.py

def val_is_var(val):
    return type(val) is str and (val[0].isupper() or val[0] == '_')

def val_is_const(val):
    return type(val) is str and val[0].islower()

fake_var_cnt = 0
def fake_var():
    global fake_var_cnt
    var = '_' + str(fake_var_cnt)
    fake_var_cnt += 1
    return var                

def unify_not_var(left, right, lbinds, rbinds):
    if type(left) is not type(right):
        return False   
    # constants
    if val_is_const(left):
        return left == right
    # lists
    if type(left) is not list:
        return False
    if len(left) != len(right):
        return False
    for new_left, new_right in zip(left, right):
        if not unify(new_left, new_right, lbinds, rbinds):
            return False
    return True

def propgate(var, val, lbinds, rbinds):
    if var in lbinds:
        propgate(lbinds[var], val, lbinds, rbinds)
        del lbinds[var]
    if var in rbinds:
        propgate(rbinds[var], val, lbinds, rbinds)
        del rbinds[var]
    for key, value in lbinds.items():
        if value == var:
            lbinds[key] = val
    for key, value in rbinds.items():
        if value == var:
            rbinds[key] = val
    
    

def unify(left, right, lbinds, rbinds):
    if not val_is_var(left):
        if not val_is_var(right):
            return unify_not_var(left, right, lbinds, rbinds)
        if not right in rbinds:
            rbinds[right] = left
            return True
        if not val_is_var(rbinds[right]):
            return unify_not_var(left, rbinds[right], lbinds, rbinds)
        propgate(rbinds[right], left, lbinds, rbinds)
        return True
    if not left in lbinds:
        if not val_is_var(right):
            lbinds[left] = right
            return True
        if not right in rbinds:
            lbinds[left] = rbinds[right] = fake_var()
            return True
        lbinds[left] = rbinds[right]
        return True
    if not val_is_var(lbinds[left]):
        if not val_is_var(right):
            return unify_not_var(lbinds[left], right, lbinds, rbinds)
        if not right in rbinds:
            rbinds[right] = lbinds[left]
            return True
        if not val_is_var(rbinds[right]):
            return unify_not_var(lbinds[left], rbinds[right], lbinds, rbinds)
        propgate(rbinds[right], lbinds[left], lbinds, rbinds)
        return True
    if not val_is_var(right):
        propgate(lbinds[left], right, lbinds, rbinds)
        return True
    if not right in rbinds:
        rbinds[right] = lbinds[left]
        return True
    # if not val_is_var(rbinds[right]):
    #     return propagate(lbinds[left], rbinds[right], lbinds, rbinds)

    propagate(lbinds[left], rbinds[right], lbinds, rbinds)
    return True

def options(binds):
    for val in binds.values():
        if not val_is_var(val):
            return True
    return False

class Search:
    def __init__(self, base, query):
        self.query = query
        self.place = iter(base)
        self.up_binds = None
        self.scope = None

    def scope_bind(self):
        new_binds = {}
        for key, value in self.up_binds.items():
            new_binds[key] = self.scope.bind(value)
        return new_binds

    def get(self, base):
        if self.scope is not None:
            if self.scope.run(base) is True:
                return self.scope_bind()
            self.up_binds = None
            self.scope = None
            
        for fact in self.place:
            lbinds = {}
            rbinds = {}
            if unify(self.query, fact[0], lbinds, rbinds):
                if fact[1] is True:
                    return lbinds
                if fact[1] is False:
                    if options(lbinds):
                        continue
                    return False
                if fact[1] == 'unknown':
                    continue
                scope = Scope(base, fact[1], rbinds)
                if scope.run(base) is True:
                    self.up_binds = lbinds
                    self.scope = scope
                    return self.scope_bind()
        return 'unknown'

class Scope:
    def __init__(self, base, queries, binds={}):
        self.final = None
        self.queries = queries
        self.sbinds = [binds]
        self.searches = [Search(base, self.bind(queries[0]))]

    def resl_var(self, var):
        for binds in self.sbinds:
            if var in binds:
                var = binds[var]
                if not val_is_var(var):
                    return self.bind(var)
        if self.final is not None:
            if var in self.final:
                var = self.final[var]
                if not val_is_var(var):
                    return self.bind(var)
        return var

    def resl_list(self, query):
        new = []
        for val in query:
            new.append(self.bind(val))
        return new

    def bind(self, query):
        if val_is_const(query):
            return query
        if val_is_var(query):
            return self.resl_var(query)
        return self.resl_list(query)

    def latest_query(self):
        return self.bind(self.queries[len(self.searches)])

    def run(self, base):
        self.final = None
        while True:
            binds = self.searches[-1].get(base)
            if binds is False or binds == 'unknown':
                self.sbinds.pop()
                self.searches.pop()
                if len(self.searches) == 0:
                    return 'unknown'
            elif len(self.searches) == len(self.queries):
                self.final = binds
                return True
            else:
                self.sbinds.append(binds)
                self.searches.append(Search(base, self.latest_query()))
        
                
def unique_binds(val, binds):
    if val_is_var(val):
        if not val in binds:
            binds.add(val)
    elif type(val) is list:
        for sub_val in val:
            unique_binds(sub_val, binds)

def max_binds(val):
    binds = set([])
    unique_binds(val, binds)
    return len(binds)

def base_add(base, fact):
    fact_left = fact[0]
    left_max = max_binds(fact_left)
    for i in range(len(base)):
        lbinds = {}
        rbinds = {}
        if unify(fact_left, base[i][0], lbinds, rbinds):
            if len(lbinds) <= len(rbinds):
                base.insert(i, fact)
                return
        else:
            right_max = max_binds(base[i][0])
            if left_max <= right_max:
                base.insert(i, fact)
                return
    base.append(fact)
            
base = []
    
base_add(base, [['human', 'Y'],       [['woman', 'Y']] ])
base_add(base, [['cat', 'socrates'],  True])
base_add(base, [['man', 'socrates'],  False             ])
base_add(base, [['human', 'X'],       [['man', 'X']]   ])
base_add(base, [['likes', 'socrates', 'X'], False])
base_add(base, [['woman', 'ophelia'], True               ])
base_add(base, [['mortal', 'Z'],      [['human', 'Z']] ])
base_add(base, [['query', 'X'], ['X']])
base_add(base, [['and', 'X', 'Y'],  ['X', 'Y']] )

# lbinds = {}
# rbinds = {}

# search = Search(base, ['X', 'socrates'])
# result = search.get(base)
# while result is not False and result != 'unknown':
#     print(result)
#     result = search.get(base)

# search = Search(base, ['likes', 'socrates', 'X'])
# print(search.get(base))

search = Search(base, ['and', ['cat', 'socrates'], ['man', 'socrates']])
print(search.get(base))