Dmiles/Mycroft prolog interpreter written in Python

original_0.py

# The simple Prolog interpreter written in Python.
# Dmiles made the trail non static.
# Alan Mycroft made the original: https://www.cl.cam.ac.uk/~am21/research/funnel/prolog.c
import sys

def main(): # A sample test program: append
    at_app = Atom("append_3");
    f_nil = TermCons(NIL)
    v_x = TermVar()
    lhs1 = TermCons(at_app, f_nil, v_x, v_x)
    c1 = Clause(lhs1, None)
    v_l = TermVar()
    v_m = TermVar()
    v_n = TermVar()
    rhs2 = TermCons(at_app, v_l, v_m, v_n)
    lhs2 = TermCons(at_app, TermCons(CONSLST, v_x, v_l),
        v_m, TermCons(CONSLST, v_x, v_n))
    c2 = Clause(lhs2, Goal(rhs2, None))
    test_p = Program(c1, Program(c2, None))
    test_p2 = Program(c2, Program(c1, None))
    v_i = TermVar()
    v_j = TermVar()

    varvar = [v_i, v_j]
    varname = ["I", "J"]
    var_name_map = TermVarMapping(varvar, varname, 2)
    
    rhs3 = TermCons(at_app, v_i, v_j,
        TermCons(CONSLST, TermCons(Atom("1")),
          TermCons(CONSLST, TermCons(Atom("2")),
            TermCons(CONSLST, TermCons(Atom("3")), f_nil))))
    g1 = Goal(rhs3, None)

    sys.stdout.write("=======Append with normal clause order:\n")
    g1.solve(test_p, 0, var_name_map)
    sys.stdout.write("\n=======Append with reversed normal clause order:\n")
    g1.solve(test_p2, 0, var_name_map)

def indent(n):
    return " " * n

class Term(object):
    pass # stringify, unify, unify2, copy, reset

class Trail(object):
    def __init__(self, tcar=None, tcdr=None):
        self.tcar = tcar
        self.tcdr = tcdr
        self.sofar = None

    def note(self):
        return self.sofar

    def push(self, term):
        self.sofar = Trail(term, self.sofar)

    def undo(self, whereto):
        while self.sofar != whereto:
            self.sofar.tcar.reset()
            self.sofar = self.sofar.tcdr

class Atom(object):
    def __init__(self, name):
        self.name = name

    def stringify(self):
        return self.name

    def eqatom(self, t):
        return self.name == t.name

NIL = Atom("[]")
CONSLST = Atom(".")

class TermCons(Term):
    def __init__(self, f, *args):
        self.fsym = f
        self.args = args
        self.arity = len(args)
        
    def stringifyList(self):
        out = ["["]
        sp = ""
        for arg in self.args:
            out.append(sp)
            out.append(arg.stringify())
            sp = "|"
        out.append("]")
        return "".join(out)

    def stringify(self):
        if self.fsym == CONSLST:
            return self.stringifyList()
        out = [self.fsym.stringify()]
        if len(self.args) == 0:
            return "".join(out)
        out.append("(")
        sp = ""
        for arg in self.args:
            out.append(sp)
            out.append(arg.stringify())
            sp = ","
        out.append(")")
        return "".join(out)

    def unify(self, mach, t):
        return t.unify2(mach, self)

    def copy(self, mach):
        return self.copy2(mach)

    def copy2(self, mach):
        return TermCons.mch(mach, self)

    def reset():
        pass

    @classmethod
    def mch(cls, mach, p):
        return TermCons(p.fsym, *(arg.copy(mach) for arg in p.args))

    def unify2(self, mach, t):
        if not self.fsym.eqatom(t.fsym):
            return False
        if self.arity != t.arity:
            return False
        for i in range(self.arity):
            if not self.args[i].unify(mach, t.args[i]):
                return False
        return True

class TermVar(Term):
    timestamp = 0
    def __init__(self):
        self.instance = self
        self.varno = TermVar.timestamp
        TermVar.timestamp += 1

    def stringify(self):
        if self.instance != self:
            return self.instance.stringify()
        return "_{}".format(self.varno)

    def unify(self, mach, t):
        if self.instance != self:
            return self.instance.unify(mach, t)
        mach.push(self)
        self.instance = t
        return True

    def copy(self, mach):
        if self.instance == self:
            mach.push(self)
            self.instance = TermVar()
        return self.instance

    def reset(self):
        self.instance = self

    def unify2(self, mach, t):
        return self.unify(mach, t)

