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 }