!752

// TODO: translator should accept this: "s/Rational/Rat" :-)

static S dataProgID = "#1002049"; // read/save data there

// Numeric quadruple
static class NQ {
  BigInteger a;
  S b;
  BigInteger c;
  S d;
  
  *() {}
  *(S a, S *b, S c, S *d) {
    this.a = smartBigint(a);
    this.c = smartBigint(c);
  }
  *(BigInteger *a, S *b, BigInteger *c, S *d) {}
  
  public boolean equals(O o) {
    ret stdEq(this, o, "a", "b", "c", "d");
  }
  
  public S toString() {
    ret a + " " + b + " is " + c + " " + d;
  }
  
  NQ reverse() {
    ret new NQ(c, d, a, b);
  }

  bool trivial() {
    ret eq(b, d) && eq(a, c);
  }
  
  bool usable() {
    if (trivial()) ret false;
    if (eq(a, 0) || eq(c, 0)) ret false;
    if (eq(b, d)) ret false; // matchin kinds, non-matching numbers
    ret true;
  }
}

static new L<NQ> terms;

p {
  load(dataProgID, "terms");
}

synchronized answer {
  if (match("* * is * *", s, m) || match("* * are * *", s, m)) {
    NQ nq = new NQ(m.unq(0), simplify(m.unq(1)), m.unq(2), simplify(m.unq(3)));
    if (terms.contains(nq))
      ret "I know!";
    terms.add(nq);
    save(dataProgID, "terms");
    ret "OK, added to theory. Now " + l(terms) + " entries";
  }
  
  if (match("show theory", s)) {
    ret structure(allToString(terms));
  }
  
  if (match("how many * * * *", s, m)) {
    S isAre = m.get(1);
    if (litlist("is", "are").contains(toLower(isAre))) {
      BigInteger a = bigint(m.unq(2));
      S b = m.unq(3);
      S d = m.unq(0);
      Rat c = calc(new Rat(a), b, d);
      if (c == null)
        ret "I don't know";
      ret a + " " + b + " " + isAre + " " + c.mixed() + " " + d + "!";
    }
  }
  
  if (match("check theory", s))
    ret checkTheory();
    
  if (match("show clusters", s))
    ret showClusters();
}

static Rat calc(Rat a, S b, S d) {
  b = simplify(b);
  d = simplify(d);
  ret calcTransitive(a, b, d, new TreeSet);
}

// b is the unit we have, d is the unit we're searching for
static Rat calcTransitive(Rat a, S b, S d, Set<S> seen) {
  print(format("calcTransitive * * * *", a, b, d, structure(seen)));
  if (eq(b, d)) ret a; // done
  if (seen.contains(b)) ret null;
  seen.add(b);
  for (NQ nq : terms) if (nq.usable()) {
    twice {
      if (eq(nq.b, b)) {
        Rat r = calcTransitive(calcForward(nq, a), nq.d, d, seen);
        if (r != null) ret r;
      }
      nq = nq.reverse();
    }
  }
  null;
}

static Rat calcForward(NQ nq, Rat a) {
  ret a.multiply(nq.c).divide(nq.a);
}

static S simplify(S s) {
  ret toSingular(toLower(s));
}

static S toSingular(S s) {
  ret dropSuffix("s", s); // yeah it's rough
}

static BigInteger smartBigint(S s) {
  if (litlist("a", "an", "one").contains(toLower(s)))
    ret bigint(1);
  ret bigint(s);
}

static S checkTheory() {
  new L<NQ> trivial;
  new L<NQ> valid;
  new L<NQ> invalid;
  for (NQ nq : terms) {
    L<NQ> bucket = nq.trivial() ? trivial : nq.usable() ? valid : invalid;
    bucket.add(nq);
  }
  
  new StringBuilder buf;
  if (!isEmpty(trivial))
    buf.append(l(trivial) + " trivial: " + joinQuoted(", ", allToString(trivial)) + ".\n");
  
  if (!isEmpty(invalid))
    buf.append(l(invalid) + " invalid: " + joinQuoted(", ", allToString(invalid)) + ".\n");
  
  if (!isEmpty(valid))
    buf.append(l(valid) + " valid statements.\n");
    
  L<L<S>> clusters = getClusters();
  buf.append(l(clusters) + " clusters. ");

  int consistent = 0;
  new L<L<S>> inconsistent;
  for (L<S> cluster : clusters) {
    boolean ok = checkCluster(cluster);
    if (ok) ++consistent; else inconsistent.add(cluster);
  }
  
  if (isEmpty(inconsistent))
    buf.append("All consistent.\n");
  else {
    buf.append(l(inconsistent) + " cluster(s) inconsistent:\n");
    for (L<S> cluster : inconsistent)
      buf.append("  " + structure(cluster) + "\n");
  }

  ret trim(buf);
}

static L<L<S>> getClusters() {
  L<NQ> l = filterByMethod(terms, "usable"); // get all usable terms
  
  // a cluster is a list of concepts.
  // first, make trivial clusters (one per concept).
  
  Map<S, L<S>> clusters = new TreeMap<S, L<S>>();
  for (NQ nq : l) {
    if (!clusters.containsKey(nq.b))
      clusters.put(nq.b, litlist(nq.b));
    if (!clusters.containsKey(nq.d))
      clusters.put(nq.d, litlist(nq.d));
  }
  
  // then, merge the clusters.
  
  for (NQ nq : l) {
    L<S> c1 = clusters.get(nq.b), c2 = clusters.get(nq.d);
    if (c1 != c2) { // different clusters, need to merge!
      mergeClusters(clusters, c1, c2);
    }
  }
  
  // IdentitySet would be more efficient, but meh.
  ret asList(new HashSet<L<S>>(clusters.values()));
}

static S showClusters() {
  L<L<S>> clusters = getClusters();
  ret l(clusters) + " clusters: " + structure(clusters);
}

static void mergeClusters(Map<S, L<S>> clusters, L<S> c1, L<S> c2) {
  for (S concept : c2) {
    clusters.put(concept, c1);
    c1.add(concept);
  }
}

static boolean checkCluster(L<S> cluster) {
  new Map<S, Rat> values;
  
  // randomly choose a concept and a value (!= 0) to start with
  values.put(cluster.get(0), rat(1));
  
  while true {
    int lastSize = l(values);
    
    for (NQ nq : terms) if (nq.usable()) {
      twice {
        Rat lvalue = values.get(nq.b);
        if (lvalue != null) {
          Rat rvalue = calcForward(nq, lvalue);
          Rat expectedValue = values.get(nq.d);
          if (expectedValue == null) 
            values.put(nq.d, rvalue);
          else if (neq(expectedValue, rvalue))
            ret false; // Cluster is inconsistent!
        }
        nq = nq.reverse();
      }
    }
    if (l(values) == lastSize) ret true; // all done
  }
}