!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 implements IStatement {}
  replace Var with ValuelessVar.
  
  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 {}
  
  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<Var> findVars(O o) { ret ai_findVarObjects Var(o); }
  
  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> facts, 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);
    print("recSolve " + f1);
    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(facts, dropFirst_virtual(statements), map3, onSuccess);
      }
    }
    print("No more matches for: " + f1 + " with " + map);
  }
  
  // Enrolling happens before graduation.
  // Enrolling happens at day 200.
  // Graduation happens at day 100. // Contradiction!
  
  L<Fact> badFacts = ll(
    new $HappensBefore$("enrolling", "graduation"),
    new $HappensAtDay$("enrolling", 200),
    new $HappensAtDay$("graduation", 100)
  );
  
  L<Fact> okFacts = ll(
    new $HappensBefore$("enrolling", "graduation"),
    new $HappensAtDay$("enrolling", 100),
    new $HappensAtDay$("graduation", 200)
  );
  
  StatementsWithVars rule($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)
    ));
  }
  
  StatementsWithVars trueFalse(bool b) {
    ret b ? new StatementsWithVars : null;
  }
  
  StatementsWithVars rule($LessThan$ in) {
    print("Checking " + in);
    O x = in.x, y = in.y;
    if (x instanceof Number && y instanceof Number)
      ret trueFalse(print(in + " => ", cmp(x/Number, y/Number) < 0));
    null;
  }

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

p-exp { new Obj; }