!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")/*)*/;
}