Coverage for /pythoncovmergedfiles/medio/medio/usr/local/lib/python3.11/site-packages/pygments/lexers/tnt.py: 23%

1""" 

2 pygments.lexers.tnt 

3 ~~~~~~~~~~~~~~~~~~~ 

4 

5 Lexer for Typographic Number Theory. 

6 

7 :copyright: Copyright 2006-2025 by the Pygments team, see AUTHORS. 

8 :license: BSD, see LICENSE for details. 

9""" 

10 

11import re 

12 

13from pygments.lexer import Lexer 

14from pygments.token import Text, Comment, Operator, Keyword, Name, Number, \ 

15 Punctuation, Error 

16 

17__all__ = ['TNTLexer'] 

18 

19 

20class TNTLexer(Lexer): 

21 """ 

22 Lexer for Typographic Number Theory, as described in the book 

23 Gödel, Escher, Bach, by Douglas R. Hofstadter 

24 """ 

25 

26 name = 'Typographic Number Theory' 

27 url = 'https://github.com/Kenny2github/language-tnt' 

28 aliases = ['tnt'] 

29 filenames = ['*.tnt'] 

30 version_added = '2.7' 

31 

32 cur = [] 

33 

34 LOGIC = set('⊃→]&∧^|∨Vv') 

35 OPERATORS = set('+.⋅*') 

36 VARIABLES = set('abcde') 

37 PRIMES = set("'′") 

38 NEGATORS = set('~!') 

39 QUANTIFIERS = set('AE∀∃') 

40 NUMBERS = set('0123456789') 

41 WHITESPACE = set('\t \v\n') 

42 

43 RULES = re.compile('''(?xi) 

44 joining | separation | double-tilde | fantasy\\ rule 

45 | carry[- ]over(?:\\ of)?(?:\\ line)?\\ ([0-9]+) | detachment 

46 | contrapositive | De\\ Morgan | switcheroo 

47 | specification | generalization | interchange 

48 | existence | symmetry | transitivity 

49 | add\\ S | drop\\ S | induction 

50 | axiom\\ ([1-5]) | premise | push | pop 

51 ''') 

52 LINENOS = re.compile(r'(?:[0-9]+)(?:(?:, ?|,? and )(?:[0-9]+))*') 

53 COMMENT = re.compile(r'\[[^\n\]]+\]') 

54 

55 def __init__(self, *args, **kwargs): 

56 Lexer.__init__(self, *args, **kwargs) 

57 self.cur = [] 

58 

59 def whitespace(self, start, text, required=False): 

60 """Tokenize whitespace.""" 

61 end = start 

62 try: 

63 while text[end] in self.WHITESPACE: 

64 end += 1 

65 except IndexError: 

66 end = len(text) 

67 if required and end == start: 

68 raise AssertionError 

69 if end != start: 

70 self.cur.append((start, Text, text[start:end])) 

71 return end 

72 

73 def variable(self, start, text): 

74 """Tokenize a variable.""" 

75 if text[start] not in self.VARIABLES: 

76 raise AssertionError 

77 end = start+1 

78 while text[end] in self.PRIMES: 

79 end += 1 

80 self.cur.append((start, Name.Variable, text[start:end])) 

81 return end 

82 

83 def term(self, start, text): 

84 """Tokenize a term.""" 

85 if text[start] == 'S': # S...S(...) or S...0 

86 end = start+1 

87 while text[end] == 'S': 

88 end += 1 

89 self.cur.append((start, Number.Integer, text[start:end])) 

90 return self.term(end, text) 

91 if text[start] == '0': # the singleton 0 

92 self.cur.append((start, Number.Integer, text[start])) 

93 return start+1 

94 if text[start] in self.VARIABLES: # a''... 

95 return self.variable(start, text) 

96 if text[start] == '(': # (...+...) 

97 self.cur.append((start, Punctuation, text[start])) 

98 start = self.term(start+1, text) 

99 if text[start] not in self.OPERATORS: 

100 raise AssertionError 

101 self.cur.append((start, Operator, text[start])) 

102 start = self.term(start+1, text) 

103 if text[start] != ')': 

104 raise AssertionError 

105 self.cur.append((start, Punctuation, text[start])) 

106 return start+1 

107 raise AssertionError # no matches 

108 

109 def formula(self, start, text): 

110 """Tokenize a formula.""" 

111 if text[start] in self.NEGATORS: # ~<...> 

112 end = start+1 

113 while text[end] in self.NEGATORS: 

114 end += 1 

115 self.cur.append((start, Operator, text[start:end])) 

116 return self.formula(end, text) 

117 if text[start] in self.QUANTIFIERS: # Aa:<...> 

118 self.cur.append((start, Keyword.Declaration, text[start])) 

119 start = self.variable(start+1, text) 

120 if text[start] != ':': 

121 raise AssertionError 

122 self.cur.append((start, Punctuation, text[start])) 

123 return self.formula(start+1, text) 

124 if text[start] == '<': # <...&...> 

125 self.cur.append((start, Punctuation, text[start])) 

126 start = self.formula(start+1, text) 

127 if text[start] not in self.LOGIC: 

