package formulaVisited;
import java.io.*;


/**
  A factory for creating formulas from a reader.
  The specific Formula subclass that is returned
  depends on what the reader reads.
  Because the factory is stateless,
  all its methods are static.
  True and false are represented by 1 and 0;
  variables are strings of letters and digits
  beginning with a lowercase letter;
  the negation operator is '~';
  conjunctions are in () with '&' as the infix operator;  and
  disjunctions are in [] with '|' as the infix operator.
*/
public class Factory {

  /**
    Reads a character stream and returns
    the formula corresponding to it, if any.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If there is a syntax error
      in the character stream.
  */
  static public Formula factory(PushbackReader _in)
      throws IOException {
    int cc;
    cc = _in.read();  _in.unread(cc);
    if /**/ ( -1 == cc) {
      throw new RuntimeException("Expected formula, found EOF");
    }
    else if ('(' == cc) {  return factoryConjunction    (_in);  }
    else if ('[' == cc) {  return factoryDisjunction    (_in);  }
    else if ('~' == cc) {  return factoryNegation       (_in);  }
    else if ('0' == cc) {  return factoryLogicalConstant(_in);  }
    else if ('1' == cc) {  return factoryLogicalConstant(_in);  }
    else if (Character.isLowerCase((char) cc)) {
      return factoryLogicalVariable(_in);
    }
    else {
      throw new RuntimeException("Expected formula, found " +
          printable(cc));
    }
  }

  /**
    Reads a character stream and returns
    the conjunction corresponding to it, if any.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If there is a syntax error
      in the character stream.
  */
  static Formula factoryConjunction(PushbackReader _in)
      throws IOException {
    expect('(', _in);
    Formula left  = factory(_in);
    skipWhitespace(_in);
    expect('&', _in);
    Formula right = factory(_in);
    skipWhitespace(_in);
    expect(')', _in);
    return new Conjunction(left, right);
  }

  /**
    Reads a character stream and returns
    the disjunction corresponding to it, if any.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If there is a syntax error
      in the character stream.
  */
  static Formula factoryDisjunction(PushbackReader _in)
      throws IOException {
    expect('[', _in);
    Formula left  = factory(_in);
    skipWhitespace(_in);
    expect('|', _in);
    Formula right = factory(_in);
    skipWhitespace(_in);
    expect(']', _in);
    return new Disjunction(left, right);
  }

  /**
    Reads a character stream and returns
    the logical constant corresponding to it, if any.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If there is a syntax error
      in the character stream.
  */
  static LogicalConstant factoryLogicalConstant(PushbackReader _in)
      throws IOException {
    String name = readName(_in);
    if /**/ (name.equals("0")) {  return LogicalConstant.zero();  }
    else if (name.equals("1")) {  return LogicalConstant.one ();  }
    else {
      throw new RuntimeException("Expected 0 or 1, found \"" +
            name + "\"");
    }
  }

  /**
    Reads a character stream and returns
    the logical variable corresponding to it, if any.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If there is a syntax error
      in the character stream.
  */
  static Formula factoryLogicalVariable(PushbackReader _in)
      throws IOException {
    String name = readName(_in);
    expectedLowerCase(name.charAt(0));
    return new LogicalVariable(name);
  }

  /**
    Reads a character stream and returns
    the negation corresponding to it, if any.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If there is a syntax error
      in the character stream.
  */
  static Formula factoryNegation(PushbackReader _in)
      throws IOException {
    expect('~', _in);
    Formula subformula = factory(_in);
    return new Negation(subformula);
  }

  /**
    Reads a character stream and returns
    the name corresponding to it, if any.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If there is a syntax error
      in the character stream.
  */
  static String readName(PushbackReader _in) throws IOException {
    StringBuffer name = new StringBuffer();
    int cc;
    while  (-1 < (cc = _in.read()) &&
            Character.isLetterOrDigit((char) cc)) {
      name.append((char) cc);
    }
    _in.unread(cc);
    if (0 == name.length()) {
      throw new RuntimeException("Name expected");
    }
    return name.toString();
  }

  /**
    Skips a string of whitespace in a character stream.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
  */
  static void skipWhitespace(PushbackReader _in)
      throws IOException {
    int cc;
    while  (-1 < (cc = _in.read()) &&
            Character.isWhitespace((char) cc)) {
      // do nothing
    }
    _in.unread(cc);
  }

  /**
    Reads a character and throws an exception
    if the character is not the expected one.
    @param _expected The expected character.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If the expected character
      was not next in the stream.
  */
  static void expect(char _expected, PushbackReader _in)
      throws IOException {
    int cc;
    if (_expected != (cc = _in.read())) {
      throw new RuntimeException("Expected '(', found " +
          printable(cc));
    }
  }

  /**
    Reads a character and throws an exception
    if the character is not lowercase.
    @param _in A pushback reader for the stream.
    @throws IOException If the stream operations do.
    @throws RuntimeException If the stream did not begin
      with a lowercase character.
  */
  static void expectedLowerCase(char _cc) {
    if (!Character.isLowerCase(_cc)) {
      throw new RuntimeException("Expected lowercase, found " +
          printable(_cc));
    }
  }

  /**
    Returns a printable string representing a character.
    @param  _cc The character.
    @return _in A string describing _cc:
      "EOF" if _cc is -1, "newline" if _cc is '\n',
      _cc in single quotes if _cc is printable,
      and the numerical value of _cc otherwise.
  */
  static String printable(int _cc) {
    if /**/ (-1   == _cc) {  return "EOF";  }
    else if ('\n' == _cc) {  return "newline";  }
    else if (Character.isISOControl((char) _cc))
                         {  return "" + _cc;  }
    else                 {  return "'" + (char) _cc + "'";  }
  }

}