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

  }

}