// do NOT initialize in static field
static final class Prolog {
  boolean upperCaseVariables = false; // true for SNL, false for NL
  long varCount;
  boolean showStuff;
  new L<Entry> stack;
  Trail sofar = null;
  new L<Clause> program;
  new L<L<Clause>> programByArity;
  long steps;
  L<S> log;
  int maxLogSize = 1000; // lines
  int maxLevel = 10000; // max stack size
  int timeLimit = 20; // 20 seconds
  long startTime;
  boolean allowEval = true;
  int defaultRewriteMax = 100;
  
  // name of theory to memorize stuff to
  S outTheory;
  
  // stats
  int maxLevelSeen; // maximum stack level reached during computation
  long topUnifications, exceptions;

  static interface INative {
    public boolean yo(Prolog p, Lisp term);
  }

  // CENTRAL method for comparing terms
  // change for modifying case-sensitivity.
  boolean headeq(S a, S b) {
    ret isQuoted (a) ? eq(a, b) : eqic(a, b);
  }
  
  static class Var extends Lisp {
    long id;
    Lisp instance;
    
    *(S name) {
      super(name);
      instance = this;
    }
    
    *(long id) {
      super("___");
      this.id = id;
      instance = this;
    }
    
    void reset() { instance = this; }
    
    public String toString() {
      if (instance != this)
        ret instance.toString();
      ret prettyName();
    }
    
    S prettyName() {
      ret isUserVar() ? getName() : "_" + id;
    }
    
    boolean isUserVar() {
      ret id == 0;
    }
    
    S getName() {
      ret head;
    }
    
    Lisp getValue() {
      Lisp l = instance;
      while (l instanceof Var) {
        Var v = cast l;
        if (v.instance == v)
          ret v;
        l = v.instance;
      }
      ret l;
    }
  }
  
  static class LCollector extends Lisp {
    new L<Lisp> solutions;
    
    *() { super("___"); }
    
    public S toString() {
      ret "<collector>";
    }
  }
  
  static class Clause {
    Lisp head;
    S loadedFrom; // theory name
    boolean used;
    
    // Either body or nat will be set (or none)
    INative nat;
    Goal body;
    
    *(Lisp *head, INative *nat) {}
    *(Lisp *head, Goal *body) {}
    *(Lisp *head, Goal *body, INative *nat) {}
    *(Lisp *head) {}
    
    Clause copy(Prolog p) {
      ret new Clause(p.copy(head), body == null ? null : body.copy(p), nat);
    }
    
    public String toString() {
      //ret head + " :- " + (body == null ? "true" : body);
      ret nat != null ? head + " :- native" :
        (body == null ? head.toString() : head + " :- " + body);
    }
    
    // fails if clause is a rule
    Lisp getStatement() {
      if (nat != null || body != null) fail("Not a statement: " + this);
      ret head;
    }
  }
  
  class Trail {
    Var tcar;
    Trail tcdr;
    
    *(Var *tcar, Trail *tcdr) {}
  }
  
