/**
 * A repository class containing constants for boolean operators and their
 * precedences. This class contains static definitions of boolean operators and
 * their precedences. Operators are declared as constant instances of classes
 * that implement the {@link Operator Operator} interface, and provide methods
 * for generating string representations of propositions that contain no
 * unnecessary brackets. Precedences of the operators are declared as integer
 * constants that are used by these methods to determine whether brackets are
 * necessary; these constants are also used by the {@link Parser Parser} class.
 *
 */
public class Operators {

	/**
	 * A value higher than the precedence of any operator. This is used by
	 * {@link BoolTerm#toString() BoolTerm.toString()} to avoid brackets around
	 * a whole term.
	 *
	 */
	public static final int MAX_PREC = 9;
	/**
	 * Precedence of "implies" operator.
	 */
	public static final int IMPLIES_PREC = 7;
	/**
	 * Precedence of "or" operator.
	 */
	public static final int OR_PREC = 5;
	/**
	 * Precedence of "and" operator.
	 */
	public static final int AND_PREC = 4;
	/**
	 * Precedence of "not" operator.
	 */
	public static final int NOT_PREC = 1;

	/**
	 * Representation of the Boolean operator "and".
	 *
	 */
	public static final Operator AND = new Operator() {

		/**
		 * Check if the array of terms is of length 2, i.e., matches the number
		 * of operands for "and".
		 */
		public boolean isWellFormed(BoolTerm[] args) {
			return (args.length == 2);
		}

		/**
		 * Give a string representing a proposition with no unnecessary
		 * brackets. The main operator of the proposition will be "and".
		 *
		 * @param args
		 *            the operands for "and": this array should be of length 2
		 * @param prec
		 *            the precedence of the operator above.
		 * @return a string representing the proposition formed by applying
		 *         "and" to the operands in <code>args</code>; the entire string
		 *         will be enclosed in brackets if parameter <code>prec</code>
		 *         is less than {@link #AND_PREC AND_PREC}
		 */
		public String toString(BoolTerm[] args, int prec) {
			String s = args[0].toString(AND_PREC) + " and "
					+ args[1].toString(AND_PREC);
			if (prec < AND_PREC)
				s = "(" + s + ")";
			return s;
		}

		/**
		 * Return the precedence of "and".
		 */
		public int getPrecedence() {
			return AND_PREC;
		}
	};

	/**
	 * Representation of the Boolean operator "or".
	 *
	 */
	public static final Operator OR = new Operator() {

		/**
		 * Check if the array of terms is of length 2, i.e., matches the number
		 * of operands for "or".
		 */
		public boolean isWellFormed(BoolTerm[] args) {
			return (args.length == 2);
		}

		/**
		 * Give a string representing a proposition with no unnecessary
		 * brackets. The main operator of the proposition will be "or".
		 *
		 * @param args
		 *            the operands for "or": this array should be of length 2
		 * @param prec
		 *            the precedence of the operator above.
		 * @return a string representing the proposition formed by applying "or"
		 *         to the operands in <code>args</code>; the entire string will
		 *         be enclosed in brackets if parameter <code>prec</code> is
		 *         less than {@link #OR_PREC OR_PREC}
		 */
		public String toString(BoolTerm[] args, int prec) {
			String s = args[0].toString(OR_PREC) + " or "
					+ args[1].toString(OR_PREC);
			if (prec < OR_PREC)
				s = "(" + s + ")";
			return s;
		}

		/**
		 * Return the precedence of "or".
		 */
		public int getPrecedence() {
			return OR_PREC;
		}
	};

	/**
	 * Representation of the Boolean operator "implies".
	 *
	 */
	public static final Operator IMPLIES = new Operator() {

		/**
		 * Check if the array of terms is of length 2, i.e., matches the number
		 * of operands for "implies".
		 */
		public boolean isWellFormed(BoolTerm[] args) {
			return (args.length == 2);
		}

		/**
		 * Give a string representing a proposition with no unnecessary
		 * brackets. The main operator of the proposition will be "implies".
		 *
		 * @param args
		 *            the operands for "implies": this array should be of length
		 *            2
		 * @param prec
		 *            the precedence of the operator above.
		 * @return a string representing the proposition formed by applying
		 *         "implies" to the operands in <code>args</code>; the entire
		 *         string will be enclosed in brackets if parameter
		 *         <code>prec</code> is less than {@link #OR_PREC OR_PREC}
		 */
		public String toString(BoolTerm[] args, int prec) {
			String s = args[0].toString(IMPLIES_PREC) + " implies "
					+ args[1].toString(IMPLIES_PREC);
			if (prec < IMPLIES_PREC)
				s = "(" + s + ")";
			return s;
		}

		/**
		 * Return the precedence of "implies".
		 */
		public int getPrecedence() {
			return IMPLIES_PREC;
		}
	};

	/**
	 * Representation of the Boolean operator "not".
	 *
	 */
	public static final Operator NOT = new Operator() {

		/**
		 * Check if the array of terms is of length 1, i.e., matches the number
		 * of operands for "not".
		 */
		public boolean isWellFormed(BoolTerm[] args) {
			return (args.length == 1);
		}

		/**
		 * Give a string representing a proposition with no unnecessary
		 * brackets. The main operator of the proposition will be "not".
		 *
		 * @param args
		 *            the operands for "not": this array should be of length 1
		 * @param prec
		 *            the precedence of the operator above.
		 * @return a string representing the proposition formed by applying
		 *         "not" to the operands in <code>args</code>; the entire string
		 *         will be enclosed in brackets if parameter <code>prec</code>
		 *         is less than {@link #OR_PREC OR_PREC}
		 */
		public String toString(BoolTerm[] args, int prec) {
			String s = "not " + args[0].toString(NOT_PREC);
			if (prec < NOT_PREC)
				s = "(" + s + ")";
			return s;
		}

		/**
		 * Return the precedence of "not".
		 */
		public int getPrecedence() {
			return NOT_PREC;
		}
	};

	/**
     * The constant `true'.
     *
     */
	public static final Operator TRUEC = new Operator() {
		public boolean isWellFormed(BoolTerm[] args) {
			return (args.length == 0);
		}

		public String toString(BoolTerm[] args, int prec) {
			return "true";
		}

		public int getPrecedence() {
			return MAX_PREC;
		}
	};

	/**
     * The constant `false'.
     *
     */
	public static final Operator FALSEC = new Operator() {
		public boolean isWellFormed(BoolTerm[] args) {
			return (args.length == 0);
		}

		public String toString(BoolTerm[] args, int prec) {
			return "false";
		}

		public int getPrecedence() {
			return MAX_PREC;
		}
	};

	
	/**
     * Make a variable as a operator.
     *
     * @param name the name of the variable
     * @return the variable as a constant operator.
     */
	public static Operator makeVar(final String name) {
		return new Operator() {
			public boolean isWellFormed(BoolTerm[] args) {
				return (args.length == 0);
			}

			public String toString(BoolTerm[] args, int prec) {
				return name;
			}

			public int getPrecedence() {
				return MAX_PREC;
			}
		};
	}
}// Operators