sclass PhilosophyBot1 {

  srecord LogicRule(lhs, rhs) {}

  srecord And(a, b) {}

  srecord If(condition, thenBlock, elseBlock) {}

  srecord For(var, condition, body) {}

  srecord While(condition, body) {}

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

  // body takes variable mapping

  // body can return

  //   Bool => immediate result (ok or fail)

  //   SS   => variable mapping

  //   null => not applicable

  srecord NativePredicate(S head, IF1<SS, NPRet> body) {}

  srecord WithAlternative(IF0<O> alternative, O result) {}

  replace Proc with L. // procedures are a list of statements

  sclass Path {

    new L<Step> steps;

    bool valid = true;

    toString { ret stdToString(this); }

  }

  abstract sclass Step {

    abstract NPRet alternative(); // perform one backtracking step

    //undo();

  }

  srecord ProcedureToRun(Proc proc, Path path) {

    ProcedureToRun(Proc proc) { this.proc = proc; path = new Path; }

  }

  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 L<ProcedureToRun> proceduresToRun;

 // parsed procedures

  transient long proceduresExecuted;

  transient new L<NativePredicate> nativePredicates;

  transient bool debugNativeCalls = true, debugAllCmds = true;

  transient new L onProcedureEnded;

  transient Set<S> vars = litciset("x", "y", "z");

  void addLogicRule(LogicRule rule) {

    if (logicRules.add(rule)) {

      print("Got logic rule", rule);

      rulesOnFacts.newA(rule); // to combine it with the facts

    }

  }

  void addFact(S fact) {

    fact = trim(fact);

    if (empty(fact)) ret;

    fact = tok_deRoundBracket(fact);

    // Check if it's a procedure

    LS tok = javaTokWithBrackets(fact);

    if (countCodeTokens(tok) == 2 && eqic(getCodeToken(tok, 0), "proc")

      && isCurlyBracketed(getCodeToken(tok, 1))) pcall {

        // It's a procedure!

        S proc = uncurly_keepSpaces(getCodeToken(tok, 1));

        if (proceduresToRun.add(new ProcedureToRun(parseProcedure(proc)))) {

          print("Got procedure:");

          print(indentx("> ", proc));

        }

      }

    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

      }

  }

  void runProcedure(S proc) pcall {

    print("Running procedure.");

    runParsedProcedure(parseProcedure(proc), new Path);

  }

  // path contains the previously executed steps with an option to backtrack

  void runParsedProcedure(Proc commands, Path path) {

    ++proceduresExecuted;

    L remainingCommands = cloneLinkedList(commands);

    O cmd;

    while not null (cmd = popFirst(remainingCommands)) {

      if (cmd cast L) continue with runParsedProcedure(cmd, path);

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

      } 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

        // TODO: path handling

        addLogicRule(new LogicRule(condition, "proc {\n" + body + "\n}"));

      } else if cmd is While(O condition, O body) {

        bool b = checkCondition(condition);

        if (!b) ret;

        proceduresToRun.add(new ProcedureToRun(ll(body, cmd), path));

      } else if (cmd cast S) {

        O result = runNativePredicate(cmd);

        if (result != null) {

          if (result instanceof WithAlternative) {

            print("Have alternative");

            IF0<NPRet> f = ((WithAlternative) result).alternative;

            S _cmd = cmd;

            path.steps.add(new Step {

              NPRet alternative() {

                ret f!;

              }

              toString { ret _cmd; }

            });

            result = ((WithAlternative) result).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, path); // notify listeners

  }

  // return var mapping (SS), Bool or null for no matching predicate

  O runNativePredicate(S s) {

    for (NativePredicate np : nativePredicates) {

      SS map = zipIt(np.head, s);

      if (map != null) {

        O result = np.body.get(mapValues tok_deRoundBracket(map));

        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;

      }

    }

    null;

  }

  bool checkCondition(O o) {

    if (o cast S) {

      if (contains(facts, o)) true;

      O result = runNativePredicate(o);

      if (result cast Bool) ret result;

      if (result instanceof Map) true; // TODO

    }

    print("Ignoring condition: " + o);

    false;

  }

  Proc parseProcedure(S proc) {

    //printStruct(proc);

    proc = withoutLinesEmptyAfterTrim(proc);

    //printStruct(proc);

    proc = autoUnindent(proc);

    //printStruct(proc);

    print(indentx("> ", proc));

    LS l = groupPythonStyleIndents_honoringBrackets(proc);

    pnl("unpythonized ", l);

    new L out;

    for i over l: {

      S s = l.get(i);

      LS tok = javaTokWithBrackets(s);

      if (eqic(firstCodeToken(tok), "if")) {

        assertEquals(s, ":", getCodeToken(tok, 2));

        out.add(new If(deRoundBracket(getCodeToken(tok, 1)),

          parseProcedure(joinSubList(tok, 3*2)), null));

      } else if (eqic(firstCodeToken(tok), "while")) {

        assertEquals(s, ":", getCodeToken(tok, 2));

        out.add(new While(deRoundBracket(getCodeToken(tok, 1)),

          parseProcedure(joinSubList(tok, 3*2))));

      } else if (eqic(firstCodeToken(tok), "else")) {

        O last = last(out);

        if (!last instanceof If) fail("Else without if");

        assertEquals(s, ":", getCodeToken(tok, 1));

        ((If) last).elseBlock = joinSubList(tok, 2*2);

      } else if (eqic(firstCodeToken(tok), "for")) {

        assertEquals(s, ":", getCodeToken(tok, 2));

        S cond = getCodeToken(tok, 1);

        // cond looks like: "(y | x has a y)"

        cond = deRoundBracket(cond);

        LS tok2 = javaTok(cond);

        assertEquals(cond, "|", getCodeToken(tok2, 1));

        S var = assertIdentifier(cond, getCodeToken(tok2, 0));

        S actualCondition = trimJoinSubList(tok2, 2*2+1);

        out.add(new For(var, actualCondition, parseProcedure(joinSubList(tok, 3*2))));

      } else

        out.add(s);

    }

    pnl("Parsed procedure ", out);

    ret out;

  }

  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 = gazelle_zip(cond, fact);

    if (map == null) null; // no match

    print("gazelle zip => " + map);

    // are only variables changed?

    if (!allKeysAreInSet(map, vars))

      null; /*with print("Non-variable changes, exiting")*/;

    ret map;

  }

  O replaceVars(O o, SS map) {

    if (empty(map)) ret o;

    // TODO: non-string cases

    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((S) cond, fact);

    if (map == null) ret; // no match

    // Now we have a proper mapping with the keys being variables!

    print("Match.");

    // drop round brackets

    // XXX? map = mapValues tok_deRoundBracket(map);

    // Apply mapping to right hand side

    S rhs_replaced = cast replaceVars(rhs, map);

    print(+rhs_replaced);

    if (remaining == null) {

      // Add as fact

      addFact(rhs_replaced);

    } else {

      // Apply mapping to remaning condition

      S remaining_replaced = cast replaceVars(remaining, map);

      addLogicRule(new LogicRule(remaining_replaced, rhs_replaced));

    }

  }

  run {

    parseProgram();

    think();

  }

  void parseProgram {

    // split into paragraphs and unindent

    LS paragraphs = map autoUnindent(map rtrim(splitAtEmptyLines(program)));

    print("Got " + n2(paragraphs, "parapraph"));

    // print the parapraphs

    print(joinWithEmptyLines(map(s -> indentx("> ", s), paragraphs)));

    // throw away comment-only and quoted paragraphs (assume it's a title)

    LS paragraphs2 = antiFilter(paragraphs, s -> 

      isSingleLine(trim(s)) && isQuoted(trim(s)) || countJavaTokens(s) == 0

      || endsWith(rtrim(s), "----"));

    print("Got " + n2(paragraphs2, "filtered paragraph"));

    print(joinWithEmptyLines(map(s -> indentx("> ", s), paragraphs2)));

    // find fact paragraphs

    print(map allLinesAreUnindented(paragraphs2));

    Pair<LS> p1 = filterAntiFilter(s ->

      !isSingleLine(trim(s)) && allLinesAreUnindented(s), paragraphs2);

    LS multiFactParagraphs = p1.a, paragraphs3 = p1.b;

    for (S para : multiFactParagraphs)

      for (S s : tlft(para))

        addFact(s);

    // find logic rules

    new LS paragraphs4;

    for (S para : paragraphs3) {

      PairS p = splitAtDoubleArrow_pair(para);

      if (p == null) continue with paragraphs4.add(para);

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

    }

    pnlStruct("Unparsed - assuming facts", paragraphs4);

    // assume the unparsed stuff consists of facts

    for (S para : paragraphs4)

      addFact(para);

    originalFacts = cloneSet(facts);

  }

  bool doSomeLogic() {

    bool anyAction;

    Pair<LogicRule, S> p;

    while not null (p = rulesOnFacts.next()) {

      set anyAction;

      //print("Combination: " + p);

      applyLogicRuleToFact(p.a, p.b);

    }

    ret anyAction;

  }

  // indicator for end of thought process (when this stays stable)

  long size() {

    ret l(logicRules) + l(facts) + proceduresExecuted;

  }

  void think {

    int round = 0;

    while (round++ < maxRounds) {

      long lastSize = size();

      print("Logic round " + round + ", size: " + lastSize);

      while (doSomeLogic() && round++ < maxRounds) {}

      for (ProcedureToRun proc : getAndClearList(proceduresToRun))

        runParsedProcedure(proc.proc, proc.path);

      if (size() == lastSize) {

        print("No changes, exiting");

        break;

      }

    }

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

    LS factsToPrint = listMinusList(facts, originalFacts);

    pnlWithHeading("Facts I deduced", factsToPrint);

    // Print the actual output

    new LS output;

    for (S fact : factsToPrint) {

      LS tok = javaTokWithBrackets(fact);

      if (countCodeTokens(tok) == 2 && eqic(getCodeToken(tok, 0), "print"))

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

  }

  void addNativePredicate(S head, IF1<SS, O> body) {

    nativePredicates.add(new NativePredicate(head, body));

  }

  // for backtracking in native predicates

  WithAlternative withAlternative(IF0<O> alternative, O result) {

    ret new WithAlternative(alternative, result);

  }

}