Prolog.java

/* prolog.c̶java: a simple Prolog interpreter written in C++,                */
/*           including an example test run as main().                   */
/* Copyright (c) Alan Mycroft, University of Cambridge, 2000.           */
// https://www.cl.cam.ac.uk/~am21/research/funnel/prolog.c
import java.util.Objects;

public final class Prolog
{
    private Prolog()
    {
    }

    private static void indent(int n)
    {
        for (int i = 0; i < n; i++) {
            System.out.print("    ");
        }
    }

    private static class Atom
    {
        private String atomname;

        public Atom(String atomname)
        {
            this.atomname = atomname;
        }

        void print()
        {
            System.out.print(atomname);
        }

        @Override
        public boolean equals(Object o)
        {
            if (this == o) {
                return true;
            }
            if (o == null || getClass() != o.getClass()) {
                return false;
            }
            Atom atom = (Atom) o;
            return Objects.equals(atomname, atom.atomname);
        }

        @Override
        public int hashCode()
        {
            return Objects.hash(atomname);
        }
    }

    private interface Term
    {
        void print();

        boolean unify(Term term);

        boolean unify2(TermCons termCons);

        Term copy();
    }

    private static class TermCons
            implements Term
    {
        private int arity;
        private Atom fsym;
        private Term[] args;

        public TermCons(Atom f)
        {

            fsym = f;
            arity = 0;
            args = null;
        }

        public TermCons(Atom f, Term a1)
        {
            fsym = f;
            arity = 1;
            args = new Term[1];
            args[0] = a1;
        }

        public TermCons(Atom f, Term a1, Term a2)
        {
            fsym = f;
            arity = 2;
            args = new Term[2];
            args[0] = a1;
            args[1] = a2;
        }

        public TermCons(Atom f, Term a1, Term a2, Term a3)
        {
            fsym = f;
            arity = 3;
            args = new Term[3];
            args[0] = a1;
            args[1] = a2;
            args[2] = a3;
        }

        public void print()
        {
            fsym.print();
            if (arity > 0) {
                System.out.print("(");
                for (int i = 0; i < arity; ) {
                    args[i].print();
                    if (++i < arity) {
                        System.out.print(",");
                    }
                }
                System.out.print(")");
            }
        }

        public boolean unify(Term t)
        {
            return t.unify2(this);
        }

        public Term copy()
        {
            return copy2();
        }

        public TermCons copy2()
        {
            return new TermCons(this);
        }

        private TermCons(TermCons p)
        {
            fsym = p.fsym;
            arity = p.arity;
            args = p.arity == 0 ? null : new Term[p.arity];
            for (int i = 0; i < arity; i++) {
                args[i] = p.args[i].copy();
            }
        }

        public boolean unify2(TermCons t)
        {
            if (!(fsym.equals(t.fsym) && arity == t.arity)) {
                return false;
            }
            for (int i = 0; i < arity; i++) {
                if (!args[i].unify(t.args[i])) {
                    return false;
                }
            }
            return true;
        }
    }

    private static class TermVar
            implements Term
    {
        private Term instance;
        private int varno;
        static int timestamp = 0;

        public TermVar()
        {
            instance = this;
            varno = ++timestamp;
        }

        public void print()
        {
            if (instance != this) {
                instance.print();
            }
            else {
                System.out.print("_");
                System.out.print(varno);
            }
        }

        public boolean unify(Term t)
        {
            if (instance != this) {
                return instance.unify(t);
            }
            Trail.Push(this);
            instance = t;
            return true;
        }

        public Term copy()
        {
            if (instance == this) {
                Trail.Push(this);
                instance = new TermVar();
            }
            return instance;
        }

        public void reset()
        {
            instance = this;
        }

        public boolean unify2(TermCons t)
        {
            return unify(t);
        }
    }

    private static class Goal
    {
        private TermCons car;
        private Goal cdr;

        public Goal(TermCons h, Goal t)
        {
            car = h;
            cdr = t;
        }

        public Goal copy()
        {
            return new Goal(car.copy2(), cdr == null ? null : cdr.copy());
        }

        public Goal append(Goal l)
        {
            return new Goal(car, cdr == null ? null : cdr.append(l));
        }

        public void print()
        {
            car.print();
            if (cdr != null) {
                System.out.print("; ");
                cdr.print();
            }
        }

