package accrue.analysis.interprocvarcontext;

import java.util.LinkedHashSet;
import java.util.Set;

/**
 * A stack of abstract values. The primary use of this class is to record the
 * expression stack during analysis. That is, 
 *
 * @param <T> The type of the abstract values.
 */
public abstract class Stack<T extends AbstractValue<T>> {
    public static final EmptyStack EMPTY = new EmptyStack();

    @SuppressWarnings("unchecked")
    public static final <T extends AbstractValue<T>> Stack<T> emptyStack() {
        return EMPTY;
    }

    public static final <T extends AbstractValue<T>> Stack<T> singleton(T v,
            Object source) {
        return new NonemptyStack<T>(v, source, Stack.<T> emptyStack());
    }

    public abstract T peek();

    public abstract Object peekSource();

    public abstract Stack<T> pop();

    public Stack<T> push(T v, Object source) {
        return new NonemptyStack<T>(v, source, this);
    }

    public abstract boolean leq(Stack<T> that);

    public abstract Stack<T> upperBound(Stack<T> that);

    public abstract Stack<T> widen(Stack<T> that);

    @Override
    public abstract boolean equals(Object o);

    public abstract boolean isEmpty();

    public abstract int size();

    protected abstract void tailString(StringBuffer sb);

    private static class EmptyStack<T extends AbstractValue<T>> extends
            Stack<T> {
        private EmptyStack() {
        }

        @Override
        public T peek() {
            throw new RuntimeException("peek called on empty stack");
        }

        @Override
        public Object peekSource() {
            throw new RuntimeException("peekSource called on empty stack");
        }

        @Override
        public Stack<T> pop() {
            throw new RuntimeException("pop called on empty stack");
        }

        @Override
        public boolean isEmpty() {
            return true;
        }

        @Override
        public int size() {
            return 0;
        }

        @Override
        public boolean leq(Stack<T> that) {
            return this == that;
        }

        @Override
        public Stack<T> upperBound(Stack<T> that) {
            if (this == that) return this;
            throw new RuntimeException("Taking upper bound of stacks of different sizes");
        }

        @Override
        public Stack<T> widen(Stack<T> that) {
            if (this == that) return this;
            throw new RuntimeException("Taking upper bound (widening) of stacks of different sizes");
        }

        @Override
        public boolean equals(Object o) {
            return this == o;
        }

        @Override
        public int hashCode() {
            return 598974;
        }

        @Override
        public String toString() {
            return "{}";
        }

        @Override
        protected void tailString(StringBuffer sb) {
        }

    }

    private static class NonemptyStack<T extends AbstractValue<T>> extends
            Stack<T> {
        private final T v;
        private final Object source;
        private final Stack<T> s;
        private final int size;

        public NonemptyStack(T v, Object source, Stack<T> s) {
            this.v = v;
            this.source = source;
            this.s = s;
            this.size = 1 + s.size();
            if (source == null)
                throw new IllegalArgumentException("Source should be descriptive and non-null");
        }

        @Override
        public T peek() {
            return v;
        }

        @Override
        public Object peekSource() {
            return source;
        }

        @Override
        public Stack<T> pop() {
            return s;
        }

        @Override
        public boolean isEmpty() {
            return false;
        }

        @Override
        public int size() {
            return this.size;
        }

        @Override
        public boolean leq(Stack<T> that) {
            if (this == that) return true;
            if (that instanceof NonemptyStack) {
                NonemptyStack<T> t = (NonemptyStack<T>) that;
                if (this.v.leq(t.v)) {
                    return this.s.leq(t.s);
                }
            }
            return false;
        }

        @Override
        public Stack<T> upperBound(Stack<T> that) {
            return wideningUpperBound(that, false);
        }

        @Override
        public Stack<T> widen(Stack<T> that) {
            return wideningUpperBound(that, true);
        }

        public Stack<T> wideningUpperBound(Stack<T> that, boolean widen) {
            if (this == that) return this;
            if (that instanceof NonemptyStack) {
                NonemptyStack<T> t = (NonemptyStack<T>) that;
                T u;
                if (widen) {
                    u = (this.v == null ? t.v : this.v.widen(t.v));
                }
                else {
                    u = (this.v == null ? t.v : this.v.upperBound(t.v));
                }
                Object newSource = null;
                if (this.source == t.source) {
                    newSource = this.source;
                }
                else {
                    newSource = mergeSources(this.source, t.source);
                }
                if (widen) {
                    return new NonemptyStack<T>(u, newSource, this.s.widen(t.s));
                }
                else {
                    return new NonemptyStack<T>(u,
                                                newSource,
                                                this.s.upperBound(t.s));
                }
            }
            throw new RuntimeException("Taking upper bound of stacks of different sizes");
        }

        private Object mergeSources(Object s, Object t) {
            Set<Object> set = new LinkedHashSet<Object>();
            if (s instanceof Set) {
                set.addAll((Set<?>) s);
            }
            else {
                set.add(s);
            }
            if (t instanceof Set) {
                set.addAll((Set<?>) t);
            }
            else {
                set.add(t);
            }
            return set;
        }

        @Override
        public int hashCode() {
            return s.hashCode() ^ ((v == null) ? 0 : v.hashCode());
        }

        @Override
        public boolean equals(Object obj) {
            if (this == obj) return true;
            if (!(obj instanceof NonemptyStack)) return false;
            NonemptyStack<?> other = (NonemptyStack<?>) obj;
            if (s == null) {
                if (other.s != null) return false;
            }
            else if (!s.equals(other.s)) return false;
            if (v == null) {
                if (other.v != null) return false;
            }
            else if (!v.equals(other.v)) return false;
            return true;
        }

        @Override
        public String toString() {
            StringBuffer sb = new StringBuffer();
            sb.append('{');
            sb.append(v.toString());
            sb.append('(');
            sb.append(source == null ? "unknown source" : source.toString());
            sb.append(')');
            s.tailString(sb);
            sb.append('}');
            return sb.toString();
        }

        @Override
        protected void tailString(StringBuffer sb) {
            sb.append("::");
            sb.append(v.toString());
            sb.append('(');
            sb.append(source.toString());
            sb.append(')');
            s.tailString(sb);
        }

    }
}
