srecord DollarVarPattern(S pat) {}
srecord Definition(O lhs, O rhs) {}
srecord Input(S s) {}
srecord Statement(S s) {}
srecord ProposeRewrite(S a, S b) {}

sclass ThoughtSpace1 {
  new LinkedHashSet objects;
  int initialObjects;
  static bool printStats;
  new L<VF1<ThoughtSpace1>> steppers;
  new Set<Class> lookingFor;
  
  void think(bool print) {
    initialObjects = l(objects);
    long startTime = now();
    int n = -1;
    while (l(objects) > n) {
      n = l(objects);
      
      // def + def -> patterned def [emerge pattern]
      L<Definition> defs = instancesOf(Definition);
      for (Definition a : defs)
        for (Definition b : defs)
          if (a.lhs instanceof S && b.lhs instanceof S) {
            S pat = combineToDollarVarPattern((S) a.lhs, (S) b.lhs);
            if (containsDollarVars(pat))
              objects.add(DollarVarPattern(pat));
          }
          
      // pattern + def -> patterned def [generalize]
      for (DollarVarPattern pat : instancesOf(DollarVarPattern)) {
        for (Definition a : defs) if (a.lhs instanceof S) {
          SS match = matchDollarVarsIC(pat.pat, (S) a.lhs);
          if (match != null)
            generalizeDefinition(a, match);
        }
      }
      
      // input + patterned def -> def       [specialize]
      // input + patterned def -> statement [implication]
      for (Input i : instancesOf(Input))
        for (Definition a : defs) if (a.lhs instanceof DollarVarPattern) {
          SS match = matchDollarVarsIC(((DollarVarPattern) a.lhs).pat, i.s);
          new Matches m;
          if (match != null) {
            S rhs = ((DollarVarPattern) a.rhs).pat;
            if (swic_trim(rhs, "[implies]", m))
              objects.add(Statement(transformEachTokenUsingMap(m.rest(), match)));
            else
              specializeDefinition(a, match);
          }
        }
        
      for (VF1<ThoughtSpace1> stepper : concurrentlyIterateList(steppers))
        callF(stepper, this);
    }
    long time = now()-startTime;
    
    if (print)
      pnlStruct(dropFirst(initialObjects, asList(objects)));
      
    if (printStats)
    print("\n" + n2(l(objects)-initialObjects, "rewrite") + " in " + (now()-startTime) + " ms");
  }
  
  void generalizeDefinition(Definition def, SS match) {
    SS rev = reverseCIMap(match);
    S lhs = transformEachTokenUsingMap((S) def.lhs, rev);
    S rhs = transformEachTokenUsingMap((S) def.rhs, rev);
    addIfNotNull(objects, Definition(DollarVarPattern(lhs), DollarVarPattern(rhs)));
  }
  
  void specializeDefinition(Definition def, SS match) {
    S lhs = transformEachTokenUsingMap(((DollarVarPattern) def.lhs).pat, match);
    S rhs = transformEachTokenUsingMap(((DollarVarPattern) def.rhs).pat, match);
    addIfNotNull(objects, Definition(lhs, rhs));
  }
  
  void addDefinitions(S defs) {
    for (S s : tlft(defs)) {
      L<S> l = splitAtJavaToken(s, "=");
      objects.add(Definition(first(l), second(l)));
    }
  }
  
  void printDefinitionsForInput() {
    final Input in = firstInstanceOf(Input, objects);
    if (in != null) {
      L<Definition> definitions = definitionsForInput(in);
      print("Got " + n2(definitions, "definition") + " for input " + quote(in.s) + (empty(definitions) ? "." : ":"));
      printStructLinesIndent(definitions);
    }
  }
  
  Input input() {
    ret firstInstanceOf(Input, objects);
  }
  
  S getInput() {
    Input i = input();
    ret i == null ? null : i.s;
  }
  
  L<Definition> definitionsForInput() { ret definitionsForInput(input()); }
  
  L<Definition> definitionsForInput(final Input in) {
    ret [Definition d : instancesOf(Definition) | eqic_gen(d.lhs, in.s)];
  }
  
  L<S> getDefinitionTexts(fS s) {
    new L<S> l;
    for (Definition d : instancesOf(Definition))
      if (eqic_gen(d.lhs, s))
        l.add((S) d.rhs);
    ret l;
  }
  
  L<Definition> literalDefinitions() {
    ret [Definition d : instancesOf(Definition) | d.lhs instanceof S && d.rhs instanceof S];
  }
  
  L<Statement> statements() {
    ret instancesOf(Statement);
  }
  
  void removeInitialObjects {
    replaceCollection(objects, dropFirst(initialObjects, asList(objects)));
    initialObjects = 0;
  }
  
  <A> L<A> instancesOf(Class<A> c) {
    ret main.instancesOf(c, objects);
  }
  
  void removeObjectsOfType(Class type) {
    removeAll(objects, instancesOf(type));
  }
  
  void setInput(S s) {
    removeObjectsOfType(Input);
    objects.add(Input(s));
  }
  
  void add(O o) { objects.add(o); }
  
  void addStepper(VF1<ThoughtSpace1> s) { steppers.add(s); }
  
  bool found() {
    ret containsExactInstanceOfAny(objects, lookingFor);
  }
}