public interface Formula<T> {

    public <R> visit(Visitor<T,R> visitor);

    /**
     * A Visitor to perform case analysis on Formula<T>.  This is 
     * intended to be exhaustive; an implementation of this 
     * interface must say how to handle all of the subcaes.  The <R>
     * variable is the result type of the Visitor.
     */
    public static interface Visitor<T, R> {
        public R visitVariable(Variable<T> var);
        public R visitNot(Not<T> var);
        public R visitAnd(And<T> var);
        public R visitOr(Or<T> var);
    }

    public static final class Variable<T> implements Formula<T> {
        private final T tag;

        public Variable(T tag) {
            this.tag = tag;
        }

        public T getTag() {
            return tag;
        }

        public <R> visit(Visitor<T,R> visitor) {
            visitor.visitVariable(this);
        }

    }

    public static final class Not<T> implements Formula<T> {
        private final Formula<T> subformula;

        public Not(Formula<T> subformula) {
            this.subformula = subformula;
        }

        public Formula<T> getSubformula() {
            return subformula;
        }

        public <R> visit(Visitor<T,R> visitor) {
            visitor.visitNot(this);
        }

    }

    public static final class And<T> implements Formula<T> {
        private final Formula<T> left;
        private final Formula<T> right;

        public And(Formula<T> left, Formula<T> right) {
            this.left = left;
        }

        public Formula<T> getLeft() {
            return left;
        }

        public Formula<T> getRight() {
            return right;
        }

        public <R> visit(Visitor<T,R> visitor) {
            visitor.visitAnd(this);
        }

    }

    public static final class Or<T> implements Formula<T> {
        private final Formula<T> left;
        private final Formula<T> right;

        public Or(Formula<T> left, Formula<T> right) {
            this.left = left;
        }

        public Formula<T> getLeft() {
            return left;
        }

        public Formula<T> getRight() {
            return right;
        }

        public <R> visit(Visitor<T,R> visitor) {
            visitor.visitOr(this);
        }

    }

}