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

}