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

1""" 

2 pygments.lexers.theorem 

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

4 

5 Lexers for theorem-proving languages. 

6 

7 See also :mod:`pygments.lexers.lean` 

8 

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

10 :license: BSD, see LICENSE for details. 

11""" 

12 

13from pygments.lexer import RegexLexer, bygroups, default, words 

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

15 Number, Punctuation, Generic, Whitespace 

16# compatibility import 

17from pygments.lexers.lean import LeanLexer # noqa: F401 

18 

19__all__ = ['CoqLexer', 'IsabelleLexer'] 

20 

21 

22class CoqLexer(RegexLexer): 

23 """ 

24 For the Coq theorem prover. 

25 """ 

26 

27 name = 'Coq' 

28 url = 'http://coq.inria.fr/' 

29 aliases = ['coq'] 

30 filenames = ['*.v'] 

31 mimetypes = ['text/x-coq'] 

32 version_added = '1.5' 

33 

34 flags = 0 # no re.MULTILINE 

35 

36 keywords1 = ( 

37 # Vernacular commands 

38 'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Include', 'Variable', 

39 'Variables', 'Parameter', 'Parameters', 'Axiom', 'Axioms', 'Hypothesis', 

40 'Hypotheses', 'Notation', 'Local', 'Tactic', 'Reserved', 'Scope', 

41 'Open', 'Close', 'Bind', 'Declare', 'Delimit', 'Definition', 'Example', 'Let', 

42 'Ltac', 'Ltac2', 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit', 

43 'Arguments', 'Types', 'Contextual', 'Strict', 'Prenex', 

44 'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure', 

45 'Variant', 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Fact', 

46 'Remark', 'Corollary', 'Proposition', 'Property', 'Goal', 

47 'Proof', 'Restart', 'Save', 'Qed', 'Defined', 'Abort', 'Admitted', 

48 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', 'Compute', 'Eval', 

49 'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside', 

50 'outside', 'Check', 'Global', 'Instance', 'Class', 'Existing', 

51 'Universe', 'Polymorphic', 'Monomorphic', 'Context', 'Scheme', 'From', 

52 'Undo', 'Fail', 'Function', 'Program', 'Elpi', 'Extract', 'Opaque', 

53 'Transparent', 'Unshelve', 'Next Obligation', 

54 ) 

55 keywords2 = ( 

56 # Gallina 

57 'forall', 'exists', 'exists2', 'fun', 'fix', 'cofix', 'struct', 

58 'match', 'end', 'in', 'return', 'let', 'if', 'is', 'then', 'else', 

59 'for', 'of', 'nosimpl', 'with', 'as', 

60 ) 

61 keywords3 = ( 

62 # Sorts 

63 'Type', 'Prop', 'SProp', 'Set', 

64 ) 

65 keywords4 = ( 

66 # Tactics 

67 'pose', 'set', 'move', 'case', 'elim', 'apply', 'clear', 'hnf', 'intro', 

68 'intros', 'generalize', 'rename', 'pattern', 'after', 'destruct', 

69 'induction', 'using', 'refine', 'inversion', 'injection', 'rewrite', 

70 'congr', 'unlock', 'compute', 'ring', 'field', 'replace', 'fold', 

71 'unfold', 'change', 'cutrewrite', 'simpl', 'have', 'suff', 'wlog', 

72 'suffices', 'without', 'loss', 'nat_norm', 'assert', 'cut', 'trivial', 

73 'revert', 'bool_congr', 'nat_congr', 'symmetry', 'transitivity', 'auto', 

74 'split', 'left', 'right', 'autorewrite', 'tauto', 'setoid_rewrite', 

75 'intuition', 'eauto', 'eapply', 'econstructor', 'etransitivity', 

76 'constructor', 'erewrite', 'red', 'cbv', 'lazy', 'vm_compute', 

77 'native_compute', 'subst', 

78 ) 

79 keywords5 = ( 

80 # Terminators 

81 'by', 'now', 'done', 'exact', 'reflexivity', 

82 'tauto', 'romega', 'omega', 'lia', 'nia', 'lra', 'nra', 'psatz', 

83 'assumption', 'solve', 'contradiction', 'discriminate', 

84 'congruence', 'admit' 

85 ) 

86 keywords6 = ( 

87 # Control 

88 'do', 'last', 'first', 'try', 'idtac', 'repeat', 

89 ) 

