sclass PhilosophyBot1 {
  srecord LogicRule(lhs, rhs) {}
  srecord And(a, b) {}
  srecord If(condition, thenBlock, elseBlock) {}
  srecord For(var, condition, body) {} // don't need var actually
  srecord ForIn(var, expr, body) {}
  srecord While(condition, body) {}

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

  // like a native predicate, but doesn't return anything
  srecord CodeFragment(S head, IVF2<SS, Env> body, bool keepBrackets) {
    CodeFragment(S head, IVF2<SS, Env> body) { this.head = head; this.body = body; }
  }

  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

  transient S program;
  transient int maxRounds = 1000;
  transient Set<S> facts = linkedCISet();
  transient Set<S> originalFacts;
  transient new LinkedHashSet<LogicRule> logicRules;
  transient new AllOnAll<LogicRule, S> rulesOnFacts;
  transient new AllOnAll<CodeFragment, S> codeOnFacts;
  transient new AllOnAll<IVF1<S>, S> anyCodeOnFacts;
  transient new L<ProcedureToRun> proceduresToRun;
 // parsed procedures
  transient long proceduresExecuted;
  transient new L<NativePredicate> nativePredicates;
  transient bool debugNativeCalls = true, debugAllCmds = true;
  transient new L onProcedureEnded;
  transient bool printNonMatches, debugContradictionChecks;
  transient bool standardImportsLoaded;
  
  // 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;

  transient Set<S> vars = litciset("x", "y", "z");
  
  *() {
    // find contradictions
    anyCodeOnFacts.newA(fact -> {
      Bool b = checkNativeCondition(fact);
      if (debugContradictionChecks)
        print("Fact check: " + b + " - " + fact);
      if (isFalse(b))
        addFact("contradiction");
    });
  }
  *(S *program) { this(); }

  void addLogicRule(LogicRule rule) {
    for (IPred<LogicRule> p : logicRulePreprocessors)
      if (p.get(rule)) ret; // has been preprocessed
      
    // 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))
      addFacts_possibleAnd(rule.rhs);

    if (logicRules.add(rule)) {
      print("Got logic rule", rule);
      rulesOnFacts.newA(rule); // to combine it with the facts
    }
  }
  
  void addFacts(Iterable<S> l) {
    fOr (S fact : l) addFact(fact);
  }

  void addFact(S fact) {
    fact = trim(fact);
    if (empty(fact)) ret;
    
    fact = tok_deRoundBracket(fact);
    
    for (IPred<S> p : factPreprocessors)
      if (p.get(fact)) ret; // 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))) {
          print("Got procedure:");
          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)) {
        print("Got fact: " + fact);
        rulesOnFacts.newB(fact); // to combine it with the rules
        codeOnFacts.newB(fact);
        anyCodeOnFacts.newB(fact);
      }
  }

  void addFacts_possibleAnd(O o) {
    if o is And(O a, O b) {
      addFacts_possibleAnd(a);
      addFacts_possibleAnd(b);
    } else if (o != null)
      addFact((S) o);
  }

  void runProcedure(S proc) pcall {
    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
        addLogicRule(new LogicRule(condition, "proc {\n" + body + "\n}"));
      } 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 ForIn(S var, S expr, O body) {
        // XXX
        O result = runNativePredicate(expr, new Env);
        if (!result instanceof Iterable) {
          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;
          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)));
          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) {
        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;
      } 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
    ret 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;
    // XXX: recurse through all structures
    if o is And(O a, O b)
      ret new And(replaceVars(a, map), replaceVars(b, map));
    if o is If(O condition, O thenBlock, O elseBlock)
      ret new If(replaceVars(condition, map), replaceVars(thenBlock, map), replaceVars(elseBlock, map));
    if o is For(S var, O condition, O body)
      ret new For(replaceVars(var, map), replaceVars(condition, map), replaceVars(body, map));
    if o is ForIn(O var, O expr, O body)
      ret new ForIn(replaceVars(var, map), replaceVars(expr, map), replaceVars(body, map));
    if o is LogicRule(O lhs, O rhs)
      ret new LogicRule(replaceVars(lhs, map), replaceVars(rhs, map));
    if (o cast L)
      ret map(x -> replaceVars(x, map), o);
    ret join(replaceCodeTokensUsingMap(javaTok((S) o), map));
  }

  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!
    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);
    print(+rhs_replaced);

    if (remaining == null) {
      // Add as fact
      addFacts_possibleAnd(rhs_replaced);
    } else {
      // Apply mapping to remaining condition
      O remaining_replaced = replaceVars(remaining, map);
      addLogicRule(new LogicRule(remaining_replaced, rhs_replaced));
    }
  }
  
  run {
    parseProgram();
    think();
  }

  !include #1025615 // smartParser1
  
  void parseProgram {
    loadProgram(program);
  }
  
  void loadProgram(S program) {
    smartParser1(program);
  }

  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);
    }
    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 {
    int round = 0;
 
    while ping (round++ < maxRounds) {
      long lastSize = size();
      print("Logic round " + round + ", size: " + lastSize);
      while (doSomeLogic() && round++ < maxRounds) {}

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

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

    LS madeFacts = listMinusList(facts, originalFacts);
    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)));
    }
    
    pnlWithHeading("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);
  }
  
  L<SS> matchStrings(S pat, Iterable<S> items) {
    new L<SS> out;
    for (S s : items) {
      SS map = zipIt(pat, s);
      if (map != null)
        out.add(mapValues tok_deRoundOrCurlyBracket(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, S body) {
    //print("Raw theory: " + quote(s));
    loadProgram(withoutLeadingLinesEmptyAfterTrim_autoUnindent(tok_deRoundOrCurlyBracket_keepFirstSpacing(body)));
    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 -> tlft_honoringBrackets($x(map))));
  }
  
  void registerImport(S name, Runnable handler) {
    S line = "import " + name;
    factPreprocessors.add(s -> {
      if (eqic(s, line)) {
        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)));
  }  
}