!752

!include #1002752 // newest LThread

static interface TheoryHolder {
  public Lisp getTheory(S name);
}

static class Rewriter {
  new L<S> log;
  new L<Lisp> statements;
  TheoryHolder holder;
  int safety, exceptions;
  int safetyMax = 10000, statementsMax = 100;
  boolean nativeOn; // use all the native functions defined in bots
  
  *(TheoryHolder *holder, L<S> theoryNames) {
    for (S name : theoryNames) {
      if (eq(name, "native"))
        nativeOn = true;
      else {
        Lisp t = null;
        pcall {
          t = holder.getTheory(name);
        }
        if (t == null)
          log.add(format("Warning: Theory * not found", name));
        else
          addTheory(t);
      }
    }
  }
  
  void addTheory(Lisp tree) {
    if (isJuxta(tree))
      for (Lisp part : tree)
        addTheory(part);
    else
      statements.add(tree);
  }
  
  IEngine makeEngine() {
    IEngine engine = null;
    if (nativeOn) {
      final L<Method> nativeBots = findNativeMethods();
      engine = new IEngine() {
        public boolean yo(Native n) {
          n.printExceptions = true;
          
          for (Method method : nativeBots)
            if (n.callExternal(method))
              ret true;
          ret false;
        }
        
        public void memorize(Lisp statement) {}
        public void forget(Lisp statement) {}
      };
    }
    ret engine;
  }
  
  LThread newLThread(Lisp rule, IEngine engine) {
    LThread thread = new LThread(rule);
    thread.engine = engine;
    //thread.log = log;
    thread.statements.addAll(statements);
    ret thread;
  }
  
  // do the rewrites!
  void go() {
    IEngine engine = makeEngine();
    boolean anyChange;
    safety = 0;
    do {
      anyChange = false;
      
      // run rules
      
      for (Lisp rule : cloneList(statements))
        if (rule.head.startsWith("if ")) try {
          LThread thread = newLThread(rule, engine);
          boolean success = thread.run();
          if (success) {
            for (Lisp s : thread.output)
              if (!statements.contains(s)) {
                statements.add(s);
                anyChange = true;
              }
          }
        } catch (Exception e) {
          exceptions++;
        }
    } while (anyChange && ++safety < safetyMax && l(statements) < statementsMax);
  }
  
  boolean query(Lisp q, SNLMatches m) {
    IEngine engine = makeEngine();
    LThread thread = newLThread(lisp("if *", q), engine);
    if (!thread.run()) ret false;
    m.addAll(thread.m);
    ret true;
  }
}

static Rewriter newRewriter(S description) {
  ret new Rewriter(new TheoryHolder() {
    public Lisp getTheory(S name) {
      ret getTheoryFromBot(name);
    }
  }, unquoteAll(codeTokensOnly(javaTok(description))));
}

static S doQuery(S query, Rewriter r) {
  new SNLMatches matches;
  if (!r.query(snlToTree(query), matches)
    && !r.query(snlToTree("X = " + query), matches)) // automagic
    ret "false\n";
  
  r.go();
  L<S> l = cloneList(r.log);
  for (S var : matches.keySet())
    l.add(var + " = " + snlFromTree(matches.get(var)));
  ret "TRUE\n" + slackSnippetOpt(fromLines(l));
}

answer {
  if (!attn()) ret null;
  
  if (matchStart("rewrite", s, m)) exceptionToUser {
    Rewriter r = newRewriter(m.rest());
    int n = l(r.statements);
    r.go();
    L<S> l = cloneList(r.log);
    L<Lisp> newStatements = subList(r.statements, n);
    if (empty(newStatements))
      l.add("<no results>");
    else
      for (Lisp tree : newStatements)
        l.add(snlFromTree(tree));
    ret slackSnippet(fromLines(l));
  }
  
  if (matchStart("query *", s, m)) exceptionToUser {
    ret doQuery(m.unq(0), newRewriter(m.rest()));
  }
  
  if (s.startsWith("nat ") || s.startsWith("native ")) exceptionToUser {
    s = dropUntilSpace(s);
    ret doQuery(s, newRewriter("native"));
  }
  
  if "list native bots"
    ret structure(findNativeBots());
}

static Lisp getTheoryFromBot(S name) {
  ret (Lisp) quickImport(callOpt(getBot("#1002762"), "getParsedTheory", name));
}

static L<Method> findNativeMethods() {
  new L l;
  for (S id : getSubBotIDs()) {
    O bot = getBot(id);
    //Method m = findMethod(bot, "yo", n); // doesn't work b/c of realms
    Method m = findMethodNamed(bot, "safe");
    if (isNativeMethod(m)) {
      l.add(m);
      Class c = m.getDeclaringClass();
      print("Declaring class: " + ihc(c) + ", bot: " + ihc(bot));
    }
  }
  print("Native methods found: " + l(l));
  ret l;
}

static L<S> findNativeBots() {
  new L l;
  for (S id : getSubBotIDs()) {
    O bot = getBot(id);
    Method m = findMethodNamed(bot, "safesafe");
    if (isNativeMethod(m))
      l.add(id);
  }
  ret l;
}

static boolean isNativeMethod(Method m) {
  if (m == null) ret false;
  Class[] p = m.getParameterTypes();
  if (p.length != 1) ret false;
  S name = p[0].getName();
  //print("Parameter type: " + name);
  ret eq("main$Native", name);
}