sclass PhilosophyBot1 {
  static transformable record LogicRule(lhs, rhs) {
    int n; // when added
    O trail;
    
    toString {
      ret (n == 0 ? "" : "[" + n + "] ") + lhs + " => " + rhs;
    }
  }
  static transformable record And(a, b) {}
  static transformable record If(condition, thenBlock, elseBlock) {}
  static transformable record For(var, condition, body) {} // don't need var actually
  static transformable record ForIn(var, expr, body) {}
  static transformable record Assignment(var, expr) {}
  static transformable record While(condition, body) {}

  replace NPRet with O. // native predicate return type (Bool/SS/null)

  // like a native predicate, but doesn't return anything
  sclass CodeFragment {
    S head;
    IVF2<SS, Env> body;
    bool keepBrackets;
    
    *(S *head, IVF2<SS, Env> *body, bool *keepBrackets) {}
    *(S *head, IVF2<SS, Env> *body) {}
    
    toString { ret stdToString(this); }
  }

  sclass Env {
    bool wantAlternatives;

    bool wantAlternatives() { ret wantAlternatives; }
  }

  srecord WithAlternative(IF0<O> alternative, O result) {}
  
  // body takes variable mapping
  // body can return
  //   Bool => immediate result (ok or fail)
  //   SS   => variable mapping
  //   WithAlternative
  //   Iterator<NPRet>
  //   null => not applicable
  // For "for $x in ..." statements, return a Iterable<stringable>?
  srecord NativePredicate(S head, IF2<SS, Env, NPRet> body) {}
  
  replace ProcedureToRun with Proc.
  replace Proc with L. // procedures are a list of statements
  
  // trail of a transformed fact
  srecord TTransformed(S fact, IF1<S> transformer) {}

  transient S program;
  transient bool programLoaded;
  transient int maxRounds = 1000;
  transient int maxFacts = 1000;
  transient Set<S> facts = syncLinkedCISet();
  transient Set<S> originalFacts = ciSet();
  transient new LinkedHashSet<LogicRule> logicRules; // modified with sync
  transient new AllOnAll<LogicRule, S> rulesOnFacts;
  transient new AllOnAll<CodeFragment, S> codeOnFacts;
  transient new AllOnAllWithUpdates<IVF1<S>, S> anyCodeOnFacts;
  transient new AllOnAll/*WithUpdates*/<IVF1<LogicRule>, LogicRule> anyCodeOnRules;
  transient new L<ProcedureToRun> proceduresToRun;
 // parsed procedures
  transient long proceduresExecuted;
  transient new L<NativePredicate> nativePredicates;
  transient bool debugNativeCalls = true, debugAllCmds = true;
  transient bool verbose = true;
  transient bool printStackTraces;
  transient new L onProcedureEnded;
  transient new L<IVF1<LogicRule>> onLogicRuleAdded;
  transient new L<IVF1<S>> onFactAdded;
  transient bool printNonMatches, debugContradictionChecks;
  transient bool standardImportsLoaded;
  transient bool curryAllRules = true; // rewrite "a & b => c" to a => b => c
  transient int logicRulesCounter;
  transient bool thoughtBegun;
  transient bool printFactsAfterThinking = true;
  transient bool noteSimplificationsAsFacts; // not a good idea - leads to endless loops
  transient bool parsing;

  // return true when you handled adding the rule
  transient new L<IPred<LogicRule>> logicRulePreprocessors;
  
  // return true when you handled adding the fact
  transient new L<IPred<S>> factPreprocessors;
  
  // extra stuff that is done every round
  transient new L<Runnable> extraLogicOperations;

  transient Set<S> vars = litciset("x", "y", "z");
  
  // phrase replacements that are made in every fact.
  // functionality is enabled by philosophyBot1_addDeepReplacement
  transient SS deepReplacements;
  
  transient L<IF1<S>> deepTransformers;
  transient L<IF1<S, WithTrail<S>>> trailEnabledDeepTransformers;
  
  // fact -> trail. to enable, initialize with ciMap()
  transient MapSO trails;
  
  Map extensions;
  
  *() {
    // find contradictions
    anyCodeOnFacts.newA(fact -> {
      Bool b = checkNativeCondition(fact);
      if (debugContradictionChecks)
        print("Fact check: " + b + " - " + fact);
      if (isFalse(b))
        addFactWithTrail("contradiction", trails == null ? null : fact);
    });
    
    _standardHandlers();
  }
  *(S *program) { this(); }
  
  void addRule(S s) {
    PairS p = splitAtFirstDoubleArrow(javaTokWithBrackets(s));
    if (p == null) if (verbose) print("addRule failed: " + s);
    addLogicRuleWithTrail(new LogicRule(splitAtAmpersand2(p.a), p.b),
      litorderedmap(op := "addRule", +s));
  }
  
  void addRules(Iterable<S> l) {
    fOr (S s : l) addRule(s);
  }
  
  O splitRuleRHS(O rhs) {
    if (rhs cast S) {
      PairS p = splitAtFirstDoubleArrow(javaTokWithBrackets(rhs));
      if (p != null) ret splitRuleRHS(new LogicRule(splitAtAmpersand2(p.a), splitRuleRHS(p.b)));
    
      ret splitAtAmpersand2(rhs);
    }
    ret rhs;
  }
  
  LogicRule curryLHS(LogicRule rule) {
    while licensed {
      O lhs = rule.lhs;
      if lhs is And(O a, O b) {
        LogicRule r = rule;
        rule = new LogicRule(a, new LogicRule(b, rule.rhs));
        rule.trail = r.trail;
      }
      else break;
    }
    ret rule;
  }
  
  void addLogicRuleWithTrail(LogicRule rule, O trail) {
    rule.trail = trail;
    addLogicRule(rule);
  }

  void addLogicRule(LogicRule rule, S originalText) {
    //print("originalText=" + originalText + " for " + rule);
    addLogicRuleWithTrail(rule, originalText);
  }
  
  void addLogicRule(LogicRule rule) {
    rule.rhs = splitRuleRHS(rule.rhs);
    
    if (curryAllRules)
      rule = curryLHS(rule);

    for (IPred<LogicRule> p : logicRulePreprocessors)
      if (p.get(rule)) ret; // has been preprocessed
      
    rule.n = ++logicRulesCounter;
      
    if (printStackTraces) printStackTrace(str(rule));
    if (trails != null && rule.trail == null)
      if (parsing)
        rule.trail = "initial rule";
      else
        fail("No trail for rule: " + rule);
        
    // is LHS a native predicate? then eval immediately
    // TODO: multiple conditions
    Bool b = checkConditionOpt(rule.lhs);
    if (isFalse(b)) ret; // drop rule
    if (isTrue(b))
      addRewrittenRHS(rule.rhs, rule);

    if (syncAdd(logicRules, rule)) {
      if (verbose) print("Got logic rule", rule);
      pcallFAll(onLogicRuleAdded, rule);
      anyCodeOnRules.newB(rule);
      rulesOnFacts.newA(rule); // to combine it with the facts
    }
  }
  
  void addFacts(Iterable<S> l) {
    fOr (S fact : l) addFact(fact);
  }
  
  void addFactWithTrail(WithTrail<S> fact) {
    if (fact != null) addFactWithTrail(fact!, fact.trail);
  }
  
  void addFactWithTrail(S fact, O trail) {
    S cleaned = addFact(fact);
    setTrail(cleaned, trail);
  }
  
  void setTrail(S fact, O trail) {
    mapPut(trails, fact, trail);
  }

  // return cleaned version
  S addFact(S fact) {
    ping();
    fact = trim(fact);
    if (empty(fact)) null;
    
    if (l(facts) >= maxFacts) null;
    
    fact = tok_deRoundBracket(fact);
    
    if (printStackTraces) printStackTrace("Adding fact: " + fact);

    if (parsing && getTrail(fact) == null) setTrail(fact, "initial fact");
    
    for (IPred<S> p : factPreprocessors)
      if (p.get(fact)) null; // has been preprocessed

    // Check if it's a procedure
    LS tok = mainTokenize(fact);
    if (countCodeTokens(tok) == 2 && firstTokenEqic(tok, "proc")
      && isCurlyBracketed(getCodeToken(tok, 1))) pcall {
        // It's a procedure!
        S proc = uncurly_keepSpaces(getCodeToken(tok, 1));
        if (proceduresToRun.add(parseProcedure(proc))) {
          if (verbose) print("Got procedure:");
          if (verbose) print(indentx("> ", proc));
        }
    } /*else if (countCodeTokens(tok) == 2 && firstTokenEqic(tok, "java")
      && isCurlyBracketed(getCodeToken(tok, 1))) pcall {
        // It's Java code
        
    }*/ else // It's a fact, not a procedure
      if (facts.add(fact)) {
        if (verbose) print("Got fact: " + fact);
        pcallFAll(onFactAdded, fact);
        rulesOnFacts.newB(fact); // to combine it with the rules
        codeOnFacts.newB(fact);
        anyCodeOnFacts.newB(fact);
      }
      
    ret fact;
  }

  void addRewrittenRHS(O o, O trail) {
    if (o cast LogicRule)
      addLogicRuleWithTrail(o, trail);
    else if o is And(O a, O b) {
      addRewrittenRHS(a, o);
      addRewrittenRHS(b, o);
    } else if (o != null)
      addFactWithTrail((S) o, trail);
  }

  void addFactFromProgram(S fact) {  
    if (countJavaTokens(fact) == 0) ret;
    fact = javaDropAllComments(fact);
    originalFacts.add(fact);
    addFact(fact);
  }

  void runProcedure(S proc) pcall {
    if (verbose) print("Running procedure.");
    runParsedProcedure(parseProcedure(proc));
  }

  void runParsedProcedure(Proc commands) {
    runParsedProcedure(commands, proceduresToRun);
  }
  
  void runParsedProcedure(Proc commands, L<Proc> whereToPostCode) {
    ++proceduresExecuted;
    new Env env;
    L remainingCommands = cloneLinkedList(commands);
    O cmd;
    while not null (cmd = popFirst_ping(remainingCommands)) {
      if (cmd cast L) continue with runParsedProcedure(cmd);
      if (cmd cast Runnable) continue with cmd.run();
      if (debugAllCmds)
        print("Running cmd: " + sfu(cmd));
      if cmd is If(O condition, O thenBlock, O elseBlock) {
        O blockToRun = checkCondition(condition) ? thenBlock : elseBlock;
        runParsedProcedure(ll(blockToRun));
      } else if cmd is For(O var, O condition, O body) {
        // make a new logic rule and add it
        // assume the variable is globally declared as a variable
        addLogicRuleWithTrail(new LogicRule(condition, "proc {\n" + body + "\n}"), litorderedmap(op := "for"));
      } else if cmd is While(O condition, O body) {
        bool b = checkCondition(condition);
        if (!b) continue;
        whereToPostCode.add(ll(body, cmd));
      } else if cmd is Assignment(S var, S expr) {
        S result = cast runNativePredicate(expr, new Env);
        SS mapping = litcimap(var, result);
        remainingCommands = mapToLinkedList(remainingCommands,
          c -> replaceVars(c, mapValues optRound(mapping)));
      } else if cmd is ForIn(S var, S expr, O body) {
        // XXX
        O result = runNativePredicate(expr, new Env);
        if (!result instanceof Iterable) {
          if (verbose) print("Warning: result of " + expr + " not iterable (" + shortClassName(result) + ")");
          continue;
        }
        Iterator it = iterator((Iterable) result);
        Runnable step = r {
          if (!it.hasNext()) ret;
          S value = str(it.next());
          SS map = litcimap(var, value);
          O body2 = replaceVars(body, map);
          //print("ForIn: " + map + " => " + body2);
          whereToPostCode.add(ll(body2, this));
        };
        step.run();
      } else if (cmd cast S) {
        O result = runNativePredicate(cmd, env);
        if (result != null) {
          result = unpackWithAlternativeOrIterator(result);
          if (isFalse(result)) ret;
          if (isTrueOpt(result)) continue;
          if (result cast S)
            continue with addFact(result);
          SS mapping = cast result; // assume it's a variable mapping
          // apply to all remaining commands and continue
          L remainingCommands2 = mapToLinkedList(remainingCommands,
            c -> replaceVars(c, mapValues optRound(mapping)));
          if (verbose) print("Applying var mapping " + mapping + " to " + remainingCommands
            + " => " + remainingCommands2);
          remainingCommands = remainingCommands2;
        } else
          addFact(cmd);
      } else if (cmd != null)
        fail("Unimplemented command: " + cmd);
    }
    pcallFAll(onProcedureEnded, commands); // notify listeners
  }

  // return var mapping (SS), Bool or null for no matching predicate
  // or result verbatim (e.g. Iterable)
  O runNativePredicate(S s, Env env) {
    for (NativePredicate np : nativePredicates) {
      SS map = zipIt(np.head, s);
      if (map != null) {
        try {
          O result = np.body.get(mapValues tok_deRoundBracket(map), env);
          if (debugNativeCalls)
            print("Native predicate result: " + np.head + " => " + result);
          if (result instanceof Map && nempty(map)) {
            result = mapKeys((SS) result, var -> lookupOrKeep(map, var));
            if (debugNativeCalls)
              print("Rewrote native predicate result: " + result);
          }
          try object result;
        } catch e { handleException(e); }
      } else
        if (printNonMatches)
          print("Non-match: " + quote(np.head) + " / " + quote(s));
    }
    null;
  }

  // returns false if unknown
  bool checkCondition(O o) {
    ret isTrue(checkConditionOpt(o));
  }
  
  // returns null if unknown
  Bool checkConditionOpt(O o) {
    if (o cast S) {
      if (contains(facts, o)) true;
      try object Bool b = checkNativeCondition(o);
    }
    //print("Ignoring condition: " + o);
    null;
  }
  
  Bool checkNativeCondition(S o) {
    O result = runNativePredicate(o, new Env);
    result = unpackWithAlternativeOrIterator(result);
    if (result cast Bool) ret result;
    if (result instanceof Map) true; // TODO
    null;
  }

  !include #1025614 // parsePythonesqueProcedure

  Proc parseProcedure(S s) {
    ret parsePythonesqueProcedure(s);
  }

  O splitAtAmpersand2(S s) {
    LS l = tok_splitAtAmpersand(s);
    if (l(l) == 1) ret s;
    ret new And(first(l), splitAtAmpersand2(join(" & ", dropFirst(l))));
  }

  // "zip" a condition with a fact (match word-by-word)
  SS zipIt(S cond, S fact) {
    SS map = zipIt_keepBrackets(cond, fact);
    if (map == null) null; // no match
    map = mapValues tok_deRoundOrCurlyBracket(map);
    // handle special case, e.g. "i am x", "i am (x)"
    removeFromMapWhere(map, (k, v) -> eqic(k, v));
    ret map;
  }
  
  SS zipIt_deBracket(S pat, S s) {
    SS map = zipIt(pat, s);
    ret map == null ? null : mapValues tok_deRoundOrCurlyBracket(map);
  }

  // "zip" a condition with a fact (match word-by-word)
  SS zipIt_keepBrackets(S cond, S fact) {
    SS map = gazelle_deepZip_keepBrackets(cond, fact);
    if (map == null) null; // no match
    if (!all(keys(map), s -> isVar(s))) null; /*with print("Non-variable changes, exiting")*/;
    ret map;
  }

  bool isVar(S s) {
    ret s != null &&
      (vars.contains(s) || s.startsWith("var_") || isDollarVar(s));
  }

  O replaceVars(O o, SS map) {
    if (empty(map)) ret o;
    ret transform(x -> replaceVars_base(x, map), o);
  }
  
  O replaceVars_base(O o, SS map) {
    if (o cast S)
      ret replaceCodeTokensUsingMap(o, map);
    null;
  }
  
  S format(S s, SS map) {
    ret replaceCodeTokensUsingMap(s, mapValues optRound(map));
  }
  
  // if f returns null, go through structure
  O transform(IF1 f, O o) {
    ret transform_understandsTransformableAndList(f, o);
  }

  void applyLogicRuleToFact(LogicRule rule, S fact) {
    O lhs = rule.lhs, rhs = rule.rhs;
    O cond, remaining = null;
    if lhs is And(O a, O b) {
      cond = a;
      remaining = b;
    } else
      cond = lhs;
    
    // now we match the condition with the fact
    SS map = zipIt_keepBrackets((S) cond, fact);
    if (map == null) {
      if (printNonMatches)
        print("Non-match: " + quote(cond) + " / " + quote(fact));
      ret; // no match
    }

    // Now we have a proper mapping with the keys being variables!
    if (verbose) print("Match: " + quote(cond) + " / " + quote(fact));

    // drop round brackets
    // XXX? map = mapValues tok_deRoundBracket(map);

    // Apply mapping to right hand side
    O rhs_replaced = replaceVars(rhs, map);
    if (verbose) print(+rhs_replaced);
    
    Map trail = litorderedmap(op := "applyLogicRuleToFact",
      +rule, +fact, +rhs_replaced, +remaining);

    if (remaining == null) {
      // No more conditions. Add as fact / new rule
      addRewrittenRHS(rhs_replaced, trail);
    } else {
      // Apply mapping to remaining condition
      O remaining_replaced = replaceVars(remaining, map);
      trail.put(+remaining_replaced);
      addLogicRuleWithTrail(new LogicRule(remaining_replaced, rhs_replaced), trail);
    }
  }
  
  run { think(); }

  !include #1025615 // smartParser1
  
  void parseProgram {
    if (programLoaded) ret;
    set programLoaded;
    loadProgram(program);
  }
  
  void loadProgram(S program) {
    set parsing;
    try {
      smartParser1(program);
    } finally {
      parsing = false;
    }
  }

  bool doSomeLogic() {
    bool anyAction;
    Pair<LogicRule, S> p;
    while not null (p = rulesOnFacts.next()) {
      ping();
      set anyAction;
      //print("Combination: " + p);
      applyLogicRuleToFact(p.a, p.b);
    }
    Pair<CodeFragment, S> p2;
    while not null (p2 = codeOnFacts.next()) {
      ping();
      set anyAction;
      //print("Combination: " + p2);
      applyCodeFragmentToFact(p2.a, p2.b);
    }
    Pair<IVF1<S>, S> p3;
    while not null (p3 = anyCodeOnFacts.next()) {
      ping();
      set anyAction;
      //print("Combination: " + p3);
      pcallF(p3.a, p3.b);
    }
    Pair<IVF1<LogicRule>, LogicRule> p4;
    while not null (p4 = anyCodeOnRules.next()) {
      ping();
      set anyAction;
      pcallF(p4.a, p4.b);
    }
    ret anyAction;
  }

  void applyCodeFragmentToFact(CodeFragment cf, S fact) {
    SS map = cf.keepBrackets ? zipIt_keepBrackets(cf.head, fact) : zipIt(cf.head, fact);
    if (map != null)
      cf.body.get(mapValues tok_deRoundBracket(map), new Env);
  }
  
  // indicator for end of thought process (when this stays stable)
  long size() {
    ret l(logicRules) + l(facts) + proceduresExecuted;
  }

  void think {
    parseProgram();
    
    set thoughtBegun;
    
    int round = 0;
 
    while ping (round++ < maxRounds) {
      long lastSize = size();
      if (verbose) print("Logic round " + round + ", size: " + lastSize);
      while (doSomeLogic() && round++ < maxRounds && l(facts) < maxFacts) {}

      for ping (Proc proc : getAndClearList(proceduresToRun))
        runParsedProcedure(proc);
        
      callFAll(extraLogicOperations);
        
      if (size() == lastSize) {
        if (verbose) print("No changes, exiting");
        break;
      }
    }

    // We're done logicking, so print all the facts gathered

    Cl<S> madeFacts = factsDeduced();
    if (printFactsAfterThinking)
      pnlWithHeading("Facts I deduced", madeFacts);

    // Print say () and print () separately

    new LS output;
    for (S fact : madeFacts) {
      LS tok = mainTokenize(fact);
      if (countCodeTokens(tok) == 2 && eqicOneOf(getCodeToken(tok, 0), "print", "say"))
        // For the user, we print without all the round brackets
        output.add(tok_dropRoundBrackets(getCodeToken(tok, 1)));
    }
    
    pnlWithHeadingIfNempty("Bot Output", output);
  }

  void addNativePredicate(S head, IF0 body) {
    nativePredicates.add(new NativePredicate(head, (map, env) -> body!));
  }
  
  void addNativePredicate(S head, IF1<SS, O> body) {
    nativePredicates.add(new NativePredicate(head, (map, env) -> body.get(map)));
  }

  void addNativePredicate(S head, IF2<SS, Env, NPRet> body) {
    nativePredicates.add(new NativePredicate(head, body));
  }

  // when you only need one result
  O unpackWithAlternativeOrIterator(O result) {
    if (result instanceof Iterator) ret first((Iterator) result);
    if (result instanceof WithAlternative) ret ((WithAlternative) result).result;
    ret result;
  }

  void onFactDo(S head, IVF2<SS, Env> body) {
    codeOnFacts.newA(new CodeFragment(head, body));
  }

  void onFactDo_keepBrackets(S head, IVF2<SS, Env> body) {
    codeOnFacts.newA(new CodeFragment(head, body, true));
  }
  
  LS filterByPattern(S pat, Iterable<S> items) {
    ret filter(items, i -> zipIt(pat, i) != null);
  }

  // pat = pattern with variables
  // results are mappings with debracketed values
  L<SS> matchFacts(S pat) {
    ret matchStrings(pat, facts);
  }
  
  SS matchString(S pat, S input) {
    ret zipIt_deBracket(pat, input);
  }
  
  L<SS> matchStrings(S pat, Iterable<S> items) {
    new L<SS> out;
    for (S s : items) {
      SS map = zipIt_deBracket(pat, s);
      if (map != null)
        out.add(map);
    }
    ret out;
  }
  
  LPair<S, SS> matchFacts2(S pat) {
    ret matchStrings2(pat, facts);
  }
  
  // returns items too
  LPair<S, SS> matchStrings2(S pat, Iterable<S> items) {
    new LPair<S, SS> out;
    for (S s : items) {
      SS map = zipIt_deBracket(pat, s);
      if (map != null)
        out.add(pair(s, map));
    }
    ret out;
  }
  
  LS matchFacts(S var, S pat) {
    ret map(matchFacts(pat), map -> map.get(var));
  }
  
  // pat = pattern with variables
  // results are mappings with debracketed values
  L<SS> matchFacts_keepBrackets(S pat) {
    new L<SS> out;
    for (S fact : facts) {
      SS map = zipIt_keepBrackets(pat, fact);
      if (map != null)
        out.add(map);
    }
    ret out;
  }

  void openAllTheories {  
    for (SS map : matchFacts_keepBrackets("theory $x $y"))
      openTheory(tok_deRoundOrCurlyBracket(map.get("$x")), map.get("$y"));
  }
  
  void openTheory(S name) {
    for (SS map : matchFacts_keepBrackets("theory $x $y"))
      if (eqic(properUnquote(tok_deRoundBracket($x(map))), name))
        ret with openTheory(name, $y(map));
    fail("Theory not defined: " + quote(name));
  }

  void openTheory(S name, S body) {
    //print("Raw theory: " + quote(s));
    loadProgram(withoutLeadingLinesEmptyAfterTrim_autoUnindent(tok_deRoundOrCurlyBracket_keepFirstSpacing(body)));
    if (verbose) print("Opened theory " + name);
  }
  
  void autoOpenTheories {
    onFactDo_keepBrackets("theory $x $y", (map, env) -> openTheory(tok_deRoundOrCurlyBracket(map.get("$x")), map.get("$y")));
  }
  
  // returns number of expectations checked
  int checkExpectations() {
    int n = 0;
    // check if all expect (...) facts are met
    for (SS map : matchFacts("expect $x")) {
      assertContains(facts, firstValue(map));
      ++n;
    }
    // check if all don't expect (...) facts are met
    for (SS map : matchFacts("don't expect $x")) {
      assertDoesntContain(facts, firstValue(map));
      ++n;
    }
    ret n;
  }
  
  void standardImports() {
    if (standardImportsLoaded) ret;
    set standardImportsLoaded;
    registerImport("math", () -> philosophyBot1_math(this));
    registerImport("bool", () -> philosophyBot1_bool(this));
    registerImport("or", () -> philosophyBot1_orHandler(this));
    registerImport("iota", () -> philosophyBot1_iotaHandler(this));
    registerImport("tlft_honoringBrackets", () -> 
      addNativePredicate("tlft_honoringBrackets $x",
        map -> printIf(verbose, "tlft output",
          tlft_honoringBrackets($x(map)))));
    addNativePredicate("printNonMatches", () -> { printNonMatches = true; true; });

    philosophyBot1_enableAddSimplifier_withTrails(this);
  }
  
  void addFactPreprocessor(IPred<S> f) {
    factPreprocessors.add(f);
  }
      
  void addLogicRulePreprocessor(IPred<LogicRule> f) {
    logicRulePreprocessors.add(f);
  }
  
  void registerImport(S name, Runnable handler) {
    S line = "import " + name;
    factPreprocessors.add(s -> {
      if (eqic(s, line)) {
        if (verbose) print("Importing " + name);
        handler.run();
        true;
      }
      false;
    });
  }
  
  bool hasFact(S fact) {
    ret contains(facts, fact);
  }
  
  bool hasContradiction() { ret hasFact("contradiction"); }
  
  LS mainTokenize(S s) {
    ret javaTokWithBrackets(s);
  }
  
  // sanitize untrusted input - overly safe version
  S sanitizeInput(S s) {
    ret joinWithSpace(antiFilter(words2_plusApostrophe(s), w -> isVar(w)));
  }
  
  void deleteFacts(Iterable<S> l) {
    Set<S> set = asCISet(l);
    facts = filterCISet(facts, f -> !contains(set, f));
  }
  
  Cl<S> factsDeduced() {
    ret listMinusList(facts, originalFacts);
  }
  
  Cl<S> deducedFacts() {
    ret factsDeduced();
  }
  
  Cl<S> factsDeducedAfterThought() {
    think();
    ret deducedFacts();
  }

  
  bool containsDollarVars(O o) {
    // abuse transform function
    new Flag flag;
    withCancelPoint(cp -> {
      transform(x -> {
        if (x cast S) {
          if (main containsDollarVars(x)) {
            flag.raise();
            cancelTo(cp);
          }
          ret x;
        }
        null;
      }, o);
    });
    ret flag!;
  }
  
  L<LogicRule> allLogicRulesWithoutLHSVars() {
    ret filter(logicRules, r -> !containsDollarVars(leftmostCondition(r.lhs)));
  }
  
  O leftmostCondition(O o) {
    while (o instanceof And) o = ((And) o).a;
    ret o;
  }
  
  void _standardHandlers {
    philosophyBot_autoOpenTheoriesHandler(this);
    addFactPreprocessor(s -> { if (eqic(s, "standard imports")) ret true with standardImports(); false; });
  }
  
  void runAndCheckExpectations {
    run();
    checkExpectations();
  }
  
  void addDeepTransformer(IF1<S> transformer) {
    if (deepTransformers == null) {
      deepTransformers = new L;
      // enable transformers
      anyCodeOnFacts.newA(fact ->
        addFactWithTrail(gazelle_deepTransform(
          s -> firstTransformersResult(deepTransformers, s), fact),
          trails == null ? null : new TTransformed(fact, transformer)));
    }
    deepTransformers.add(transformer);
  }
  
  void addTrailEnabledDeepTransformer(IF1<S, WithTrail<S>> transformer) {
    if (trailEnabledDeepTransformers == null) {
      trailEnabledDeepTransformers = new L;
      // enable transformers
      anyCodeOnFacts.newA(fact -> {
        WithTrail<S> simplified = gazelle_deepTransform_withTrail(
          s -> firstTransformersResult_trailEnabled(trailEnabledDeepTransformers, s), fact);
        if (simplified == null) ret;
        addFactWithTrail(simplified);
        if (noteSimplificationsAsFacts)
          addFact(format("$x simplifies $y", litmap($x := fact, $y := simplified!)));
      });
    }
    trailEnabledDeepTransformers.add(transformer);
  }
  
  O getExtension(O key) { ret mapGet(extensions, key); }
  
  void addExtension(O key, O value) {
    if (extensions == null) extensions = new Map;
    extensions.put(key, value);
  }
  
  void enableTrails() { if (trails == null) trails = ciMap(); }
  
  O getTrail(S fact) { ret mapGet(trails, fact); }
  
  // get trail for arbitrary object (fact/rule)
  O getTrail(O o) {
    if (o cast LogicRule) ret o.trail;
    if (o cast S)
      ret mapGet(trails, o);
    null;
  }
  
  void printDeducedFactsWithTrails() {
    printAsciiHeading("Deduced facts with trails");
    for (S fact : factsDeduced()) {
      print(fact);
      printUnlessNull("  << ", getTrail(fact));
    }
  }
  
  L<WithTrail<S>> deducedFactsWithTrails() {
    ret map(factsDeduced(), s -> WithTrail(getTrail(s), s));
  }
  
  void setTrailForAllLogicRules(O trail) {
    for (LogicRule r : logicRules)
      r.trail = trail;
  }
  
  L<LogicRule> logicRules() {
    ret cloneList(logicRules);
  }
  
  Pair<Set<LogicRule>, Set<S>> rulesAndFactsUsedForMaking(O factOrLogicRule) {
    Set l = thingsUsedForMaking(factOrLogicRule);
    ret pair(instancesOfAsSet LogicRule(l), setIntersection(asCISet(stringsOnly(l)), facts));
  }
  
  Set thingsUsedForMaking(O factOrLogicRule) {
    ret philosophyBot1_visitTrailsTree_gen(this, null, factOrLogicRule);
  }
  
  void addExtraLogicOperation(Runnable r) {
    extraLogicOperations.add(r);
  }
  
  void addCodeOnFact(IVF1<S> f) {
    anyCodeOnFacts.newA(f);
  }
  
  void updateCodeOnFact(IVF1<S> f) {
    anyCodeOnFacts.updateA(f);
  }
  
  void addCodeOnRule(IVF1<LogicRule> f) {
    anyCodeOnRules.newA(f);
  }
  
  /*void updateCodeOnRule(IVF1<LogicRule> f) {
    anyCodeOnRules.updateA(f);
  }*/
  
  void handleException(Throwable e) {
    print("BOT", e);
  }
}