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