    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    }