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

}