mkanren.py

# http://mullr.github.io/micrologic/literate.html translated to python
# Variables themselves are represented as vectors that hold
# their variable index. Variable equality is determined by coincidence
# of indices in vectors.

class LVar:
    def __init__(self, uid):
        self.uid = uid

    def __hash__(self):
        return hash((LVar,self.uid))
    
    def __eq__(self, other):
        if isinstance(other, LVar):
            return self.uid == other.uid
        else:
            return False

    def __ne__(self, other):
        return not self.__eq__(other)
    
    def __repr__(self):
        return "L_" + str(self.uid)

def isLVar(x):
    return isinstance(x, LVar)

def addSubstitution(substitutionMap, lvar, value):
    if isinstance(substitutionMap,dict):
        substitutionMap[lvar]=value
        
def walk(u, smap):
    if isinstance(u,LVar):
        if u in smap:
            return walk(smap[u],smap)
        else:
            return u
    else:
        return u
        
def unify(u, v, smap):
    uw = walk(u,smap)
    vw = walk(u,smap)
    # Terms that walk to equal values always unify, but add nothing
    # to the substitution map
    if uw == vw:
        return smap
    
    # Unifying an lvar term with some other value creates a new entry in
    # the substitution map
    if isLVar(u):
        return addSubstitution(u,v)
    if isLVar(v):
        return addSubstitution(v,u)
    
    return None