001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.parser;
004    
005    import javafe.util.Assert;
006    
007    class TokenQueue
008    {
009        //// Instance variables
010    
011        /**
012         * Contents of queue tokens.  Used as circular buffer with
013         * <code>start</code> and <code>end</code> being output and input
014         * pointers, respectively.  <code>toks[start]</code> is first
015         * element; <code>toks[(end + toks.len - 1) % toks.len]</code> is
016         * last element.
017         */
018    
019        //@ invariant \nonnullelements(toks);
020        //@ spec_public
021        private Token[] toks;
022    
023        //@ invariant 0 <= start && start < toks.length;
024        //@ spec_public
025        private int start;
026    
027        //@ invariant 0 <= end && end < toks.length;
028        //@ spec_public
029        private int end;
030    
031    
032        //@ ensures !notempty;
033        public TokenQueue() {
034            toks = new Token[4];
035            for(int i = 0; i < toks.length; i++)
036                toks[i] = new Token();
037            start = end = 0;
038        }
039    
040    
041        /** Do not write.  True iff queue is not empty. */  //
042        //@ invariant notempty == (end != start );
043        public boolean notempty = false;
044    
045        // Invariants (size == ((end + toks.length) - start) % toks.length):
046    
047    
048        //// Methods
049    
050        /** Returns number of items in token queue. */
051    
052        //@ ensures \result>=0;
053        //@ ensures \result>0 == notempty;
054        public int size() {
055            int sa = (start <= end ? 0 : toks.length);
056            return (end + sa) - start;
057        }
058    
059        /** Returns <code>n</code>th element in token queue.
060         <pre><esc>
061         requires 0 <= n;
062         </esc></pre>    
063         */
064    
065        //@ ensures \result != null;
066        public Token elementAt(int n) {
067            int sa = (start <= end ? 0 : toks.length);
068            int size = (end + sa) - start;
069            if (n < 0 || size <= n)
070                throw new IndexOutOfBoundsException();
071            int ndx = start + n;
072            if (toks.length <= ndx) ndx -= toks.length;
073            return toks[ndx];
074        }   //@ nowarn Exception;
075    
076        public void setElementAt(int n,Token t) {
077            int sa = (start <= end ? 0 : toks.length);
078            int size = (end + sa) - start;
079            if (n < 0 || size <= n)
080                throw new IndexOutOfBoundsException();
081            int ndx = start + n;
082            if (toks.length <= ndx) ndx -= toks.length;
083            toks[ndx] = t;
084        }   //@ nowarn Exception;
085    
086    
087        /** Empties lookahead queue. */
088    
089        //@ modifies end, notempty, start;
090        //@ ensures !notempty;
091        public void clear() {
092            end = start = 0;
093            notempty = false;
094            for(int i = 0; i < toks.length; i++) {
095                Token t = toks[i];
096                //@ assert 0 <= i && i < toks.length;
097                //@ assert (\forall int j; 0 <= j && j < toks.length ==> toks[j] != null );
098                //@ assert toks[0] != null;
099                //@ assert t != null;
100                t.clear();
101            }
102        }
103    
104        /** Removes head of token queue.  Requires: notempty
105         <pre><esc>
106         requires dst != null;
107         </esc></pre>
108         */
109    
110        //@ requires notempty;
111        //@ modifies start;
112        //@ modifies notempty;
113        public void dequeue(Token dst) {
114            if (start != end) {
115                toks[start].copyInto(dst);
116    
117                // Clear token to allow GC:
118                toks[start].clear();
119    
120                start = start+1;
121                if (start == toks.length) start = 0; 
122                notempty = (start != end);
123            } else Assert.precondition(false);
124        }
125    
126        /** Pushes a token onto the lookahead queue.
127         <pre><esc>
128         requires td != null;
129         </esc></pre>
130         */
131    
132        public void enqueue(Token td) {
133            Assert.notNull(td);
134    
135            // We always have space at end
136            td.copyInto(toks[end]);
137            end=end+1;
138            if (end == toks.length) end = 0; 
139    
140            if (start == end) {
141                // Out of space, need to extend array, double it
142                int len = toks.length;
143                Token[] _new = new Token[2*len];
144                for(int i = 0; i < len; i++) _new[i] = toks[(i + start) % len];
145                for(int i = _new.length-1; len <= i; i--) _new[i] = new Token();
146                start = 0;
147                end = toks.length;
148                toks = _new;
149            }
150            notempty = true;
151        }
152    
153        //@ ensures \result != null;
154        private String stateToString() {
155            return ("start: " + start
156                    + " end: " + end
157                    + " length: " + toks.length);
158        }
159    
160        public void zzz(String prefix) {
161            Assert.notFalse(notempty == (end != start), prefix+"notempty not correct");
162                        
163            int len = toks.length;
164            int size = size();
165    
166            Assert.notFalse(0 <= start && start < len, prefix + "start out of bounds");
167            Assert.notFalse(0 <= end && end < len, prefix + "end out of bounds");
168            for(int i = 0; i < len; i++) {
169                Assert.notNull(toks[i], (prefix + "bad lookahead queue: "
170                                         + stateToString() + " at: " + i));
171                int ndx = (i + start) % len;
172                if (i < size) toks[ndx].zzz();
173                else Assert.notFalse(toks[ndx].auxVal == null,   //@ nowarn Pre;
174                                     prefix + "bad lookahead queue: "
175                                     + stateToString() + " at: " + ndx);
176            }
177        }
178    }