!7

/*
    Event 1 happens before event 2 :=
      vars {event 1, event 2, X, Y}
      Event 1 happens at day X.
      Event 2 happens at day Y.
      X < Y.

*/

sclass Obj {
  class Fact {}
  
  record Var(S name) { toString { ret name; } }
  
  record StatementsWithVars(Set<Var> vars, L<Fact> statements) {
    *(Fact... statements) {
      this.statements = asList(statements);
      collectVars();
    }
    
    void collectVars {
      vars = new Set;
      fOr (Fact f : statements)
        vars.addAll(print("Vars", findVars(f)));
    }
  }
  
  L scanObject(O o) {
    ret filter(nonStaticNonPrimitiveNonTransientFieldValues(o),
      v -> v != null && !v instanceof S && v != Obj.this);
  }
  
  L<Var> findVars(Fact statement) {
    Cl out = transitiveHullOfFunction(o -> scanObject(o), (O) statement);
    print(classNames(out));
    ret instancesOf Var(out);
  }
  
  bool matchIndividual(O a, O b, Map<Var, O> map) {
    if (a cast Var)
      ret strictPut(map, a, b);
    else
      ret eq(a, b);
  }
  
  Map<Var, O> matchFacts(Fact f1, Fact f2) {
    if (f1 == null || f2 == null) null;
    if (f1.getClass() != f2.getClass()) null;
    L<Field> fields = nonStaticNonTransientFieldObjects(f1);
    new Map<Var, O> map;
    for (Field f : fields)
      if (!matchIndividual(fieldGet(f, f1), fieldGet(f, f2), map))
        null;
    ret map;
  }
  
  void recSolve(L<Fact> statements, Map<Var, O> map, IVF1<Map<Var, O>> onSuccess) {
    if (empty(statements)) {
      print("No more statements to process");
      callF(onSuccess, map);
      ret;
    }
    
    Fact f1 = first(statements);
    for (Fact f2 : facts) {
      Map<Var, O> map2 = matchFacts(f1, f2);
      if (map2 != null) {
        Map<Var, O> map3 = mergeMapsStrictly(map, map2);
        if (map3 == null) continue; // can't merge
        print("Found match for statement: " + map2);
        print("Full map now: " + map3);
        recSolve(dropFirst_virtual(statements), map3, onSuccess);
      }
    }
  }
  
  record $HappensBefore$<A, B>(A event1, B event2) extends Fact {}
  record $HappensAtDay$<A, B>(A event, B y) extends Fact {}
  record $LessThan$<A, B>(A x, A y) extends Fact {}
  
  // Enrolling happens before graduation.
  // Enrolling happens at day 200.
  // Graduation happens at day 100. // Contradiction!
  
  L<Fact> facts = ll(
    new $HappensBefore$("enrolling", "graduation"),
    new $HappensAtDay$("enrolling", 200),
    new $HappensAtDay$("graduation", 100)
  );
  
  StatementsWithVars rule1($HappensBefore$ in) {
    O event1 = in.event1, event2 = in.event2;
    Var X = new Var("X"), Y = new Var("Y");
    ret print(new StatementsWithVars(
      new $HappensAtDay$(event1, X),
      new $HappensAtDay$(event2, Y),
      new $LessThan$(X, Y)
    ));
  }

  *() {
    pnlWithHeading("Facts", facts);
    for (Fact f : facts) {
      StatementsWithVars out = cast callOpt(this, 'rule1, f);
      if (out == null) continue;
      // Now we have a bunch of statements with possible variables.
      // Let's match them with the facts.
      recSolve(out.statements, null, map -> { print("Got: " + map); });
    }
  }
}

p-exp { new Obj; }