Coverage for /pythoncovmergedfiles/medio/medio/usr/local/lib/python3.8/site-packages/pygments/lexers/tnt.py: 34%
206 statements
« prev ^ index » next coverage.py v7.2.7, created at 2023-07-01 06:54 +0000
1"""
2 pygments.lexers.tnt
3 ~~~~~~~~~~~~~~~~~~~
5 Lexer for Typographic Number Theory.
7 :copyright: Copyright 2006-2023 by the Pygments team, see AUTHORS.
8 :license: BSD, see LICENSE for details.
9"""
11import re
13from pygments.lexer import Lexer
14from pygments.token import Text, Comment, Operator, Keyword, Name, Number, \
15 Punctuation, Error
17__all__ = ['TNTLexer']
20class TNTLexer(Lexer):
21 """
22 Lexer for Typographic Number Theory, as described in the book
23 Gödel, Escher, Bach, by Douglas R. Hofstadter
25 .. versionadded:: 2.7
26 """
28 name = 'Typographic Number Theory'
29 url = 'https://github.com/Kenny2github/language-tnt'
30 aliases = ['tnt']
31 filenames = ['*.tnt']
33 cur = []
35 LOGIC = set('⊃→]&∧^|∨Vv')
36 OPERATORS = set('+.⋅*')
37 VARIABLES = set('abcde')
38 PRIMES = set("'′")
39 NEGATORS = set('~!')
40 QUANTIFIERS = set('AE∀∃')
41 NUMBERS = set('0123456789')
42 WHITESPACE = set('\t \v\n')
44 RULES = re.compile('''(?xi)
45 joining | separation | double-tilde | fantasy\\ rule
46 | carry[- ]over(?:\\ of)?(?:\\ line)?\\ ([0-9]+) | detachment
47 | contrapositive | De\\ Morgan | switcheroo
48 | specification | generalization | interchange
49 | existence | symmetry | transitivity
50 | add\\ S | drop\\ S | induction
51 | axiom\\ ([1-5]) | premise | push | pop
52 ''')
53 LINENOS = re.compile(r'(?:[0-9]+)(?:(?:, ?|,? and )(?:[0-9]+))*')
54 COMMENT = re.compile(r'\[[^\n\]]+\]')
56 def __init__(self, *args, **kwargs):
57 Lexer.__init__(self, *args, **kwargs)
58 self.cur = []
60 def whitespace(self, start, text, required=False):
61 """Tokenize whitespace."""
62 end = start
63 try:
64 while text[end] in self.WHITESPACE:
65 end += 1
66 except IndexError:
67 end = len(text)
68 if required and end == start:
69 raise AssertionError
70 if end != start:
71 self.cur.append((start, Text, text[start:end]))
72 return end
74 def variable(self, start, text):
75 """Tokenize a variable."""
76 if text[start] not in self.VARIABLES:
77 raise AssertionError
78 end = start+1
79 while text[end] in self.PRIMES:
80 end += 1
81 self.cur.append((start, Name.Variable, text[start:end]))
82 return end
84 def term(self, start, text):
85 """Tokenize a term."""
86 if text[start] == 'S': # S...S(...) or S...0
87 end = start+1
88 while text[end] == 'S':
89 end += 1
90 self.cur.append((start, Number.Integer, text[start:end]))
91 return self.term(end, text)
92 if text[start] == '0': # the singleton 0
93 self.cur.append((start, Number.Integer, text[start]))
94 return start+1
95 if text[start] in self.VARIABLES: # a''...
96 return self.variable(start, text)
97 if text[start] == '(': # (...+...)
98 self.cur.append((start, Punctuation, text[start]))
99 start = self.term(start+1, text)
100 if text[start] not in self.OPERATORS:
101 raise AssertionError
102 self.cur.append((start, Operator, text[start]))
103 start = self.term(start+1, text)
104 if text[start] != ')':
105 raise AssertionError
106 self.cur.append((start, Punctuation, text[start]))
107 return start+1
108 raise AssertionError # no matches
110 def formula(self, start, text):
111 """Tokenize a formula."""
112 if text[start] in self.NEGATORS: # ~<...>
113 end = start+1
114 while text[end] in self.NEGATORS:
115 end += 1
116 self.cur.append((start, Operator, text[start:end]))
117 return self.formula(end, text)
118 if text[start] in self.QUANTIFIERS: # Aa:<...>
119 self.cur.append((start, Keyword.Declaration, text[start]))
120 start = self.variable(start+1, text)
121 if text[start] != ':':
122 raise AssertionError
123 self.cur.append((start, Punctuation, text[start]))
124 return self.formula(start+1, text)
125 if text[start] == '<': # <...&...>
126 self.cur.append((start, Punctuation, text[start]))
127 start = self.formula(start+1, text)
128 if text[start] not in self.LOGIC:
129 raise AssertionError
130 self.cur.append((start, Operator, text[start]))
131 start = self.formula(start+1, text)
132 if text[start] != '>':
133 raise AssertionError
134 self.cur.append((start, Punctuation, text[start]))
135 return start+1
136 # ...=...
137 start = self.term(start, text)
138 if text[start] != '=':
139 raise AssertionError
140 self.cur.append((start, Operator, text[start]))
141 start = self.term(start+1, text)
142 return start
144 def rule(self, start, text):
145 """Tokenize a rule."""
146 match = self.RULES.match(text, start)
147 if match is None:
148 raise AssertionError
149 groups = sorted(match.regs[1:]) # exclude whole match
150 for group in groups:
151 if group[0] >= 0: # this group matched
152 self.cur.append((start, Keyword, text[start:group[0]]))
153 self.cur.append((group[0], Number.Integer,
154 text[group[0]:group[1]]))
155 if group[1] != match.end():
156 self.cur.append((group[1], Keyword,
157 text[group[1]:match.end()]))
158 break
159 else:
160 self.cur.append((start, Keyword, text[start:match.end()]))
161 return match.end()
163 def lineno(self, start, text):
164 """Tokenize a line referral."""
165 end = start
166 while text[end] not in self.NUMBERS:
167 end += 1
168 self.cur.append((start, Punctuation, text[start]))
169 self.cur.append((start+1, Text, text[start+1:end]))
170 start = end
171 match = self.LINENOS.match(text, start)
172 if match is None:
173 raise AssertionError
174 if text[match.end()] != ')':
175 raise AssertionError
176 self.cur.append((match.start(), Number.Integer, match.group(0)))
177 self.cur.append((match.end(), Punctuation, text[match.end()]))
178 return match.end() + 1
180 def error_till_line_end(self, start, text):
181 """Mark everything from ``start`` to the end of the line as Error."""
182 end = start
183 try:
184 while text[end] != '\n': # there's whitespace in rules
185 end += 1
186 except IndexError:
187 end = len(text)
188 if end != start:
189 self.cur.append((start, Error, text[start:end]))
190 end = self.whitespace(end, text)
191 return end
193 def get_tokens_unprocessed(self, text):
194 """Returns a list of TNT tokens."""
195 self.cur = []
196 start = end = self.whitespace(0, text)
197 while start <= end < len(text):
198 try:
199 # try line number
200 while text[end] in self.NUMBERS:
201 end += 1
202 if end != start: # actual number present
203 self.cur.append((start, Number.Integer, text[start:end]))
204 # whitespace is required after a line number
205 orig = len(self.cur)
206 try:
207 start = end = self.whitespace(end, text, True)
208 except AssertionError:
209 del self.cur[orig:]
210 start = end = self.error_till_line_end(end, text)
211 continue
212 # at this point it could be a comment
213 match = self.COMMENT.match(text, start)
214 if match is not None:
215 self.cur.append((start, Comment, text[start:match.end()]))
216 start = end = match.end()
217 # anything after the closing bracket is invalid
218 start = end = self.error_till_line_end(start, text)
219 # do not attempt to process the rest
220 continue
221 del match
222 if text[start] in '[]': # fantasy push or pop
223 self.cur.append((start, Keyword, text[start]))
224 start += 1
225 end += 1
226 else:
227 # one formula, possibly containing subformulae
228 orig = len(self.cur)
229 try:
230 start = end = self.formula(start, text)
231 except (AssertionError, RecursionError): # not well-formed
232 del self.cur[orig:]
233 while text[end] not in self.WHITESPACE:
234 end += 1
235 self.cur.append((start, Error, text[start:end]))
236 start = end
237 # skip whitespace after formula
238 orig = len(self.cur)
239 try:
240 start = end = self.whitespace(end, text, True)
241 except AssertionError:
242 del self.cur[orig:]
243 start = end = self.error_till_line_end(start, text)
244 continue
245 # rule proving this formula a theorem
246 orig = len(self.cur)
247 try:
248 start = end = self.rule(start, text)
249 except AssertionError:
250 del self.cur[orig:]
251 start = end = self.error_till_line_end(start, text)
252 continue
253 # skip whitespace after rule
254 start = end = self.whitespace(end, text)
255 # line marker
256 if text[start] == '(':
257 orig = len(self.cur)
258 try:
259 start = end = self.lineno(start, text)
260 except AssertionError:
261 del self.cur[orig:]
262 start = end = self.error_till_line_end(start, text)
263 continue
264 start = end = self.whitespace(start, text)
265 except IndexError:
266 try:
267 del self.cur[orig:]
268 except NameError:
269 pass # if orig was never defined, fine
270 self.error_till_line_end(start, text)
271 return self.cur