90 # 'as', 'assert', 'begin', 'class', 'constraint', 'do', 'done', 

91 # 'downto', 'else', 'end', 'exception', 'external', 'false', 

92 # 'for', 'fun', 'function', 'functor', 'if', 'in', 'include', 

93 # 'inherit', 'initializer', 'lazy', 'let', 'match', 'method', 

94 # 'module', 'mutable', 'new', 'object', 'of', 'open', 'private', 

95 # 'raise', 'rec', 'sig', 'struct', 'then', 'to', 'true', 'try', 

96 # 'type', 'val', 'virtual', 'when', 'while', 'with' 

97 keyopts = ( 

98 '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.', 

99 '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-', 

100 '<->', '=', '>', '>]', r'>\}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', 

101 r'\[\|', ']', '_', '`', r'\{', r'\{<', r'lp:\{\{', r'\|', r'\|]', r'\}', '~', '=>', 

102 r'/\\', r'\\/', r'\{\|', r'\|\}', 

103 # 'Π', 'Σ', # Not defined in the standard library 

104 'λ', '¬', '∧', '∨', '∀', '∃', '→', '↔', '≠', '≤', '≥', 

105 ) 

106 operators = r'[!$%&*+\./:<=>?@^|~-]' 

107 prefix_syms = r'[!?~]' 

108 infix_syms = r'[=<>@^|&+\*/$%-]' 

109 

