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 }