!7

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

sS defs = [[
A cup of water = A cup with water inside
A cup of Peter = A cup that belongs to Peter
A cup of glass = A cup that consists of glass
A cup of style = A cup that has a lot of style
a $a with $b inside       = [implies] $b is smaller than a $a
a $a that belongs to $b   = [implies] $b is a person
a $a that consists of $b  = [implies] $b is a material
a $a that has a lot of $b = [implies] $b is a property
]];

p-exp {
  new ThoughtSpace ts;
  ts.objects.add(Input("a cup of joe"));
  
  ts.addDefinitions(defs);
  ts.think(false);
  //ts.printDefinitionsForInput();
  
  for (Definition d : ts.definitionsForInput()) {
    print("\nTrying definition " + sfu(d));
    new ThoughtSpace ts2;
    ts2.objects.add(Input((S) d.rhs));
    ts2.addDefinitions(defs);
    ts2.think(false);
    ts2.removeInitialObjects();
    
    //pnlStruct(ts2.literalDefinitions());
    pnlStruct(ts2.statements());
  }
}

sclass ThoughtSpace {
  new LinkedHashSet objects;
  int initialObjects;
  
  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, objects);
      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, objects)) {
        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, objects))
        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);
          }
        }
    }
    long time = now()-startTime;
    
    if (print)
      pnlStruct(dropFirst(initialObjects, asList(objects)));
    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);
  }
  
  L<Definition> definitionsForInput() { ret definitionsForInput(input()); }
  
  L<Definition> definitionsForInput(final Input in) {
    ret [Definition d : instancesOf(Definition, objects) | eqic_gen(d.lhs, in.s)];
  }
  
  L<Definition> literalDefinitions() {
    ret [Definition d : instancesOf(Definition, objects) | d.lhs instanceof S && d.rhs instanceof S];
  }
  
  L<Statement> statements() {
    ret instancesOf(Statement, objects);
  }
  
  void removeInitialObjects {
    replaceCollection(objects, dropFirst(initialObjects, asList(objects)));
    initialObjects = 0;
  }
}

Began life as a copy of #1017020