110 tokens = { 

111 'root': [ 

112 (r'\s+', Text), 

113 (r'false|true|\(\)|\[\]', Name.Builtin.Pseudo), 

114 (r'\(\*', Comment, 'comment'), 

115 (r'\b(?:[^\W\d][\w\']*\.)+[^\W\d][\w\']*\b', Name), 

116 (r'\bEquations\b\??', Keyword.Namespace), 

117 (r'\b(Elpi)(\s+)(Program|Query|Accumulate|Command|Typecheck|Db|Export|Tactic)?\b', bygroups(Keyword.Namespace,Text,Keyword.Namespace)), 

118 # Very weak heuristic to distinguish the Set vernacular from the Set sort 

119 (r'\bUnset\b|\bSet(?=[ \t]+[A-Z][a-z][^\n]*?\.)', Keyword.Namespace, 'set-options'), 

120 (r'\b(?:String|Number)\s+Notation', Keyword.Namespace, 'sn-notation'), 

121 (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

122 (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), 

123 (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), 

124 (words(keywords4, prefix=r'\b', suffix=r'\b'), Keyword), 

125 (words(keywords5, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo), 

126 (words(keywords6, prefix=r'\b', suffix=r'\b'), Keyword.Reserved), 

127 # (r'\b([A-Z][\w\']*)(\.)', Name.Namespace, 'dotted'), 

128 (r'\b([A-Z][\w\']*)', Name), 

129 (r'({})'.format('|'.join(keyopts[::-1])), Operator), 

130 (rf'({infix_syms}|{prefix_syms})?{operators}', Operator), 

131 

132 (r"[^\W\d][\w']*", Name), 

133 

134 (r'\d[\d_]*', Number.Integer), 

135 (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex), 

136 (r'0[oO][0-7][0-7_]*', Number.Oct), 

137 (r'0[bB][01][01_]*', Number.Bin), 

138 (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float), 

139 

140 (r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'", String.Char), 

141 

142 (r"'.'", String.Char), 

143 (r"'", Keyword), # a stray quote is another syntax element 

144 

145 (r'"', String.Double, 'string'), 

146 

147 (r'[~?][a-z][\w\']*:', Name), 

148 (r'\S', Name.Builtin.Pseudo), 

149 ], 

150 'set-options': [ 

151 (r'\s+', Text), 

152 (r'[A-Z]\w*', Keyword.Namespace), 

153 (r'"', String.Double, 'string'), 

154 (r'\d+', Number.Integer), 

155 (r'\.', Punctuation, '#pop'), 

156 ], 

157 'sn-notation': [ 

158 (r'\s+', Text), 

159 # Extra keywords to highlight only in this scope 

160 (r'\b(?:via|mapping|abstract|warning|after)\b', Keyword), 

161 (r'=>|[()\[\]:,]', Operator), 

162 (r'\b[^\W\d][\w\']*(?:\.[^\W\d][\w\']*)*\b', Name), 

163 (r'\d[\d_]*', Number.Integer), 

164 (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex), 

165 (r'\(\*', Comment, 'comment'), 

166 (r'\.', Punctuation, '#pop'), 

167 ], 

168 'comment': [ 

169 # Consume comments like ***** as one token 

170 (r'([^(*)]+|\*+(?!\)))+', Comment), 

171 (r'\(\*', Comment, '#push'), 

172 (r'\*\)', Comment, '#pop'), 

173 (r'[(*)]', Comment), 

174 ], 

175 'string': [ 

176 (r'[^"]+', String.Double), 

177 (r'""', String.Double), 

178 (r'"', String.Double, '#pop'), 

179 ], 

180 'dotted': [ 

181 (r'\s+', Text), 

182 (r'\.', Punctuation), 

183 (r'[A-Z][\w\']*(?=\s*\.)', Name.Namespace), 

184 (r'[A-Z][\w\']*', Name.Class, '#pop'), 

185 (r'[a-z][a-z0-9_\']*', Name, '#pop'), 

186 default('#pop') 

187 ], 

188 } 

189 

190 def analyse_text(text): 

191 if 'Qed' in text and 'Proof' in text: 

192 return 1 

193 

194 

195class IsabelleLexer(RegexLexer): 

196 """ 

197 For the Isabelle proof assistant. 

198 """ 

199 

200 name = 'Isabelle' 

201 url = 'https://isabelle.in.tum.de/' 

202 aliases = ['isabelle'] 

203 filenames = ['*.thy'] 

204 mimetypes = ['text/x-isabelle'] 

205 version_added = '2.0' 

206 

207 keyword_minor = ( 

208 'and', 'assumes', 'attach', 'avoids', 'binder', 'checking', 

209 'class_instance', 'class_relation', 'code_module', 'congs', 

210 'constant', 'constrains', 'datatypes', 'defines', 'file', 'fixes', 

211 'for', 'functions', 'hints', 'identifier', 'if', 'imports', 'in', 

212 'includes', 'infix', 'infixl', 'infixr', 'is', 'keywords', 'lazy', 

213 'module_name', 'monos', 'morphisms', 'no_discs_sels', 'notes', 

214 'obtains', 'open', 'output', 'overloaded', 'parametric', 'permissive', 

215 'pervasive', 'rep_compat', 'shows', 'structure', 'type_class', 

216 'type_constructor', 'unchecked', 'unsafe', 'where', 

217 ) 

218 

219 keyword_diag = ( 

220 'ML_command', 'ML_val', 'class_deps', 'code_deps', 'code_thms', 

221 'display_drafts', 'find_consts', 'find_theorems', 'find_unused_assms', 

222 'full_prf', 'help', 'locale_deps', 'nitpick', 'pr', 'prf', 

223 'print_abbrevs', 'print_antiquotations', 'print_attributes', 

224 'print_binds', 'print_bnfs', 'print_bundles', 

225 'print_case_translations', 'print_cases', 'print_claset', 

226 'print_classes', 'print_codeproc', 'print_codesetup', 

227 'print_coercions', 'print_commands', 'print_context', 

228 'print_defn_rules', 'print_dependencies', 'print_facts', 

229 'print_induct_rules', 'print_inductives', 'print_interps', 

230 'print_locale', 'print_locales', 'print_methods', 'print_options', 

231 'print_orders', 'print_quot_maps', 'print_quotconsts', 

232 'print_quotients', 'print_quotientsQ3', 'print_quotmapsQ3', 

233 'print_rules', 'print_simpset', 'print_state', 'print_statement', 

234 'print_syntax', 'print_theorems', 'print_theory', 'print_trans_rules', 

235 'prop', 'pwd', 'quickcheck', 'refute', 'sledgehammer', 'smt_status', 

236 'solve_direct', 'spark_status', 'term', 'thm', 'thm_deps', 'thy_deps', 

237 'try', 'try0', 'typ', 'unused_thms', 'value', 'values', 'welcome', 

238 'print_ML_antiquotations', 'print_term_bindings', 'values_prolog', 

239 ) 

240 

241 keyword_thy = ('theory', 'begin', 'end') 

242 

243 keyword_section = ('header', 'chapter') 

244 

245 keyword_subsection = ( 

246 'section', 'subsection', 'subsubsection', 'sect', 'subsect', 

247 'subsubsect', 

248 ) 

249 

250 keyword_theory_decl = ( 

251 'ML', 'ML_file', 'abbreviation', 'adhoc_overloading', 'arities', 

252 'atom_decl', 'attribute_setup', 'axiomatization', 'bundle', 

253 'case_of_simps', 'class', 'classes', 'classrel', 'codatatype', 

254 'code_abort', 'code_class', 'code_const', 'code_datatype', 

255 'code_identifier', 'code_include', 'code_instance', 'code_modulename', 

256 'code_monad', 'code_printing', 'code_reflect', 'code_reserved', 

257 'code_type', 'coinductive', 'coinductive_set', 'consts', 'context', 

258 'datatype', 'datatype_new', 'datatype_new_compat', 'declaration', 

259 'declare', 'default_sort', 'defer_recdef', 'definition', 'defs', 

260 'domain', 'domain_isomorphism', 'domaindef', 'equivariance', 

261 'export_code', 'extract', 'extract_type', 'fixrec', 'fun', 

262 'fun_cases', 'hide_class', 'hide_const', 'hide_fact', 'hide_type', 

263 'import_const_map', 'import_file', 'import_tptp', 'import_type_map', 

264 'inductive', 'inductive_set', 'instantiation', 'judgment', 'lemmas', 

265 'lifting_forget', 'lifting_update', 'local_setup', 'locale', 

266 'method_setup', 'nitpick_params', 'no_adhoc_overloading', 

267 'no_notation', 'no_syntax', 'no_translations', 'no_type_notation', 

268 'nominal_datatype', 'nonterminal', 'notation', 'notepad', 'oracle', 

269 'overloading', 'parse_ast_translation', 'parse_translation', 

270 'partial_function', 'primcorec', 'primrec', 'primrec_new', 

271 'print_ast_translation', 'print_translation', 'quickcheck_generator', 

272 'quickcheck_params', 'realizability', 'realizers', 'recdef', 'record', 

273 'refute_params', 'setup', 'setup_lifting', 'simproc_setup', 

274 'simps_of_case', 'sledgehammer_params', 'spark_end', 'spark_open', 

275 'spark_open_siv', 'spark_open_vcg', 'spark_proof_functions', 

276 'spark_types', 'statespace', 'syntax', 'syntax_declaration', 'text', 

277 'text_raw', 'theorems', 'translations', 'type_notation', 

278 'type_synonym', 'typed_print_translation', 'typedecl', 'hoarestate', 

279 'install_C_file', 'install_C_types', 'wpc_setup', 'c_defs', 'c_types', 

280 'memsafe', 'SML_export', 'SML_file', 'SML_import', 'approximate', 

281 'bnf_axiomatization', 'cartouche', 'datatype_compat', 

282 'free_constructors', 'functor', 'nominal_function', 

283 'nominal_termination', 'permanent_interpretation', 

284 'binds', 'defining', 'smt2_status', 'term_cartouche', 

285 'boogie_file', 'text_cartouche', 

286 ) 

287 

288 keyword_theory_script = ('inductive_cases', 'inductive_simps') 

289 

290 keyword_theory_goal = ( 

291 'ax_specification', 'bnf', 'code_pred', 'corollary', 'cpodef', 

292 'crunch', 'crunch_ignore', 

293 'enriched_type', 'function', 'instance', 'interpretation', 'lemma', 

294 'lift_definition', 'nominal_inductive', 'nominal_inductive2', 

295 'nominal_primrec', 'pcpodef', 'primcorecursive', 

296 'quotient_definition', 'quotient_type', 'recdef_tc', 'rep_datatype', 

297 'schematic_corollary', 'schematic_lemma', 'schematic_theorem', 

298 'spark_vc', 'specification', 'subclass', 'sublocale', 'termination', 

299 'theorem', 'typedef', 'wrap_free_constructors', 

300 ) 

301 

302 keyword_qed = ('by', 'done', 'qed') 

303 keyword_abandon_proof = ('sorry', 'oops') 

304 

305 keyword_proof_goal = ('have', 'hence', 'interpret') 

306 

307 keyword_proof_block = ('next', 'proof') 

308 

309 keyword_proof_chain = ( 

310 'finally', 'from', 'then', 'ultimately', 'with', 

311 ) 

312 

313 keyword_proof_decl = ( 

314 'ML_prf', 'also', 'include', 'including', 'let', 'moreover', 'note', 

315 'txt', 'txt_raw', 'unfolding', 'using', 'write', 

316 ) 

317 

318 keyword_proof_asm = ('assume', 'case', 'def', 'fix', 'presume') 

319 

320 keyword_proof_asm_goal = ('guess', 'obtain', 'show', 'thus') 

321 

322 keyword_proof_script = ( 

323 'apply', 'apply_end', 'apply_trace', 'back', 'defer', 'prefer', 

324 ) 

325 

326 operators = ( 

327 '::', ':', '(', ')', '[', ']', '_', '=', ',', '|', 

328 '+', '-', '!', '?', 

329 ) 

330 

331 proof_operators = ('{', '}', '.', '..') 

332 

333 tokens = { 

334 'root': [ 

335 (r'\s+', Whitespace), 

336 (r'\(\*', Comment, 'comment'), 

337 (r'\\<open>', String.Symbol, 'cartouche'), 

338 (r'\{\*|‹', String, 'cartouche'), 

339 

340 (words(operators), Operator), 

341 (words(proof_operators), Operator.Word), 

342 

343 (words(keyword_minor, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo), 

344 

345 (words(keyword_diag, prefix=r'\b', suffix=r'\b'), Keyword.Type), 

346 

347 (words(keyword_thy, prefix=r'\b', suffix=r'\b'), Keyword), 

348 (words(keyword_theory_decl, prefix=r'\b', suffix=r'\b'), Keyword), 

349 

350 (words(keyword_section, prefix=r'\b', suffix=r'\b'), Generic.Heading), 

351 (words(keyword_subsection, prefix=r'\b', suffix=r'\b'), Generic.Subheading), 

352 

353 (words(keyword_theory_goal, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

354 (words(keyword_theory_script, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

355 

356 (words(keyword_abandon_proof, prefix=r'\b', suffix=r'\b'), Generic.Error), 

357 

358 (words(keyword_qed, prefix=r'\b', suffix=r'\b'), Keyword), 

359 (words(keyword_proof_goal, prefix=r'\b', suffix=r'\b'), Keyword), 

360 (words(keyword_proof_block, prefix=r'\b', suffix=r'\b'), Keyword), 

361 (words(keyword_proof_decl, prefix=r'\b', suffix=r'\b'), Keyword), 

362 

363 (words(keyword_proof_chain, prefix=r'\b', suffix=r'\b'), Keyword), 

364 (words(keyword_proof_asm, prefix=r'\b', suffix=r'\b'), Keyword), 

365 (words(keyword_proof_asm_goal, prefix=r'\b', suffix=r'\b'), Keyword), 

366 

367 (words(keyword_proof_script, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo), 

368 

369 (r'\\<(\w|\^)*>', Text.Symbol), 

370 

371 (r"'[^\W\d][.\w']*", Name.Type), 

372 

373 (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex), 

374 (r'0[oO][0-7][0-7_]*', Number.Oct), 

375 (r'0[bB][01][01_]*', Number.Bin), 

376 

377 (r'"', String, 'string'), 

378 (r'`', String.Other, 'fact'), 

379 (r'[^\s:|\[\]\-()=,+!?{}._][^\s:|\[\]\-()=,+!?{}]*', Name), 

380 ], 

381 'comment': [ 

382 (r'[^(*)]+', Comment), 

383 (r'\(\*', Comment, '#push'), 

384 (r'\*\)', Comment, '#pop'), 

385 (r'[(*)]', Comment), 

386 ], 

387 'cartouche': [ 

388 (r'[^{*}\\‹›]+', String), 

389 (r'\\<open>', String.Symbol, '#push'), 

390 (r'\{\*|‹', String, '#push'), 

391 (r'\\<close>', String.Symbol, '#pop'), 

392 (r'\*\}|›', String, '#pop'), 

393 (r'\\<(\w|\^)*>', String.Symbol), 

394 (r'[{*}\\]', String), 

395 ], 

396 'string': [ 

397 (r'[^"\\]+', String), 

398 (r'\\<(\w|\^)*>', String.Symbol), 

399 (r'\\"', String), 

400 (r'\\', String), 

401 (r'"', String, '#pop'), 

402 ], 

403 'fact': [ 

404 (r'[^`\\]+', String.Other), 

405 (r'\\<(\w|\^)*>', String.Symbol), 

406 (r'\\`', String.Other), 

407 (r'\\', String.Other), 

408 (r'`', String.Other, '#pop'), 

409 ], 

410 }