!759

!include #1002884 // Prolog with shared clauses

!include #1002933 // Natives

static boolean showLog, printTimings = true;

static Prolog p;

static Prolog parsingInterpreter;

//static O theoryBot;

static Method getTheoryMethod;

p {

  new Prolog p;

  parsingInterpreter = p;

  p.addNatives(new IntMul, new IntDiv, new IntAdd, new IntMinus);

  p.addNatives(new GreaterThan, new HeadExists, new TheoriesList);

  p.addNatives(new tocons, new fromcons, new LessThan, new arg, new Arity);

  p.addNatives(new operator, new Unquote, new IsQuoted, new IsWord, new RemoveWord, new GetTheory, new TextOfTheory);

  p.addNatives(new Solve1, new Think, new MemorizeImpl, new RewriteWithTheory, new NLSafeParse);

  p.addNatives(new StartsWith);

}

static class CacheEntry {

  S text;

  Lisp parsed;

  L<Prolog.Clause> program;

  *(S *text) {

  }

  Lisp getParsed() {

    if (parsed == null)

      parsed = nlParse(text);

    ret parsed;

  }

  L<Prolog.Clause> getProgram() {

    if (program == null)

      program = parsingInterpreter.parseProgram(text);

    ret program;

  }

}

static new Map<CIString, CacheEntry> parseCache;

static S getTheoryFromBot(S name) ctex {

  if (getTheoryMethod != null)

    ret (S) getTheoryMethod.invoke(null, name);

  ret (S) callOpt(theoryBot(), "getTheoryOpt", name);

}

static void cacheGetTheoryMethod() {

  getTheoryMethod = findMethod(theoryBot(), "getTheoryOpt", "");

}

static S findTheory(S name) {

  ret getTheoryFromBot(name);

}

static S saveTheory(S name, S text) {

  ret (S) callOpt(theoryBot(), "saveTheory", name, text);

}

static Lisp getParsedTheory(S name) {

  CacheEntry entry = getCacheEntry(name);

  ret entry == null ? null : entry.getParsed();

}

static L<Prolog.Clause> getProgram(S name) {

  CacheEntry entry = getCacheEntry(name);

  ret entry == null ? null : entry.getProgram();

}

static CacheEntry getCacheEntry(S name) {

  S text = findTheory(name);

  if (text == null) ret null;

  CacheEntry entry = parseCache.get(new CIString(name));

  if (entry == null || neq(entry.text, text)) {

    entry = new CacheEntry(text);

    parseCache.put(new CIString(name), entry);

  }

  ret entry;

}

static S prettyPrintTerms(L<Lisp> l, boolean outerBrackets) {

  new L<S> out;

  for (Lisp term : l) {

    S s = nlUnparse(term, !outerBrackets);

    //out.add(outerBrackets ? "[" + s + "]" : s);

    out.add(s);

  }

  ret joinLines(out);

}

static void loadTheories(Prolog p, L<S> theoryNames) {

  if (theoryNames.contains("signed")) {

    theoryNames.remove("signed");

    theoryNames.addAll(getLiveTheories());

  }

  if (theoryNames.contains("signedstefan")) {

    theoryNames.remove("signedstefan");

    theoryNames.addAll(getLiveTheories ("stefanreich"));

  }

  cacheGetTheoryMethod();

  try {

    for (S t : asSet(theoryNames)) { // todo: ignore case

      loadTheoryImpl(p, t);

      long n = getTheoryCounter(t);

      for (long i = 1; i <= n; i++)

        loadTheoryImpl(p, t + "." + i);

    }

  } finally { 

    getTheoryMethod = null;

  }

}

static long getTheoryCounter(S name) {

  //ret (long) call(theoryBot(), "getTheoryCounter", name);

  S text = findTheory(name + ".count");

  ret isEmpty(text) ? 0 : parseLong(text);

}

static void loadTheoryImpl(Prolog p, S name) {

  L<Prolog.Clause> program = getProgram(name);

  if (program != null)

    p.addProgram(program, name);

}

