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