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