!752

static class Prolog {

  int varCount;

  boolean showStuff;

  class Var extends Lisp {

    Lisp instance;

    *() {

      this("V" + (++varCount));

    }

    *(S name) {

      super(name);

      instance = this;

    }

    void reset() { instance = this; }

    public String toString() {

      if (instance == this) ret getName();

      ret instance.toString();

    }

    S getName() {

      ret head;

    }

  }

  class Clause {

    Lisp head;

    Goal body;

    *(Lisp *head, Goal *body) {}

    *(Lisp *head) {}

    Clause copy() {

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

    }

    public String toString() {

      //ret head + " :- " + (body == null ? "true" : body);

      ret body == null ? head.toString() : head + " :- " + body;

    }

  };

  static class Program {

    Clause pcar;

    Program pcdr;

    *(Clause *pcar, Program *pcdr) {}

    *(L<Clause> clauses) {

      this(clauses, 0);

    }

    *(L<Clause> clauses, int i) {

      pcar = clauses.get(i);

      if (i+1 < l(clauses))

        pcdr = new Program(clauses, i+1);

    }

    *(Clause... clauses) {

      this(asList(clauses));

    }

    public String toString() {

      ret pcdr == null ? pcar + "." : pcar + ".\n" + pcdr;

    }

  }

  class Trail {

    Var tcar;

    Trail tcdr;

    *(Var *tcar, Trail *tcdr) {}

  }

  Trail sofar = null;

  Trail Trail_Note() { return sofar; }

  void Trail_Push(Var x) { sofar = new Trail(x, sofar); }

  void Trail_Undo(Trail whereto) {

    for (; sofar != whereto; sofar = sofar.tcdr)

      sofar.tcar.reset();

  }

  static class TermVarMapping {

    new L<Var> vars;

    *(L<Var> *vars) {}

    *(Var... vars) { this.vars.addAll(asList(vars)); }

    void showanswer() {

      print("TRUE.");

      for (Var v : vars)

        print("  " + v.getName() + " = " + v);

    }

  }

  class Goal {

    Lisp car;

    Goal cdr;

    *(Lisp *car, Goal *cdr) {}

    *(Lisp *car) {}

    public String toString() {

      ret cdr == null ? car.toString() : car + "; " + cdr;

    }

    void solve(Program p, int level, TermVarMapping map) {

      if (showStuff)

        print(indent(level) + "solve@" + level + ": " + this);

      for (Program q = p; q != null; q = q.pcdr) {

        Trail t = Trail_Note();

        Clause c = q.pcar.copy();

        Trail_Undo(t);

        if (showStuff)

          print(indent(level) + "  try:" + c);

        if (unify(car, 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

          if (showStuff)

            print(indent(level) + "  nomatch.");

        Trail_Undo(t);

      }

    }

    Goal copy() {

      return new Goal(copy2(car),

        cdr == null ? null : cdr.copy());

    }

    Goal append(Goal l) {

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

    }

  } // class Goal

  boolean unify(Lisp thiz, Lisp t) {

    if (thiz instanceof Var) { // TermVar::unify

      Var v = cast thiz;

      if (v.instance != v)

        return unify(v.instance, t);

      Trail_Push(v);

      v.instance = t;

      return true;

    }

    // TermCons::unify

    return unify2(t, thiz);

  }

  boolean unify2(Lisp thiz, Lisp t) { 

    if (thiz instanceof Var)

      return unify(thiz, t);

    int arity = thiz.size();

    if (neq(thiz.head, t.head) || arity != t.size())

      return false;

    for (int i = 0; i < arity; i++)

      if (!unify(thiz.get(i), t.get(i)))

        return false;

    return true;

  }

  Lisp copy(Lisp thiz) {

    if (thiz instanceof Var) {

      Var v = cast thiz;

      if (v.instance == v) {

        Trail_Push(v);

        v.instance = new Var();

      }

      return v.instance;

    }

    ret copy2(thiz);

  }

  Lisp newTermCons(Lisp t) {

    Lisp l = new Lisp(t.head);

    for (Lisp arg : t)

      l.add(copy(arg));

    ret l;

  }

  Lisp copy2(Lisp thiz) {

    return newTermCons(thiz);

  }

  Var newVar() {

    ret new Var;

  }

  Var newVar(S name) {

    ret new Var(name);

  }

  Clause clause(Lisp head, Goal body) {

    ret new Clause(head, body);

  }

  Clause clause(Lisp head) {

    ret new Clause(head);

  }

} // class Prolog

p {

  new Prolog p;

  /* A sample test program: append */

  S at_app = "app";

  S at_cons = "cons";

  Lisp f_nil = lisp("nil");

  Lisp f_1 = lisp("1");

  Lisp f_2 = lisp("2");

  Lisp f_3 = lisp("3");

  Lisp v_x = p.newVar();

  Lisp lhs1 = lisp(at_app, f_nil, v_x, v_x);

  Prolog.Clause c1 = p.clause(lhs1);

  Lisp v_l = p.newVar();

  Lisp v_m = p.newVar();

  Lisp v_n = p.newVar();

  Lisp rhs2 = lisp(at_app, v_l, v_m, v_n);

  Lisp lhs2 = lisp(at_app, lisp(at_cons, v_x, v_l),

                                        v_m,

                                        lisp(at_cons, v_x, v_n));

  Prolog.Clause c2 = p.clause(lhs2, p.new Goal(rhs2));

  Prolog.Var v_i = p.newVar("I");

  Prolog.Var v_j = p.newVar("J");

  Lisp rhs3 = lisp(at_app, v_i, v_j, 

                        lisp(at_cons, f_1,

                        lisp(at_cons, f_2,

                        lisp(at_cons, f_3, f_nil))));

  Prolog.Goal g1 = p.new Goal(rhs3);

  Prolog.Program test_p = new Prolog.Program(c1, c2);

  Prolog.Program test_p2 = new Prolog.Program(c2, c1);

  Prolog.TermVarMapping var_name_map = new Prolog.TermVarMapping(v_i, v_j);

  p.showStuff = true;

  print("=======Append with normal clause order:");

  print(test_p);

  print();

  g1.solve(test_p, 0, var_name_map);

  print();

  /*

  print("=======Append with reversed normal clause order:");

  print(test_p2);

  print();

  g1.solve(test_p2, 0, var_name_map);

  */

}