source: CIVL/mods/dev.civl.com/scripts/lexical_stream.py

main
Last change on this file was c2b37db, checked in by Alex Wilton <awilton@…>, 8 months ago

Merged focus branch into trunk.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5988 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 7.1 KB
RevLine 
[c2b37db]1import re
2from dataclasses import dataclass
3
4class LexicalStream:
5 """
6 invariants:
7 + _in is a readable, unclosed text stream
8 + _eof is a boolean which is true iff _in has reached the end of its stream
9 (but we may still have unread text in _buffer)
10 + _buffer is a list of strings satisfying:
11 + len(_buffer) > 0
12 + if _buffer[i] contains '\n' for some i then it is the last character of the string
13 + if _buffer[i] does not contain '\n' then i ~= -1 and _eof.
14 + if _peekStack is empty then len(_buffer) == 1
15 + _peekStack is a list of SourceLoc satisfying:
16 + for all 0 <= i <= j < len(_peekStack): SourceLoc(0,0) <= _peekStack(i) <= _peekStack(j) <= _headLoc
17 + _headLoc is a SourceLoc satisfying:
18 + 0 <= _headLoc.lineNum < len(_buffer)
19 + 0 <= _headLoc.charPos <= len(_buffer[_headLoc.lineNum])
20 + _headLoc.charPos == len(_buffer[_headLoc.lineNum]) iff all of the following hold:
21 + _headLoc.lineNum ~= -1
22 + _headLoc.charPos == 0 (i.e. the last string is just "")
23 + _eof
24 + _buffLoc is a SourceLoc that only can increase over time.
25
26 (note that ~= means "equal as an index". So 3 ~= -1 wrt list l if l[3] refers to the same element as l[-1])
27 """
28 def __init__(self, rTxtFile):
29 assert rTxtFile.readable() and not rTxtFile.closed
30 self._in = rTxtFile
31 self._buffer = [self._in.readline()]
32 self._eof = self._buffer[0] == ""
33 self._peekStack = []
34 self._headLoc = SourceLoc(0,0)
35 self._buffLoc = SourceLoc(0,0)
36
37 def start(self):
38 self._peekStack.append(self._headLoc)
39
40 def complete(self):
41 openLoc = self._peekStack.pop()
42 closedLines = []
43
44 if self._headLoc.lineNum == openLoc.lineNum:
45 closedLines = [self._buffer[openLoc.lineNum][openLoc.charPos:self._headLoc.charPos]]
46 else:
47 closedLines = [self._buffer[openLoc.lineNum][openLoc.charPos:]]
48
49 closedLines.extend(self._buffer[openLoc.lineNum+1:self._headLoc.lineNum])
50 if self._headLoc.charPos > 0:
51 closedLines.append(self._buffer[self._headLoc.lineNum][:self._headLoc.charPos])
52 if len(self._peekStack) == 0:
53 self._shrinkBufferToHead()
54
55 return SourceRange(closedLines, self._getGlobalLoc(openLoc))
56
57 def revert(self):
58 self._headLoc = self._peekStack.pop()
59
60 def eof(self):
61 return self._eof and self._eob(self._headLoc)
62
63 def readline(self):
64 return self.readlines(1)[0]
65
66 def readlines(self, n):
67 if n <= 0:
68 return None
69
70 result = [self._restOfLine()]
71 bufferTail = self._buffer[self._headLoc.lineNum+1:]
72 tailBufferReads = min(n-1, self._bufferEnd().lineNum)
73
74 result.extend(bufferTail[:tailBufferReads])
75 pulledReads = n - len(bufferTail) - 1
76
77 if pulledReads >= 0:
78 pullStart = self._pull(pulledReads)
79
80 result.extend(self._buffer[pullStart.lineNum:])
81 self._headLoc = self._bufferEnd()
82 self._headLoc = self._pull()
83 else:
84 self._headLoc = SourceLoc(self._headLoc.lineNum + 1 + tailBufferReads, 0)
85
86 return result
87
88
89 def read(self, n):
90 if self.eof():
91 return ""
92
93 rest = self._restOfLine()
94 if n < len(rest):
95 self._headLoc = SourceLoc(self._headLoc.lineNum, self._headLoc.charPos + n)
96 return rest[:n]
97 else:
98 rest = self.readline()
99 return rest + self.read(n-len(rest))
100
101 def match(self, string):
102 self.start()
103 if self.read(len(string)) == string:
104 return self.complete()
105 else:
106 self.revert()
107 return None
108
109 """
110 Note: Only performs regex matching on current line.
111 """
112 def regmatch(self, pattern):
113 rest = self._restOfLine()
114 match = re.match(pattern, rest)
115 if match:
116 self.read(match.end())
117 return match
118 else:
119 return None
120
121 def peek(self, pattern):
122 self.start()
123 isMatch = self.regmatch(pattern) != None
124 self.revert()
125 return isMatch
126
127 def skipws(self):
128 rest = self._restOfLine()
129 while (nextNonWs := len(rest) - len(rest.lstrip())) == len(rest) and not self.eof():
130 self.readline()
131 rest = self._restOfLine()
132 self._headLoc = SourceLoc(self._headLoc.lineNum, self._headLoc.charPos + nextNonWs)
133
134 def pos(self):
135 return self._getGlobalLoc(self._headLoc)
136
137 # Private methods
138
139 def _restOfLine(self):
140 return self._buffer[self._headLoc.lineNum][self._headLoc.charPos:]
141
142 def _getGlobalLoc(self, relLoc):
143 return self._buffLoc.add(relLoc)
144
145 def _bufferEnd(self):
146 return SourceLoc.lineArrEnd(self._buffer)
147
148 def _eob(self, loc):
149 return loc >= self._bufferEnd()
150
151 def _shrinkBufferToHead(self):
152 if self._headLoc.lineNum > 0:
153 self._buffer = self._buffer[self._headLoc.lineNum:]
154 self._buffLoc = SourceLoc(self._buffLoc.lineNum + self._headLoc.lineNum, 0)
155 self._headLoc = SourceLoc(0, self._headLoc.charPos)
156
157 """
158 Reads n newlines from _in and moves them into the buffer.
159 Does not change _headLoc. Returns starting location of pulled lines.
160 If _eof when called, then no change to _buffer and returns _bufferEnd()
161 """
162 def _pull(self, n=1):
163 pulledLines = []
164 while n > 0 and not self._eof:
165 newLine = self._in.readline()
166
167 if newLine == "":
168 self._eof = True
169 pulledLines.append(newLine)
170 n -= 1
171
172 if len(pulledLines) > 0 and self._eob(self._headLoc) and len(self._peekStack) == 0:
173 # Condition implies we can throw out old _buffer
174 # Also, invariant implies that len(_buffer) == 1 hence
175 # we only need to shift _buffLoc forward one line
176 self._buffLoc = SourceLoc(self._buffLoc.lineNum+1,0)
177 self._buffer = pulledLines
178 return SourceLoc(0,0)
179
180 result = self._bufferEnd()
181
182 self._buffer.extend(pulledLines)
183 return result
184
185
186class SourceRange:
187 def __init__(self, lines, startLoc):
188 self._lines = lines
189 self._startLoc = startLoc
190 self._endLoc = startLoc.add(SourceLoc(len(lines)-1, len(lines[-1])))
191
192 def getStr(self):
193 return ''.join(self._lines)
194
195 def getLines(self):
196 return self._lines
197
198 def getStartLoc(self):
199 return self._startLoc
200
201 def getEndLoc(self):
202 return self._endLoc
203
204@dataclass(order=True, frozen=True)
205class SourceLoc:
206 lineNum: int
207 charPos: int
208
209 # Intentially not __add__ since it isn't associative
210 def add(self, other):
211 charPos = other.charPos
212 if other.lineNum == 0:
213 charPos += self.charPos
214 return SourceLoc(self.lineNum + other.lineNum, charPos)
215
216 def lineArrEnd(lines):
217 return SourceLoc(len(lines) - 1 if len(lines[-1]) == 0 else len(lines), 0)
218
219class ParseError(Exception):
220 def __init__(self, lineNum):
221 self.lineNum = lineNum
Note: See TracBrowser for help on using the repository browser.