!752

!include #1002825 // new structure

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 prologify(new Clause(head, body));
  }
  
  Clause clause(Lisp head) {
    ret prologify(new Clause(head));
  }
  
  Clause clause(Lisp head, Lisp body) {
    ret clause(head, new Goal(body));
  }
  
  Lisp prologify(Lisp term) {
    ret prologify(term, new HashMap);
  }
  
  Clause prologify(Clause c) {
    new HashMap vars;
    ret new Clause(
      prologify(c.head, vars),
      prologify(c.body, vars));
  }
  
  Goal prologify(Goal goal, Map<S, Var> vars) {
    if (goal == null) ret null;
    ret new Goal(
      prologify(goal.car, vars),
      prologify(goal.cdr, vars));
  }
  
  Lisp prologify(Lisp term, Map<S, Var> vars) {
    if (term == null) ret null;
    if (snlIsVar(term)) {
      Var v = vars.get(term.head);
      if (v == null)
        vars.put(term.head, v = newVar(term.head));
      ret v;
    } else {
      Lisp l = new Lisp(term.head);
      for (Lisp arg : term)
        l.add(prologify(arg, vars));
      ret l;
    }
  }
  
  L<Var> findVars(Lisp term) {
    new IdentityHashMap<Var, Boolean> map;
    findVars(term, map);
    ret asList(map.keySet());
  }
  
  void findVars(Lisp term, IdentityHashMap<Var, Boolean> map) {
    if (term instanceof Var)
      map.put((Var) term, Boolean.TRUE);
    else
      for (Lisp arg : term)
        findVars(arg, map);
  }
  
  static Map<S, Var> makeVarMap(L<Var> vars) {
    new HashMap<S, Var> map;
    for (Var v : vars)
      map.put(v.getName(), v);
    ret map;
  }
  
  // Executor stack entry
  static class Entry {
    Goal goal;
    Program q;
    Trail trail;
    boolean trailSet;
    
    *(Program *q, Goal *goal) {}
  }
  
  Executor executor;
  
  Executor newExecutor(Program p, Goal goal) {
    if (executor != null) fail("Already got an executor");
    ret executor = new Executor(p, goal);
  }

  // a stackless, step-based executor for Prolog queries
  // only one instance per Prolog instance!
  class Executor {
    Program p;
    new L<Entry> stack;
    
    *(Program *p, Goal goal) {
      stack.add(new Entry(p, goal));
    }
    
    int level() {
      ret l(stack)-1;
    }
    
    boolean done() {
      ret empty(stack);
    }
    
    boolean step() {
      if (done()) fail("done!"); // safety
      
      Entry e = last(stack);
      
      if (e.trailSet) {
        Trail_Undo(e.trail);
        e.trailSet = false;
      }
      
      if (e.q == null) { // program loop ends
        removeLast(stack);
        ret false;
      }
        
      if (showStuff)
        print(indent(level()) + "solve@" + level() + ": " + e.goal);
        
      // now in program loop
      
      e.trail = Trail_Note();
      e.trailSet = true;
      Clause c = e.q.pcar.copy();
      e.q = e.q.pcdr; // next clause in program
      Trail_Undo(e.trail);
      if (showStuff)
        print(indent(level()) + "  try:" + c);
      if (unify(e.goal.car, c.head)) {
        Goal gdash = c.body == null ? e.goal.cdr : c.body.append(e.goal.cdr);
        if (gdash == null)
          ret true;
        else {
          stack.add(new Entry(p, gdash));
          ret false;
        }
      } else
        if (showStuff)
          print(indent(level()) + "  nomatch.");
          
      ret false;
    }
  }
  
} // 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");
  
  // Try making a clause from pure Lisp
  
  Lisp lhs1 = lisp("app", "nil", "X", "X");
  Prolog.Clause c1 = p.clause(lhs1);
  print("c1: " + structure_seen(c1));
  
  Lisp rhs2 = lisp(at_app, "L", "M", "N");
  Lisp lhs2 = lisp(at_app, lisp(at_cons, "X", "L"),
    "M",
    lisp(at_cons, "X", "N"));
                                        
  Prolog.Clause c2 = p.clause(lhs2, rhs2);
  
  // Test prologify
  
  Lisp rhs3pre = lisp("app", "I", "J", 
    lisp("cons", "1",
    lisp("cons", "2",
    lisp("cons", "3", "nil"))));
  
  Lisp rhs3 = p.prologify(rhs3pre);
  L<Prolog.Var> vars = p.findVars(rhs3);
  print("Vars: " + structure_seen(vars));
  Map<S, Prolog.Var> varMap = Prolog.makeVarMap(vars);
  Prolog.Var v_i = varMap.get("I");
  Prolog.Var v_j = varMap.get("J");
  assertNotNull(v_i);
  assertNotNull(v_j);
  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);

  /*
  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);
  */
  
  p.showStuff = true;
  Prolog.Executor e = p.newExecutor(test_p, g1);
  int safety = 0;
  while (!e.done() && ++safety < 1000) {
    if (e.step()) {
      print("Solution at iteration " + safety + ":");
      var_name_map.showanswer();
    }
  }
  print("Steps: " + safety);
}