static S solutionPrettyPrint(Map<S, Lisp> solution) {

  S s = "FALSE";

  if (solution != null) {

    new L<S> l;

    solution = new TreeMap(solution); // sort

    for (S var : solution.keySet())

      l.add(var + " = " + nlUnparse(solution.get(var), false));

    s = "TRUE.\n" + slackSnippetOpt(joinLines(l));

  }

  /*if (showStack)

    s += "\nStack:" + slackSnippetOpt(prettyPrintTerms(p.getStackTerms(), false));*/

  if (showLog) {

    L<S> usedTheories = p.getUsedTheories();

    L<S> lines = litlist("Used theories: " + join(", ", usedTheories));

    L<Lisp> mem = p.getMemorizedStatements();

    if (nempty(mem)) {

      lines.add("Thoughts:");

      for (Lisp x : mem)

        lines.add("  " + nlUnparse(x));

    }

    lines.addAll(p.log);

    s += "\n" + slackSnippet(lines);

  }

  ret s;

}

static Prolog newProlog(L<S> theoryNames) {

  ret p = newSubProlog(theoryNames, showLog);

}

static Prolog newProlog(L<S> theoryNames, boolean showLog) {

  ret p = newSubProlog(theoryNames, showLog);

}

static Prolog newSubProlog(L<S> theoryNames, boolean showLog) {

  long startTime = now();

  int parses = nlParse_count.get();

  Prolog p = new Prolog;

  if (showLog)

    p.logOn();

  p.copyProgramFrom(parsingInterpreter); // natives!

  long t2 = now();

  loadTheories(p, theoryNames);

  if (printTimings) {

    parses = nlParse_count.get()-parses;

    long end = now();

    long time = end-startTime;

    t2 = end-t2;

    print("Making prolog interpreter with " + l(theoryNames) + " theories: " + time + " ms (" + parses + " parses, " + t2 + " ms in loadTheories)");

  }

  ret p;

}

// n = how many solutions to print

static S solve(Lisp question, L<S> theoryNames, int n) {

  new StringBuilder buf;

  question = new EvalTransform().evalTransformQuestion(question);

  newProlog(theoryNames);

  time {

    try {

      Map<S, Lisp> solution = p.solve(question);

      if (solution == null)

        buf.append("FALSE in " + structure(theoryNames) + (p.log != null ? "\n" + slackSnippet(p.log) : ""));

      else {

        buf.append(solutionPrettyPrint(solution) + "\n");

        while (--n > 0) {

          solution = p.nextSolution();

          if (solution == null) break;

          buf.append(solutionPrettyPrint(solution) + "\n");

        }

        if (p.nextSolution() != null)

          buf.append("[more]");

        else

          buf.append("[done]");

      }

    } catch (Exception e) {

      ret e + "\n" + slackSnippet(p.log);

    }

  }

  buf.append(" " + lastTiming() + " ms");

  ret str(buf);

}

static L<S> nlParseStringList(Lisp tree) {

  if (tree.isLeaf())

    ret litlist(unquote(tree.raw()));

  new L<S> l;

  for (Lisp t : tree) {

    if (!t.isLeaf()) continue; // huh?

    S s = t.head;

    if (eq(s, ",") /*|| eq(s, "and")*/) continue;

    l.add(unquote(s));

  }

  ret l;

}

static L<S> getTheoryNames() {

  ret (L) callOpt(theoryBot(), "getTheoryNames");

}

static L<S> getLiveTheories() {

  ret concatLists (

    getLiveTheories (getUserName ()),

    getLiveTheories ("stefanreich"));

  }

static L<S> getLiveTheories(S user) {

  ret empty(user) ? litlist() : (L) callOpt(theoryBot(), "getTheoriesSignedByAs", user, "live");

}

