!752

// TermCons -> Lisp

static int varCount;

static 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;

  }

}

static 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);

  }

};

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));

  }

}

static class Trail {

  Var tcar;

  Trail tcdr;

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

};

static Trail sofar = null;

static Trail Trail_Note() { return sofar; }

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

static 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);

  }

}

static 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) {

    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);

      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

        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

static boolean unify(Lisp thiz, Lisp t) {

  if (thiz instanceof Var) {

    Var v = cast thiz;

    if (v.instance != v)

      return unify(v.instance, t);

    Trail_Push(v);

    v.instance = t;

    return true;

  }

  return unify2(t, thiz);

}

static 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;

}

static 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);

}

static Lisp newTermCons(Lisp t) {

  Lisp l = new Lisp(t.head);

  for (Lisp arg : t)

    l.add(copy(arg));

  ret l;

}

static Lisp copy2(Lisp thiz) {

  return newTermCons(thiz);

}

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 = new Var;

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

  Clause c1 = new Clause(lhs1);

  Lisp v_l = new Var();

  Lisp v_m = new Var();

  Lisp v_n = new Var();

  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));

  Clause c2 = new Clause(lhs2, new Goal(rhs2));

  Var v_i = new Var();

  Var v_j = new Var();

  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))));

  Goal g1 = new Goal(rhs3);

  Program test_p = new Program(c1, c2);

  Program test_p2 = new Program(c2, c1);

  TermVarMapping var_name_map = new TermVarMapping(v_i, v_j);

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

  g1.solve(test_p, 0, var_name_map);

  print();

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

  g1.solve(test_p2, 0, var_name_map);

}