sclass PhilosophyBot1 {

  static transformable record LogicRule(lhs, rhs) {

    int n; // when added

    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 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

  transient S program;

  transient bool programLoaded;

  transient int maxRounds = 1000;

  transient int maxFacts = 1000;

  transient Set<S> facts = linkedCISet();

  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 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 bool verbose = true;

  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;

  // 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;

  Map extensions;

  *() {

    // find contradictions

    anyCodeOnFacts.newA(fact -> {

      Bool b = checkNativeCondition(fact);

      if (debugContradictionChecks)

        print("Fact check: " + b + " - " + fact);

      if (isFalse(b))

        addFact("contradiction");

    });

    _standardHandlers();

  }

  *(S *program) { this(); }

  void addRule(S s) {

    PairS p = splitAtFirstDoubleArrow(javaTokWithBrackets(s));

    if (p == null) if (verbose) print("addRule failed: " + s);

    addLogicRule(new LogicRule(splitAtAmpersand2(p.a), p.b));

  }

  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)

        rule = new LogicRule(a, new LogicRule(b, rule.rhs));

      else break;

    }

    ret rule;

  }

  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;

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

    if (syncAdd(logicRules, rule)) {

      if (verbose) print("Got logic rule", rule);

      pcallFAll(onLogicRuleAdded, 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) {

    ping();

    fact = trim(fact);

    if (empty(fact)) ret;

    if (l(facts) >= maxFacts) 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))) {

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

      }

  }

  void addRewrittenRHS(O o) {

    if (o cast LogicRule)

      addLogicRule(o);

    else if o is And(O a, O b) {

      addRewrittenRHS(a);

      addRewrittenRHS(b);

    } else if (o != null)

      addFact((S) o);

  }

  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

        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) {

          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;

          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) {

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

  }

  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) {

    if (o == null) null;

    ping();

    try object f.get(o);

    if (o cast Transformable)

      ret o.transformUsing(x -> transform(f, x));

    if (o cast L)

      ret map(x -> transform(f, x), o);

    fail("Don't know how to transform: " + className(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);

    if (remaining == null) {

      // Add as fact / new rule

      addRewrittenRHS(rhs_replaced);

    } else {

      // Apply mapping to remaining condition

      O remaining_replaced = replaceVars(remaining, map);

      addLogicRule(new LogicRule(remaining_replaced, rhs_replaced));

    }

  }

  run { think(); }

  !include #1025615 // smartParser1

  void parseProgram {

    if (programLoaded) ret;

    set programLoaded;

    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 {

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

  }

  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 ->

        addFact(gazelle_deepTransform(

          s -> firstTransformersResult(deepTransformers, s), fact)));

    }

    deepTransformers.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);

  }

}