static S solve(S s, boolean showLog) {

  main.showLog = showLog;

  s = s.trim();

  int n = 1;

  int i = s.indexOf(']');

  if (i >= 2) {

    S s2 = dropPrefix("[", substring(s, 0, i));

    if (isInteger(s2)) {

      n = parseInt(s2);

      s = s.substring(i+1).trim();

    }

  }

  Lisp tree = nlParse(s);

  //ret structure(tree);

  new Map<S, Lisp> m;

  if (nlMatch("$text in $theory", tree, m)) {

    print("text in theory");

    Lisp question = m.get("text");

    Lisp t = m.get("theory");

    L<S> theoryNames = nlParseStringList(t);

    ret solve(question, theoryNames, n);

  }

  if (nlMatch("theory $t", tree, m)) {

    print("theory");

    S theoryName = unquote(m.get("t").raw());

    ret solve(nlParse(findTheory(theoryName)), litstringlist("signed"), n);

  }

  if (nlMatch("$text", tree, m)) {

    print("text");

    Lisp question = m.get("text");

    ret solve(question, litstringlist("signed"), n);

  }

  ret "hm?";

}

synchronized answer {

  if "top unifications"

    ret p == null ? "-" : str(p.topUnifications);

  if (!attn()) ret null;

  if (swic(s, "solve ")) exceptionToUser {

    s = dropPrefixIgnoreCase("solve ", s);

    ret solve(s, false);

  }

  if (swic(s, "eval ")) exceptionToUser {

    s = trim(dropPrefixIgnoreCase("eval ", s));

    S var = nlMakeUnusedVar(s);

    s = var + " = " + s;

    ret solve(s, false);

  }

  if (swic(s, "log ")) exceptionToUser {

    s = dropPrefixIgnoreCase("log ", s);

    ret solve(s, true);

  }

  if (swic(s, "say ")) exceptionToUser {

    s = dropPrefixIgnoreCase("say ", s);

    new Map<S, Lisp> mm;

    if (nlMatch("$text in $theory", s, mm)) {

      Lisp question = mm.get("text");

      Lisp t = mm.get("theory");

      s = "[[think [user says " + nlUnparse(question, false) + "]] and [say $x]] in " + nlUnparse(t, false);

      print("s = " + s);

      ret solve(s, true);

    }

    ret "woot syntax";

  }

  if "produce *" exceptionToUser {

    ret produce(m.unq(0));

  }

  if "my program" exceptionToUser {

    S user = getUserName();

    if (empty(user)) ret "go to slack please";

    p = new Prolog;

    loadTheories(p, getLiveTheories());

    ret p.showProgram();

  }

  if "log" exceptionToUser {

    ret slackSnippet(p.log);

  }

  if "rewrite * with *" exceptionToUser {

    ret rewrite(m.unq(0), m.unq(1), null);

  }

  if "rewrite * with * as *" exceptionToUser {

    ret rewrite(m.unq(0), m.unq(1), m.unq(2));

  }

  if "time findTheory" exceptionToUser {

    time {

      //theoryBot = getBot("#1002762");

      cacheGetTheoryMethod();

      try {

        for (int i = 0; i < 1000; i++)

          findTheory("and");

      } finally {

        //theoryBot = null;

        getTheoryMethod = null;

      }

    }

    ret (lastTiming()/1000.0) + " ms";

  }

}

static S rewrite(S tname1, S tname2, S tname3) {

  newProlog(litlist(tname1, "signed"), true);

  L<Prolog.Clause> rewriteTheory = p.parseProgram(findTheory(tname2));

  L<Lisp> rewritten = p.rewriteWith(rewriteTheory);

  S text = prettyPrintTerms(rewritten, true);

  if (tname3 == null)

    ret slackSnippet(text) + "\n" + slackSnippet(p.log);

  ret saveTheory(tname3, text);

}

static S produce(S theoryName) {

  S outName = theoryName + ".out";

  showLog = false;

  newProlog(litlist(theoryName));

  S question = "say $x";

  Lisp out = lisp("[]");

  p.start(question);

  int max = 100;

  while (out.size() < max) {

    Map<S, Lisp> solution = p.nextSolution();

    if (solution == null) break;

    out.add(solution.get("$x"));

  }

  ret (out.size() >= max ? "WARNING MAXED OUT\n" : "") + saveTheory(outName, nlUnparse(out));

}

static void incrementTheory(S name, Lisp value) {

  call(theoryBot(), "incrementTheory", name, nlUnparse(value));

}

static O theoryBot() {

  ret /*or(theoryBot,*/ getBot("#1002762")/*)*/;

}