class Goal(object):
    def __init__(self, h, t):
        self.car = h
        self.cdr = t
        self.mach = Trail()

    def copy(self, mach):
        return Goal(
            self.car.copy2(mach),
            None if self.cdr is None else self.cdr.copy(mach))

    def append(self, l):
        return Goal(self.car, None if self.cdr is None else self.cdr.append(l))

    def stringify(self):
        out = self.car.stringify()
        if self.cdr != None:
            out += "; "
            out += self.cdr.stringify()
        return out

    def solve(self, p, level, map):
        sys.stdout.write(indent(level))
        sys.stdout.write("solve@" + repr(level) + ": " + self.stringify() + "\n")
        q = p
        while q != None:
            t = self.mach.note()
            c = q.pcar.copy(self.mach)
            self.mach.undo(t)
            sys.stdout.write(indent(level))
            sys.stdout.write("  try:" + c.stringify() + "\n")
            if (self.car.unify(self.mach, c.head)):
                gdash = self.cdr if c.body == None else c.body.append(self.cdr)
                if gdash == None:
                    sys.stdout.write(map.showanswer())
                else:
                    gdash.solve(p, level+1, map)
            else:
                sys.stdout.write(indent(level))
                sys.stdout.write("  nomatch.\n")
            self.mach.undo(t)
            q = q.pcdr

class Clause(object):
    def __init__(self, h, t):
        self.head = h
        self.body = t

    def copy(self, mach):
        return Clause(self.head.copy2(mach),
            None if self.body is None else self.body.copy(mach))
    
    def stringify(self):
        out = self.head.stringify()
        out += " :- "
        if self.body is None:
            out += "true"
        else:
            out += self.body.stringify()
        return out

class Program(object):
    def __init__(self, h, t):
        self.pcar = h
        self.pcdr = t

class TermVarMapping(object):
    def __init__(self, vv, vt, vs):
        self.varvar = vv
        self.vartext = vt
        self.size = vs

    def showanswer(self):
        if self.size == 0:
            return "yes\n"
        out = []
        for i in range(self.size):
            out.append(self.vartext[i] + " = " + self.varvar[i].stringify() + "\n")
        return "".join(out)

if __name__ == "__main__":
    main()

original_1.py

# The simple Prolog interpreter written in Python.
# Dmiles made the trail non static.
# Alan Mycroft made the original: https://www.cl.cam.ac.uk/~am21/research/funnel/prolog.c
import sys

# append(NIL, X, X)       <- true
# append([X|L], M, [X|N]) <- append(L, M, N)

def main(): # A sample test program: append
    at_app = Atom("append_3")
    # The first clause: append(NIL, X, X) :- true.
    f_nil = TermCons(NIL)
    v_x = TermVar()
    lhs1 = TermCons(at_app, f_nil, v_x, v_x)
    c1 = Clause(lhs1, None)
    # The second clause: append([X|L], M, [X|N]) :- append(L, M, N).
    v_l = TermVar()
    v_m = TermVar()
    v_n = TermVar()
    rhs2 = TermCons(at_app, v_l, v_m, v_n)
    lhs2 = TermCons(at_app, TermCons(CONSLST, v_x, v_l),
        v_m, TermCons(CONSLST, v_x, v_n))
    c2 = Clause(lhs2, Goal(rhs2, None))
    test_p = Program([c1, c2])
    test_p2 = Program([c2, c1])
    # Variable table for the query.
    v_i = TermVar()
    v_j = TermVar()
    var_name_map = TermVarMapping([("I", v_i), ("J", v_j)])
    # The goal.
    rhs3 = TermCons(at_app, v_i, v_j,
        TermCons(CONSLST, TermCons(Atom("1")),
          TermCons(CONSLST, TermCons(Atom("2")),
            TermCons(CONSLST, TermCons(Atom("3")), f_nil))))
    g1 = Goal(rhs3, None)

    sys.stdout.write("=======Append with normal clause order:\n")
    g1.solve(test_p, 0, var_name_map)
    sys.stdout.write("\n=======Append with reversed normal clause order:\n")
    g1.solve(test_p2, 0, var_name_map)

# The trail is a stack associated to the goal.
# It is a mutable data structure that keeps track of the
# substitutions that have been done.
class Trail(object):
    def __init__(self):
        self.sofar = []

    def note(self):
        return len(self.sofar)

    def push(self, term):
        self.sofar.append(term)

    def undo(self, whereto):
        while len(self.sofar) != whereto:
            self.sofar.pop().reset()

class Atom(object):
    def __init__(self, name):
        self.name = name

    def stringify(self):
        return self.name

    def eqatom(self, t):
        return self.name == t.name