  Trail Trail_Note() { return sofar; }
  void Trail_Set(Var x, Lisp value) {
    sofar = new Trail(x, sofar);
    x.instance = value;
    /*if (showStuff)
      log(indent(level()) + "  Push " + x.prettyName() + " (" + x + ")");*/
  }
  void Trail_Undo(Trail whereto) {
    for (; sofar != whereto; sofar = sofar.tcdr) {
      /*if (showStuff)
        log(indent(level()) + "  Resetting variable " + sofar.tcar.prettyName() + " (" + sofar.tcar + ")");*/
      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.prettyName() + " = " + v);
    }
  }
      
  static class Goal {
    Lisp car;
    Goal cdr;
    
    *(Lisp *car, Goal *cdr) {}
    *(Lisp *car) {}
    
    public String toString() {
      ret cdr == null ? car.toString() : car + "; " + cdr;
    }
    
    Goal copy(Prolog p) {
      return new Goal(p.copy(car),
        cdr == null ? null : cdr.copy(p));
    }
    
    Goal append(Goal l) {
      return new Goal(car, cdr == null ? l : cdr.append(l));
    }
    
  } // class Goal
  
  boolean unifyOrRollback(Lisp a, Lisp b) {
    Trail t = Trail_Note();
    if (unify(a, b)) ret true;
    Trail_Undo(t);
    ret false;
  }
  
  boolean unify(Lisp thiz, Lisp t) {
    if (thiz == null) fail("thiz=null");
    if (t == null) fail("t=null");
    
    if (thiz instanceof Var) { // TermVar::unify
      Var v = cast thiz;
      if (v.instance != v)
        return unify(v.instance, t);
      Trail_Set(v, 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 (!headeq(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_Set(v, newVar());
      }
      return v.instance;
    }
    
    // copy2 (copy non-var)
    Lisp l = new Lisp(thiz.head);
    for (Lisp arg : thiz)
      l.add(copy(arg));
    ret l;
  }
  
  Var newVar() {
    ret new Var(++varCount);
  }
  
  Var newVar(S name) {
    ret new Var(name);
  }
  
  Clause clause(Lisp head, Goal body) {
    ret prologify(new Clause(head, body));
  }
  
  // primary processor for freshly parsed rules
  
  Clause clause(Lisp rule) {
    L<Lisp> ops = snlSplitOps(rule);
    /*if (showStuff)
      log("clause(Lisp): " + rule + " => " + structure(ops)); */
      
    // expand rule shortcuts (say/memorize/...)
    
    for (int i = 0; i < l(ops)-1; i++)
      if (ops.get(i).is("memorize *"))
        ops.set(i, lisp("and *", lisp("[]", "memorize", ops.get(i))));
    
    if (!empty(ops) && last(ops).is("say *"))
      ops.set(l(ops)-1, lisp("then *", lisp("[]", "say", last(ops).get(0))));
      
    rule = empty(ops) ? rule : snlJoinOps(ops);

    if (allowEval)
      rule = new EvalTransform().evalTransformRule(rule);
      
    ops = snlSplitOps(rule);
    if (!empty(ops) && last(ops).is("then *")) {
      Lisp head = last(ops).get(0);
      Goal goal = null;
      
      // TODO: check the actual words (if/and/...)
      for (int i = l(ops)-2; i >= 0; i--)
        goal = new Goal(ops.get(i).get(0), goal);
        
      ret clause(head, goal);
    } else
      ret clause(rule, (Lisp) null);
  }
  
  Clause clause(Lisp head, Lisp body) {
    ret clause(head, body == null ? null : new Goal(body));
  }
  
  Lisp prologify(Lisp term) {
    ret prologify(term, new HashMap);
  }
  
  Clause prologify(Clause c) {
    new HashMap vars;
    c = new Clause(
      prologify(c.head, vars),
      prologify(c.body, vars),
      c.nat);
    /*if (showStuff)
      log("Clause made: " + structure_seen(c));*/
    ret c;
  }
  
  Goal prologify(Goal goal, Map<S, Var> vars) {
    if (goal == null) ret null;
    ret new Goal(
      prologify(goal.car, vars),
      prologify(goal.cdr, vars));
  }
  
  // Note: only for un-prologified
  boolean isVar(Lisp term) {
    ret upperCaseVariables ? snlIsVar(term) : nlIsVar(term);
  }
  
  // for prologified (e.g. in native clauses)
  boolean isLiveVar(Lisp term) {
    ret term instanceof Var;
  }
  
  Lisp prologify(Lisp term, Map<S, Var> vars) {
    if (term == null) ret null;
    if (isVar(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(Goal g) {
    new IdentityHashMap<Var, Boolean> map;
    while (g != null) {
      findVars(g.car, map);
      g = g.cdr;
    }
    ret asList(map.keySet());
  }
  
  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;
  }
  
  new L<Clause> emptyProgram;
  
  // Executor stack entry
  class Entry {
    Goal goal;
    L<Clause> program; // full program or filtered by arity
    int programIdx = 0;
    Trail trail;
    boolean trailSet;

    *(Goal *goal) {
      Lisp car = resolve1(goal.car);
      if (car instanceof Var) {
        if (showStuff)
          log("Weird: Goal is variable: " + car);
        program = Prolog.this.program;
      } else {
        int arity = car.size();
        program = arity >= l(programByArity) ? emptyProgram : programByArity.get(arity);
        if (showStuff)
          log(indent(level()) + "Goal arity " + arity + ": " + render(car) + ", have " + n2(program, "fact") + " of this arity");
      }
    }
  }
  
  void start(S goal) {
    start(nlParse(goal));
  }
  
  void start(Lisp goal) {
    start(new Goal(prologify(goal)));
  }
  
  S render(Lisp term) {
    ret nlUnparse(resolve(term));
  }
  
  S render(Goal goal) {
    ret goal == null ? "-" : render(goal.car);
  }
  
  S render(Clause c) {
    ret c == null ? "-" : render(c.head);
  }
  
  // warning: doesn't prologify the goal
  void start(Goal goal) {
    if (showStuff)
      log("Starting on goal: " + render(goal));
    steps = 0;
    stack = new L;
    Trail_Undo(null);
    stackAdd(new Entry(goal));
    startTime = sysNow();
  }
  
  void log(S s) {
    if (log != null) {
      if (l(log) == maxLogSize) {
        log.add("[Log overflow]");
        showStuff = false;
      }
      else if (l(log) < maxLogSize)
        log.add(s);
    } else if (showStuff)
      print("prolog: " + s);
  }
    
  int level() {
    ret l(stack)-1;
  }
  
  boolean done() {
    boolean result = empty(stack);
    /*if (showStuff && result)
      log("Done with goal!");*/
    ret result;
  }

  boolean gnext(Goal g) {  
    Goal gdash = g.cdr;
    if (gdash == null) {
      if (showStuff)
        log("gnext true");
      ret true;
    } else {
      stackAdd(new Entry(gdash));
      ret false;
    }
  }
  
  void stackPop() {
    Entry e = popLast(stack);
    if (e.trailSet)
      Trail_Undo(e.trail);
  }
  
  void backToCutPoint(int n) {
    if (showStuff)
      log("back to cut point " + n);
    while (l(stack) >= n) {
      if (showStuff)
        log("cut: dropping " + structure(last(stack).goal));
      stackPop();
    }
  }

  boolean step() {
    ping();
    if (done()) fail("done!"); // safety
    if (sysNow() >= startTime+timeLimit*1000)
      fail("time limit reached: " + timeLimit + " s");
    
    ++steps;
    Entry e = last(stack);
    
    if (e.trailSet) {
      Trail_Undo(e.trail);
      e.trailSet = false;
    }
    
    e.trail = Trail_Note();
    e.trailSet = true;
    
    // cut operator - suceeds first time
    if (e.goal.car.is("!", 1)) {
      if (showStuff)
        log("cut " + e.programIdx + ". " + structure(e.goal));
      if (e.programIdx == -1) {
        ++e.programIdx;
        ret gnext(e.goal);
      } else if (e.programIdx == 0) {
        ++e.programIdx;
        // fails 2nd time and cuts
        //e.goal.car.head = "false"; // super-hack :D
        backToCutPoint(parseInt(e.goal.car.get(0).raw()));
        ret false;
      } else {
        stackPop();
        ret false;
      }
    }

    if (e.programIdx >= l(e.program)) { // program loop ends
      removeLast(stack);
      ret false;
    }
      
    // now in program loop - get next clause to try
    
    Clause cc = e.program.get(e.programIdx);
    ++e.programIdx;
    
    // copy the clause; synchronize on it because it may come
    // from a shared Prolog interpreter
    
    Clause c;
    synchronized(cc) {
      c = cc.copy(this);
      Trail_Undo(e.trail);
    }
    
    S text = null;
    if (showStuff)
      //text = "  Goal: " + e.goal + ". Got clause: " + c;
      text = "Got clause: " + render(c);
    ++topUnifications;
    if (unify(e.goal.car, c.head)) {
      cc.used = true; // mark clause used
      if (showStuff) {
        log(indent(level()) + text);
        log(indent(level()) + "  Clause unifies to: " + render(c));
      }
      Goal gdash;
      if (c.nat != null) {
        if (showStuff)
          log(indent(level()) + " Clause is native.");
        if (!c.nat.yo(this, c.head)) {
          if (showStuff)
            log(indent(level()) + "Native clause fails");
          ret false;
        }
        gdash = e.goal.cdr;
      } else
        gdash = c.body == null ? e.goal.cdr : resolveCut(c.body).append(e.goal.cdr);
      if (showStuff)
        log(indent(level()) + "  gdash: " + render(gdash));
        
      if (gdash == null) {
        if (showStuff)
          log("SUCCESS!");
        ret true;
      } else {
        Entry e2 = new Entry(gdash);
        /*if (showStuff)
          log(indent(level()) + "New goal: " + render(gdash));*/
        stackAdd(e2);
        ret false;
      }
    } /*else
      if (showStuff)
        log(indent(level()) + "No match for clause.");*/
        
    ret false;
  }
  
  // resolve cut in clause body
  Goal resolveCut(Goal g) {
    if (g.car.is("!", 0))
      ret fixCut(g);
    if (g.cdr == null)
      ret g;
    ret new Goal(g.car, resolveCut(g.cdr));
  }
  
  // note stack length in cut
  Goal fixCut(Goal g) {
    ret new Goal(lisp("!", lstr(stack)), g.cdr); // max. one cut per clause
  }
  
  void stackAdd(Entry e) {
    stack.add(e);
    int n = l(stack);
    if (n > maxLevel) fail("Maximum stack level reached: " + n);
    if (n > maxLevelSeen) maxLevelSeen = n;
  }
  
  void addClause(S text) {
    addClause(nlParse(text));
  }
  
  void addClauses(L<Lisp> l) {
    for (Lisp clause : unnull(l))
      addClause(clause);
  }
  
  // synonym of addClause
  void addStatement(S text) {
    addClause(text);
  }
  
  void addClause(Lisp c) {
    addClause(clause(c));
  }
  
  void addClause(Lisp c, S name) {
    addClause(clause(c), name);
  }
  
  void addClause(Clause c) {
    addClause(c, null);
  }
  
  void addClause(Clause c, S name) {
    c.loadedFrom = name;
    program.add(c);
    if (c.head instanceof Var) {
      if (showStuff)
        log("WARNING: Clause is variable, will not be executed right now: " + c);
      ret;
    }
    int arity = c.head.size();
    growArityList(arity);
    programByArity.get(arity).add(c);
  }
  
  void growArityList(int arity) {
    while (arity >= l(programByArity))
      programByArity.add(new L);
  }
  
  boolean canSolve(Lisp goal) {
    ret canSolve(new Goal(prologify(goal)));
  }
  
  boolean canSolve(S goal) {
    ret canSolve(nlParse(goal));
  }
  
  boolean canSolve(Goal goal) {
    start(goal);
    while (!done())
      if (step())
        ret true;
    ret false;
  }
  
  S solveAsText(S goal, S var) {
    Map<S, Lisp> solution = solve(goal);
    ret solution == null ? null : nlUnparse(solution.get(addPrefix("$", var)));
  }
  
  // return variable map or null if unsolved
  Map<S, Lisp> solve(Lisp goal) {
    start(goal);

    ret nextSolution();
  }
  
  Map<S, Lisp> solve(S text) {
    ret solve(nlParse(text));
  }
  
  Map<S, Lisp> getUserVarMap() {
    Goal g = stack.get(0).goal;
    if (showStuff)
      log("UserVarMap goal: " + g);
    new HashMap<S, Lisp> map;
    for (Var v : findVars(g))
      if (v.isUserVar()) {
        Lisp term = resolve(v);
        boolean ok = !(term instanceof Var) || (term != v && ((Var) term).isUserVar());
        if (showStuff)
          log("UserVarMap var " + v + " ok: " + ok);
        if (ok)
          map.put(v.getName(), term);
      }
    ret map;
  }
  
  Map<S, Lisp> nextSolution() {
    if (showStuff)
      log("nextSolution");
    int n = 0;
    while (!done()) {
      ++n;
      if (step()) {
        if (showStuff)
          log("  solution found in step " + n);
        ret getUserVarMap();
      }
    }
    if (showStuff)
      log("\nNo solution");
    ret null;
  }
  
  void code(S text) {
    addTheory(text, "ad hoc");
  }
  
  void addTheory(S text, S name) {
    for (Clause c : parseProgram(text))
      addClause(c, name);
  }
    
  void addTheory(S text, Lisp tree) {
    addTheory(text, tree, null);
  }
  
  void addTheory(S text, Lisp tree, S name) {
    for (Clause c : parseProgram(text, tree))
      addClause(c, name);
  }
  
  L<Clause> parseProgram(S text) {
    ret parseProgram(text, nlParse(text));
  }
  
  L<Clause> parseProgram(S text, Lisp tree) {
    new L<Clause> l;
    if (nlIsMultipleStatements(text))
      for (Lisp part : tree)
        l.add(clause(part));
    else
      l.add(clause(tree));
    ret l;
  }
  
  L<Lisp> parseStatements(S text) {
    ret map(func(Clause c) { c.getStatement() }, parseProgram(text));
  }
    
  // Resolve top-level only
  Lisp resolve1(Lisp term) {
    if (term instanceof Var)
      ret ((Var) term).getValue();
    ret term;
  }
  
  // resolve all variables
  Lisp resolve(Lisp term) {
    term = resolve1(term);
      
    // smart recurse
    for (int i = 0; i < term.size(); i++) {
      Lisp l = term.get(i);
      Lisp r = resolve(l);
      if (l != r) {
        Lisp x = new Lisp(term.head);
        for (int j = 0; j < i; j++)
          x.add(term.get(j));
        x.add(r);
        for (i++; i < term.size(); i++)
          x.add(resolve(term.get(i)));
        ret x;
      }
    }
    
    ret term;
  }
  
  // looks for a bodyless rule in the program that matches the term
   // todo: eqic
  boolean containsStatement(Lisp term) {
    for (Clause c : program)
      if (c.body == null && c.nat == null && eq(c.head, term))
        ret true;
    ret false;
  }
  
  // closed == contains no variables
  boolean isClosedTerm(Lisp term) {
    if (term instanceof Var)
      ret false;
    else
      for (Lisp arg : term)
        if (!isClosedTerm(arg))
          ret false;
    ret true;
  }
  
  void addNative(BaseNative n) {
    addClause(prologify(new Clause(nlParse(n.pat), n)), "nat");
  }
  
  void addNatives(BaseNative... l) {
    for (BaseNative n : l)
      addNative(n);
  }
    
  void addNatives(L<BaseNative> l) {
    for (BaseNative n : l)
      addNative(n);
  }
  
  L<Lisp> getStackTerms() {
    new L<Lisp> l;
    for (Entry e : stack)
      l.add(e.goal.car);
    ret l;
  }
  
  void logOn() {
    log = new L;
    showStuff = true;
  }

  static abstract class BaseNative implements INative {
    S pat;
    Prolog p;
    Map<S, Lisp> m;
    
    *(S *pat) {}
    
    abstract boolean yo();
    
    public boolean yo(Prolog p, Lisp term) {
      m = new HashMap;
      this.p = p;
      try {
        // Terms are always resolved for native code!
        ret nlMatch(pat, p.resolve(term), m) && yo();
      } catch (Exception e) {
        ++p.exceptions;
        if (p.showStuff)
          p.log("Exception in native class " + getClass().getName() + ": " + getStackTrace(e));
        ret false;
      } finally {
        this.p = null;
      }
    }
    
    boolean unify(S var, Lisp term) {
      ret set(var, term);
    }
    
    boolean set(S var, Lisp term) {
      Lisp v = m.get(var);
      if (v == null)
        fail("Variable " + var + " not found");
      ret p.unify(v, term);
    }

    boolean unifyForeign(IdentityHashMap<Lisp, S> varMap, Map<S, Lisp> solution) {
      if (p.showStuff)
        p.log("unifyForeign with: " + structure(solution));
      for (Lisp v : varMap.keySet()) {
        S name = varMap.get(v);
        Lisp value = solution.get(name);
        if (value == null) continue;
        if (!p.unify(v, escapeVariables(value))) {
          ret false; // rollback?
        }
      }
      ret true;
    }
    
    // fills varMap
    Lisp exportVars(Lisp tree, IdentityHashMap<Lisp, S> varMap) {
      if (tree instanceof Var) {
        S name = varMap.get(tree);
        if (name == null) {
          name = "$_" + (varMap.size()+1);
          varMap.put(tree, name);
        }
        ret lisp(name);
      }
      
      Lisp lisp = new Lisp(tree.head);
      for (Lisp sub : tree)
        lisp.add(exportVars(sub, varMap));
      ret lisp;
    }
    
    // var = without $
    Lisp get(S var) {
      ret m.get(var);
    }
    
    S unq(S var) {
      ret m.get(var).unq();
    }
  } // BaseNative
  
  // Prolog constructor
  *() {
    addClause(lisp("true"));
    addBaseNatives();
  }
  
  *(Prolog p) {
    copyProgramFrom(p);
  }
  
  static class State {
    Trail trail;
    L<Entry> stack;
  }
  
  State saveState() {
    new State s;
    s.trail = sofar;
    s.stack = stack;
    sofar = null;
    ret s;
  }
  
  void restoreState(State s) {
    sofar = s.trail;
    stack = s.stack;
  }
  
  // auto-rewrite with all clauses in DB
  L<Lisp> rewrite() {
    ret rewriteWith(program, defaultRewriteMax);
  }
  
  L<Lisp> rewrite(int max) {
    ret rewriteWith(program, max);
  }
  
  // Note: rewriteTheory is not searched for facts (only rules)
  L<Lisp> rewriteWith(Prolog rewriteTheory) {
    ret rewriteWith(rewriteTheory.program());
  }
  
  L<Lisp> rewriteWith(L<Clause> rewriteTheory) {
    ret rewriteWith(rewriteTheory, defaultRewriteMax);
  }
  
  L<Lisp> rewriteWith(L<Clause> rewriteTheory, int max) {
    new L<Lisp> l;
    rewriteWithInto(rewriteTheory, limitedListCollector(l, max));
    ret l;
  }
  
  void rewriteInto(Collector<Lisp> collector) {
    rewriteWithInto(program, collector);
  }
  
  void rewriteWithInto(L<Clause> rewriteTheory, Collector<Lisp> collector) {
    if (collector.full()) ret;
    for (Prolog.Clause clause : rewriteTheory) {
      if (clause.body == null) continue; // need conditions to rewrite anything
      
      // usual safe clause copying
      
      Trail t = Trail_Note();
      Clause c;
      synchronized(clause) {
        c = clause.copy(this);
        Trail_Undo(t);
      }
      
      State state = saveState();
      try {
        start(c.body);
        while (!done()) {
          if (step()) {
            Lisp term = resolve(c.head);
            if (!isClosedTerm(term)) {
              if (showStuff)
                log("Not a closed term, skipping: " + term);
              continue;
            }
            
            if (containsStatement(term)) {
              if (showStuff)
                log("Statement exists, skipping: " + term);
              continue;
            }
            
            if (collector.contains(term))
              continue;
              
            if (showStuff)
              log("Found new statement: " + term);
            collector.add(term);
            if (collector.full()) {
              log("Collector full");
              break;
            }
          }
        }
      } finally {
        restoreState(state);
      }
    }
  }
  
  static class NewCollector extends BaseNative {
    *() { super("$x = new collector"); }
    
    boolean yo() {
      ret set("x", new LCollector);
    }
  }
  
  class Save extends BaseNative {
    *() { super("saveTo($x, $collector)"); }
    
    boolean yo() {
      LCollector collector = (LCollector) get("collector");
      Lisp x = get("x");
      collector.solutions.add(resolve(x));
      ret true;
    }
  }
  
  static class Retrieve extends BaseNative {
    *() { super("$x = retrieve($collector)"); }
    
    boolean yo() {
      print("Retrieve: collector = " + get("collector"));
      LCollector collector = (LCollector) get("collector");
      ret set("x", nlList(collector.solutions));
    }
  }
  
  void addBaseNatives() {
    addNatives(new NewCollector, new Save, new Retrieve);
  }
  
  static Lisp escapeVariables(Lisp tree) {
    if (tree instanceof Var) {
      S name = ((Var) tree).prettyName();
      ret lisp("[]", "var", name);
    }
    
    Lisp lisp = new Lisp(tree.head);
    for (Lisp sub : tree)
      lisp.add(escapeVariables(sub));
    ret lisp;
  }
  
  boolean addClauseIfNew(Lisp clause, S name) {
    if (containsStatement(clause)) ret false;
    addClause(clause, name);
    ret true;
  }
  
  L<Clause> getUsedClauses() {
    new L<Clause> l;
    for (Clause c : program)
      if (c.used)
        l.add(c);
    ret l;
  }
  
  L<S> getUsedTheories() {
    new TreeSet<S> theories;
    for (Clause c : getUsedClauses())
      theories.add(or(c.loadedFrom, "?"));
    ret asList(theories);
  }
  
  void think(Lisp x) {
    addClauseIfNew(x, "thought");  // TODO: vars and stuff?
  }
  
  L<Lisp> getMemorizedStatements() {
    new L<Lisp> l;
    for (Clause c : program)
      if (c.body == null && c.nat == null && c.head.is("[]", 2) && c.head.get(0).is("memorized"))
        l.add(c.head);
    ret l;
  }
  
  S showClause(Clause c) {
    ret nlUnparse(c.head) + (c.body == null ? "" : " :- ...");
  }
  
  S showProgram() {
    new L<S> l;
    for (Clause c : program)
      l.add(showClause(c));
    ret n(l(program), "statement") + " " + slackSnippet(joinLines(l  ));
  }
  
  void copyProgramFrom(Prolog p) {
    program.addAll(p.program);
    growArityList(l(p.programByArity));
    for (int i = 0; i < l(p.programByArity); i++)
      programByArity.get(i).addAll(p.programByArity.get(i));
  }
  
  void addProgram(L<Clause> clauses, S loadedFrom) {
    for (Clause c : clauses)
      addClause(c, loadedFrom);
  }
  
  void addClauses(S text) {
    addTheory(text, fsI(programID()));
  }
  
  L<S> statementsAsText() {
    ret statementsAsText(0);
  }
  
  L<S> statementsAsText(int startingFromIndex) {
    new L<S> l;
    for (int i = startingFromIndex; i < l(program); i++) {
      Clause c = program.get(i);
      if (c.nat == null) {
        if (c.body != null)
          l.add("[if ? then " + nlUnparse(c.head, false) + "]"); // TODO
        else
          l.add(nlUnparse(c.head, false));
      }
    }
    ret l;
  }
  
  int mark() {
    ret l(program);
  }
  
  L<Clause> program() { ret program; }
  
  L<Lisp> rewriteAndSave() {
    L<Lisp> l = rewrite();
    addClauses(l);
    ret l;
  }
} // class Prolog

Began life as a copy of #1002868