!752

static L<S> data = toLinesFullTrim([[
  If A likes B then A will greet B.
  If X then Y.
  If U then V. && U. => V.
  John likes Paul.
]]);

static L<L<S>> log;

static S toCheck = "John will greet Paul.";

sclass Flow {
  new StringBuilder desc;
  new L<Flow> subs;
  
  Flow sub(S desc) {
    new Flow flow;
    flow.append(desc);
    subs.add(flow);
    ret flow;
  }
  
  void append(O o) {
    desc.append(o).append("\n");
  }
  
  void x(O o) { append(o); }
  
  public S toString() {
    ret str(desc) + indentx(allToStringWithLineBreaks(subs));
  }
}

p-typewriter {
  // Parse data
  log = map("tok", data);
  
  new TreeSet<S> newData;
  
  // Go through all rules
  new Flow flow;
  for (L<S> tok : log) {
    SS m = matchSingle("I => O", tok);
    if (m == null) continue;
    S i = m.get("I"), o = m.get("O");
    // Parse left-hand
    L<S> tokI = tok(i);
    L<L<S>> is = splitAtAmpersands(tokI);
    flow.x("Processing LHS: " + struct(is));
    // Apply rule to input
    for (SS m2 : gSatAnd(is, flow))
      newData.add(join(" ", replaceVars(tok(o), m2)));
  }
  
  print("Lines made (\*l(newData)*/):");
  psl(asList(newData));
  printWithAsciiHeading("FLOW", flow);
}

// null = no satisfaction
// otherwise return var map
static Iterable<SS> gSatAnd(L<L<S>> statements, Flow flow) {
  flow = flow.sub("gSatAnd" + struct(statements));
  assertTrue(l(statements) >= 1);
  
  if (l(statements) == 1)
    ret gSat(first(statements), flow);
  
  new L<SS> l;
  for (SS map : gSat(first(statements), flow)) {
    flow.x("First clause satisfied. " + struct(map));
    L<L<S>> s2 = mapReplaceVars(dropFirst(statements), map);
    flow.x("Now looking for: " + struct(s2));
    for (SS map2 : gSatAnd(s2, flow)) {
      flow.x("Sub gSatAnd returned: " + struct(map2));
      addIfNotEmpty(l, mergeMappings(map, map2));
    }
  }
  ret l;
}

static IterableIterator<SS> gSat(L<S> pat, Flow flow) {
  flow = flow.sub("gSat" + struct(pat));
  ret gMatch(pat, flow);
}

static IterableIterator<SS> gMatch(final L<S> pat, final Flow flow) {
  ret new IterableIterator<SS>() {
    int i = l(log);
    Iterator<SS> m;
    
    public bool hasNext() {
      if (m != null && m.hasNext()) true;
      m = null;
      while (--i >= 0) {
        L<SS> l = match(pat, get(log, i));
        if (nempty(l)) {
          flow.x("gMatch found: " + struct(l));
          m = l.iterator();
          true;
        }
      }
      false;
    }
    
    public SS next() { ret m.next(); }
  };
}

static L<L<S>> splitAtAmpersands(L<S> tok) {
  new L<L<S>> l;
  int iAmp;
  while ((iAmp = indexOfSubList(tok, ll("&", "&"))) >= 0) {
    //print("&& found at " + iAmp);
    l.add(subList(tok, 0, iAmp));
    tok = subList(tok, iAmp+2);
  }
  l.add(tok);
  ret l;
}

static SS matchSingle(S pat, L<S> input) {
  ret getSingletonOpt(match(tok(pat), input));
}

static SS matchSingle(S pat, S input) {
  ret getSingletonOpt(match(pat, input));
}

static L<S> tok(S s) {
  ret s == null ? null : codeTokens(nlTok(s));
}

static L<SS> match(S pat, S input) {
  ret match(tok(pat), tok(input));
}

static L<SS> match(L<S> pat, L<S> input) {
  Map<Int, S> vars = singleCharacterVars(pat);
  new L<SS> matches;
  matchImpl(pat, vars, 0, input, 0, new HashMap, matches);
  ret matches;
}

static void matchImpl(L<S> pat, Map<Int, S> vars,
  int iPat, L<S> input, int iInput, SS values,
  L<SS> matches) {
  if (iPat >= l(pat)) {
    if (iInput < l(input)) ret; // fail, too much input
    //print("Match! " + struct(values));
    matches.add(cloneMap(values));
    ret;
  }
  if (iInput >= l(input)) ret; // out of input
  S t = pat.get(iPat);
  S var = vars.get(iPat);
  if (var != null) {
    // it's a variable, try different lengths of input as match
    for (int jInput = iInput+1; jInput <= l(input); jInput++) {
      S value = join(" ", subList(input, iInput, jInput));
      S oldValue = values.get(var);
      if (oldValue != null && !eqic(value, oldValue)) ret; // fail, bad multi-assignment
      if (oldValue == null)
        values.put(var, value);
      // proceed
      matchImpl(pat, vars, iPat+1, input, jInput, values, matches);
      // delete assignment
      if (oldValue == null) values.remove(var); else values.put(var, oldValue);
    }
  } else {
    // it's a literal
    if (!eqic(t, input.get(iInput))) ret; // fail
    // match, proceed
    matchImpl(pat, vars, iPat+1, input, iInput+1, values, matches);
  }
}

static Map<Int, S> singleCharacterVars(L<S> tok) {
  new Map<Int, S> vars;
  for i over tok: {
    S t = tok.get(i);
    if (l(t) == 1 && isUpperCaseLetter(t.charAt(0)))
      vars.put(i, t);
  }
  ret vars;
}

static L<L<S>> mapReplaceVars(L<L<S>> patterns, final SS map) {
  ret map(func(L<S> pat) { replaceVars(pat, map) }, patterns);
}

static L<S> replaceVars(L<S> tok, final Map<S, S> map) {
  ret flattenList(map(tok, func(S t) { or((O) tok(map.get(t)), t) }));
}