NIL = Atom("[]")
CONSLST = Atom(".")

class TermCons(object):
    def __init__(self, f, *args):
        assert isinstance(f, Atom)
        self.fsym = f
        self.args = args
        self.arity = len(args)
        
    def stringifyList(self):
        out = ["["]
        sp = ""
        for arg in self.args:
            out.append(sp)
            out.append(arg.stringify())
            sp = "|"
        out.append("]")
        return "".join(out)

    def stringify(self):
        if self.fsym == CONSLST:
            return self.stringifyList()
        out = [self.fsym.stringify()]
        if len(self.args) == 0:
            return "".join(out)
        out.append("(")
        sp = ""
        for arg in self.args:
            out.append(sp)
            out.append(arg.stringify())
            sp = ","
        out.append(")")
        return "".join(out)

    def copy(self, mach):
        return TermCons(self.fsym, *(arg.copy(mach) for arg in self.args))

    def reset():
        pass

    def unify(self, mach, t):
        return t.unify_tcons(mach, self)

    def unify_tcons(self, mach, t):
        if not self.fsym.eqatom(t.fsym):
            return False
        if self.arity != t.arity:
            return False
        for i in range(self.arity):
            if not self.args[i].unify(mach, t.args[i]):
                return False
        return True

class TermVar(object):
    timestamp = 0
    def __init__(self):
        self.instance = self
        self.varno = TermVar.timestamp
        TermVar.timestamp += 1

    def stringify(self):
        if self.instance != self:
            return self.instance.stringify()
        return "_{}".format(self.varno)

    # During copying, the .instance is used as a reference to the copy.
    def copy(self, mach):
        if self.instance == self:
            mach.push(self)
            self.instance = TermVar()
        return self.instance

    def reset(self):
        self.instance = self

    def unify(self, mach, t):
        if self.instance != self:
            return self.instance.unify(mach, t)
        mach.push(self)
        self.instance = t
        return True

    def unify_tcons(self, mach, t):
        return self.unify(mach, t)

class Goal(object):
    def __init__(self, h, t):
        assert isinstance(h, TermCons)
        assert isinstance(t, Goal) or t is None
        self.car = h
        self.cdr = t
        self.mach = Trail()

    def copy(self, mach):
        return Goal(
            self.car.copy(mach),
            None if self.cdr is None else self.cdr.copy(mach))

    def append(self, l):
        return Goal(self.car, None if self.cdr is None else self.cdr.append(l))

    def stringify(self):
        out = self.car.stringify()
        if self.cdr != None:
            out += "; "
            out += self.cdr.stringify()
        return out

    def solve(self, p, level, map):
        sys.stdout.write(" "*level)
        sys.stdout.write("solve@" + repr(level) + ": " + self.stringify() + "\n")
        for k in range(len(p.clauses)):
            # Instantiating the clause.
            t = self.mach.note()
            c = p.clauses[k].copy(self.mach)
            self.mach.undo(t)
            # When instantiated, trying to unify the current goal with c.head.
            sys.stdout.write(" "*level)
            sys.stdout.write("  try:" + c.stringify() + "\n")
            if (self.car.unify(self.mach, c.head)):
                # If unification is successful, the remaining goal is appended
                # to the new goal. The solving starts again.
                gdash = self.cdr if c.body == None else c.body.append(self.cdr)
                if gdash == None:
                    sys.stdout.write(map.showanswer())
                else:
                    # This implementation is using the return stack
                    # to keep track of the backtracking options.
                    gdash.solve(p, level+1, map)
            else:
                sys.stdout.write(" "*level)
                sys.stdout.write("  nomatch.\n")
            self.mach.undo(t)

class Clause(object):
    def __init__(self, h, t):
        assert isinstance(h, TermCons)
        assert isinstance(t, Goal) or t is None
        self.head = h
        self.body = t

    def copy(self, mach):
        return Clause(self.head.copy(mach),
            None if self.body is None else self.body.copy(mach))
    
    def stringify(self):
        out = self.head.stringify()
        out += " :- "
        if self.body is None:
            out += "true"
        else:
            out += self.body.stringify()
        return out

class Program(object):
    def __init__(self, clauses):
        self.clauses = clauses

class TermVarMapping(object):
    def __init__(self, table):
        self.table = table

    def showanswer(self):
        if len(self.table) == 0:
            return "yes\n"
        out = []
        for text, var in self.table:
            out.append("{} = {}\n".format(text, var.stringify()))
        return "".join(out)

if __name__ == "__main__":
    main()