!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; }