128 raise AssertionError 

129 self.cur.append((start, Operator, text[start])) 

130 start = self.formula(start+1, text) 

131 if text[start] != '>': 

132 raise AssertionError 

133 self.cur.append((start, Punctuation, text[start])) 

134 return start+1 

135 # ...=... 

136 start = self.term(start, text) 

137 if text[start] != '=': 

138 raise AssertionError 

139 self.cur.append((start, Operator, text[start])) 

140 start = self.term(start+1, text) 

141 return start 

142 

143 def rule(self, start, text): 

144 """Tokenize a rule.""" 

145 match = self.RULES.match(text, start) 

146 if match is None: 

147 raise AssertionError 

148 groups = sorted(match.regs[1:]) # exclude whole match 

149 for group in groups: 

150 if group[0] >= 0: # this group matched 

151 self.cur.append((start, Keyword, text[start:group[0]])) 

152 self.cur.append((group[0], Number.Integer, 

153 text[group[0]:group[1]])) 

154 if group[1] != match.end(): 

155 self.cur.append((group[1], Keyword, 

156 text[group[1]:match.end()])) 

157 break 

158 else: 

159 self.cur.append((start, Keyword, text[start:match.end()])) 

160 return match.end() 

161 

162 def lineno(self, start, text): 

163 """Tokenize a line referral.""" 

164 end = start 

165 while text[end] not in self.NUMBERS: 

166 end += 1 

167 self.cur.append((start, Punctuation, text[start])) 

168 self.cur.append((start+1, Text, text[start+1:end])) 

169 start = end 

170 match = self.LINENOS.match(text, start) 

171 if match is None: 

172 raise AssertionError 

173 if text[match.end()] != ')': 

174 raise AssertionError 

175 self.cur.append((match.start(), Number.Integer, match.group(0))) 

176 self.cur.append((match.end(), Punctuation, text[match.end()])) 

177 return match.end() + 1 

178 

179 def error_till_line_end(self, start, text): 

180 """Mark everything from ``start`` to the end of the line as Error.""" 

181 end = start 

182 try: 

183 while text[end] != '\n': # there's whitespace in rules 

184 end += 1 

185 except IndexError: 

186 end = len(text) 

187 if end != start: 

188 self.cur.append((start, Error, text[start:end])) 

189 end = self.whitespace(end, text) 

190 return end 

191 

192 def get_tokens_unprocessed(self, text): 

193 """Returns a list of TNT tokens.""" 

194 self.cur = [] 

195 start = end = self.whitespace(0, text) 

196 while start <= end < len(text): 

197 try: 

198 # try line number 

199 while text[end] in self.NUMBERS: 

200 end += 1 

201 if end != start: # actual number present 

202 self.cur.append((start, Number.Integer, text[start:end])) 

203 # whitespace is required after a line number 

204 orig = len(self.cur) 

205 try: 

206 start = end = self.whitespace(end, text, True) 

207 except AssertionError: 

208 del self.cur[orig:] 

209 start = end = self.error_till_line_end(end, text) 

210 continue 

211 # at this point it could be a comment 

212 match = self.COMMENT.match(text, start) 

213 if match is not None: 

214 self.cur.append((start, Comment, text[start:match.end()])) 

215 start = end = match.end() 

216 # anything after the closing bracket is invalid 

217 start = end = self.error_till_line_end(start, text) 

218 # do not attempt to process the rest 

219 continue 

220 del match 

221 if text[start] in '[]': # fantasy push or pop 

222 self.cur.append((start, Keyword, text[start])) 

223 start += 1 

224 end += 1 

225 else: 

226 # one formula, possibly containing subformulae 

227 orig = len(self.cur) 

228 try: 

229 start = end = self.formula(start, text) 

230 except (AssertionError, RecursionError): # not well-formed 

231 del self.cur[orig:] 

232 while text[end] not in self.WHITESPACE: 

233 end += 1 

234 self.cur.append((start, Error, text[start:end])) 

235 start = end 

236 # skip whitespace after formula 

237 orig = len(self.cur) 

238 try: 

239 start = end = self.whitespace(end, text, True) 

240 except AssertionError: 

241 del self.cur[orig:] 

242 start = end = self.error_till_line_end(start, text) 

243 continue 

244 # rule proving this formula a theorem 

245 orig = len(self.cur) 

246 try: 

247 start = end = self.rule(start, text) 

248 except AssertionError: 

249 del self.cur[orig:] 

250 start = end = self.error_till_line_end(start, text) 

251 continue 

252 # skip whitespace after rule 

253 start = end = self.whitespace(end, text) 

254 # line marker 

255 if text[start] == '(': 

256 orig = len(self.cur) 

257 try: 

258 start = end = self.lineno(start, text) 

259 except AssertionError: 

260 del self.cur[orig:] 

261 start = end = self.error_till_line_end(start, text) 

262 continue 

263 start = end = self.whitespace(start, text) 

264 except IndexError: 

265 try: 

266 del self.cur[orig:] 

267 except NameError: 

268 pass # if orig was never defined, fine 

269 self.error_till_line_end(start, text) 

270 return self.cur