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)

  // like a native predicate, but doesn't return anything
  srecord CodeFragment(S head, IVF2<SS, Env> 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
  //   null => not applicable
  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 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");
  
  *() {}
  *(S *program) {}

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

  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(remainingCommands)) {
      if (cmd cast L) continue with runParsedProcedure(cmd);
      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) ret;
        whereToPostCode.add(ll(body, cmd));
      } 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
  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;
      }
    }
    null;
  }

  bool checkCondition(O o) {
    if (o cast S) {
      if (contains(facts, o)) true;
      O result = runNativePredicate(o, nu Env(wantAlternatives := false));
      result = unpackWithAlternativeOrIterator(result);
      if (result cast Bool) ret result;
      if (result instanceof Map) true; // TODO
    }
    print("Ignoring condition: " + o);
    false;
  }

  !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 = gazelle_zip(cond, fact);
    if (map == null) null; // no match
    print("gazelle zip => " + map);

    // are only variables changed?
    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;
    // 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();
  }

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

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

  void applyCodeFragmentToFact(CodeFragment cf, S fact) {
    SS map = 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 (round++ < maxRounds) {
      long lastSize = size();
      print("Logic round " + round + ", size: " + lastSize);
      while (doSomeLogic() && round++ < maxRounds) {}

      for (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 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, 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;
  }

  // pattern contains "x" and "y" etc.
  // we return a list of variable mappings
  L<SS> listFactsMatching(S pattern) {
    new L<SS> out;
    for ping (S fact : facts) {
      SS map = zipIt(pattern, fact);
      if (map != null)
        out.add(mapValues tok_deRoundBracket(map));
    }
    ret out;
  }

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