        void solve(Program p, int level, TermVarMapping map)
        {
            indent(level);
            System.out.print("solve@");
            System.out.print(level);
            System.out.print(": ");
            this.print();
            System.out.println();
            for (Program q = p; q != null; q = q.pcdr) {
                Trail t = Trail.Note();
                Clause c = q.pcar.copy();
                Trail.Undo(t);
                indent(level);
                System.out.println("  try:");
                c.print();
                System.out.println();
                if (car.unify(c.head)) {
                    Goal gdash = c.body == null ? cdr : c.body.append(cdr);
                    if (gdash == null) {
                        map.showanswer();
                    }
                    else {
                        gdash.solve(p, level + 1, map);
                    }
                }
                else {
                    indent(level);
                    System.out.println("  nomatch.");
                }
                Trail.Undo(t);
            }
        }
    }

    private static class Clause
    {
        public TermCons head;
        public Goal body;

        public Clause(TermCons h, Goal t)
        {
            head = h;
            body = t;
        }

        public Clause copy()
        {
            return new Clause(head.copy2(), body == null ? null : body.copy());
        }

        public void print()
        {
            head.print();
            System.out.print(" :- ");
            if (body == null) {
                System.out.print("true");
            }
            else {
                body.print();
            }
        }
    }

    private static class Program
    {
        public Clause pcar;
        public Program pcdr;

        public Program(Clause h, Program t)
        {
            pcar = h;
            pcdr = t;
        }
    }

    private static class Trail
    {
        private TermVar tcar;
        private Trail tcdr;
        static Trail sofar = null;

        private Trail(TermVar h, Trail t)
        {
            tcar = h;
            tcdr = t;
        }

        public static Trail Note()
        {
            return sofar;
        }

        public static void Push(TermVar x)
        {
            sofar = new Trail(x, sofar);
        }

        public static void Undo(Trail whereto)
        {
            for (; sofar != whereto; sofar = sofar.tcdr) {
                sofar.tcar.reset();
            }
        }
    }

    private static class TermVarMapping
    {
        private TermVar[] varvar;
        private String[] vartext;
        private int size;

        public TermVarMapping(TermVar[] vv, String[] vt, int vs)
        {
            varvar = vv;
            vartext = vt;
            size = vs;
        }

        public void showanswer()
        {
            if (size == 0) {
                System.out.println("yes");
            }
            else {
                for (int i = 0; i < size; i++) {
                    System.out.print(vartext[i]);
                    System.out.print(" = ");
                    varvar[i].print();
                    System.out.println();
                }
            }
        }
    }

    public static void main(String[] args)
    {
        /* A sample test program: append */

        Atom at_app = new Atom("app");
        Atom at_cons = new Atom("cons");
        TermCons f_nil = new TermCons(new Atom("nil"));
        TermCons f_1 = new TermCons(new Atom("1"));
        TermCons f_2 = new TermCons(new Atom("2"));
        TermCons f_3 = new TermCons(new Atom("3"));

        Term v_x = new TermVar();
        TermCons lhs1 = new TermCons(at_app, f_nil, v_x, v_x);
        Clause c1 = new Clause(lhs1, null);

        Term v_l = new TermVar();
        Term v_m = new TermVar();
        Term v_n = new TermVar();
        TermCons rhs2 = new TermCons(at_app, v_l, v_m, v_n);
        TermCons lhs2 = new TermCons(at_app, new TermCons(at_cons, v_x, v_l),
                v_m,
                new TermCons(at_cons, v_x, v_n));
        Clause c2 = new Clause(lhs2, new Goal(rhs2, null));

        TermVar v_i = new TermVar();
        TermVar v_j = new TermVar();
        TermCons rhs3 = new TermCons(at_app, v_i, v_j,
                new TermCons(at_cons, f_1,
                        new TermCons(at_cons, f_2,
                                new TermCons(at_cons, f_3, f_nil))));

        Goal g1 = new Goal(rhs3, null);

        Program test_p = new Program(c1, new Program(c2, null));
        Program test_p2 = new Program(c2, new Program(c1, null));

        TermVar varvar[] = {v_i, v_j};
        String[] varname = {"I", "J"};
        TermVarMapping var_name_map = new TermVarMapping(varvar, varname, 2);

        System.out.println("=======Append with normal clause order:");
        g1.solve(test_p, 0, var_name_map);
        System.out.println("\n=======Append with reversed normal clause order:");
        g1.solve(test_p2, 0, var_name_map);
    }
}