!752

static PersistentMap<S, S> theories;
static new Map<S, Lisp> parsedTheories;
static new Index index;

static class Index {
  new L<L<Lisp>> byArity;
  
  void addTheory(Lisp tree) {
    for (Lisp statement : tree) {
      int arity = statement.size();
      while (arity >= l(byArity))
        byArity.add(new L);
      byArity.get(arity).add(statement);
    }
  }
  
  Lisp searchOne(S query) {
    Lisp tree = nlParse(query);
    int arity = tree.size();
    L<Lisp> entries = get(byArity, arity);
    if (entries != null)
      for (Lisp statement : entries)
        if (match(tree, statement))
          ret statement;
    ret null;
  }
  
  static boolean match(Lisp query, Lisp statement) {
    new HashMap matches;
    //print("Checking: " + nlUnparse(statement));
    ret nlMatch(query, statement, matches);
  }
}

p {
  File theoriesFile = getProgramFile("theories-downloaded");
  int n = (int) theoriesFile.length();
  S url = "http://ai1.lol/1002762/raw/theoriesInc?" + makePostData("n", n);
  S page = loadPage(url);
  S id = firstLine(page);
  page = dropFirstLine(page);
  int m = parseInt(firstLine(page).trim());
  page = dropFirstLine(page);
  page = htmldecode(page);
  //(n + l(toUtf8(page)))
  appendToTextFile(theoriesFile, page);
  int n2 = (int) theoriesFile.length();
  if (m == n2)
    print(n == n2 ? "Nothing to download (n=" + n + ")" : "Sizes ok - " + n + " -> " + n2);
  else
    print("Size mismatch? " + m + "/" + n2);
    
  theories = new PersistentMap(theoriesFile);
  print(theories.size() + " theories. Parsing...");
  
  time {
    for (S theoryName : theories.keySet()) {
      S text = theories.get(theoryName);
      Lisp tree = nlParseExpand(text);
      parsedTheories.put(theoryName, tree);
    }
  }
  
  print("Parsed all. Making index.");
  
  time {
    for (S theoryName : parsedTheories.keySet()) {
      Lisp tree = parsedTheories.get(theoryName);
      index.addTheory(tree);
    }
  }
  
  print("Made index. Trying a search");
  
  S query = "mrshutco lives in $x";
  print(query);
  print("  " + nlUnparse(index.searchOne(query)));
}