Mercurial Repositories > eric / file comparison
comparison: ThirdParty/Pygments/pygments/lexers/theorem.py
ThirdParty/Pygments/pygments/lexers/theorem.py
- changeset 4697
- c2e9bf425554
- parent 4172
- 4f20dba37ab6
- child 5713
- 6762afd9f963
equal
deleted
inserted
replaced
| 4696:bf4d19a7cade | 4697:c2e9bf425554 |
|---|---|
| 3 pygments.lexers.theorem | 3 pygments.lexers.theorem |
| 4 ~~~~~~~~~~~~~~~~~~~~~~~ | 4 ~~~~~~~~~~~~~~~~~~~~~~~ |
| 5 | 5 |
| 6 Lexers for theorem-proving languages. | 6 Lexers for theorem-proving languages. |
| 7 | 7 |
| 8 :copyright: Copyright 2006-2014 by the Pygments team, see AUTHORS. | 8 :copyright: Copyright 2006-2015 by the Pygments team, see AUTHORS. |
| 9 :license: BSD, see LICENSE for details. | 9 :license: BSD, see LICENSE for details. |
| 10 """ | 10 """ |
| 11 | 11 |
| 12 import re | 12 import re |
| 13 | 13 |
| 41 'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure', | 41 'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure', |
| 42 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Corollary', | 42 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Corollary', |
| 43 'Proposition', 'Fact', 'Remark', 'Example', 'Proof', 'Goal', 'Save', | 43 'Proposition', 'Fact', 'Remark', 'Example', 'Proof', 'Goal', 'Save', |
| 44 'Qed', 'Defined', 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', | 44 'Qed', 'Defined', 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', |
| 45 'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside', | 45 'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside', |
| 46 'outside', 'Check', | 46 'outside', 'Check', 'Global', 'Instance', 'Class', 'Existing', |
| 47 'Universe', 'Polymorphic', 'Monomorphic', 'Context' | |
| 47 ) | 48 ) |
| 48 keywords2 = ( | 49 keywords2 = ( |
| 49 # Gallina | 50 # Gallina |
| 50 'forall', 'exists', 'exists2', 'fun', 'fix', 'cofix', 'struct', | 51 'forall', 'exists', 'exists2', 'fun', 'fix', 'cofix', 'struct', |
| 51 'match', 'end', 'in', 'return', 'let', 'if', 'is', 'then', 'else', | 52 'match', 'end', 'in', 'return', 'let', 'if', 'is', 'then', 'else', |
| 62 'induction', 'using', 'refine', 'inversion', 'injection', 'rewrite', | 63 'induction', 'using', 'refine', 'inversion', 'injection', 'rewrite', |
| 63 'congr', 'unlock', 'compute', 'ring', 'field', 'replace', 'fold', | 64 'congr', 'unlock', 'compute', 'ring', 'field', 'replace', 'fold', |
| 64 'unfold', 'change', 'cutrewrite', 'simpl', 'have', 'suff', 'wlog', | 65 'unfold', 'change', 'cutrewrite', 'simpl', 'have', 'suff', 'wlog', |
| 65 'suffices', 'without', 'loss', 'nat_norm', 'assert', 'cut', 'trivial', | 66 'suffices', 'without', 'loss', 'nat_norm', 'assert', 'cut', 'trivial', |
| 66 'revert', 'bool_congr', 'nat_congr', 'symmetry', 'transitivity', 'auto', | 67 'revert', 'bool_congr', 'nat_congr', 'symmetry', 'transitivity', 'auto', |
| 67 'split', 'left', 'right', 'autorewrite', 'tauto', | 68 'split', 'left', 'right', 'autorewrite', 'tauto', 'setoid_rewrite', |
| 69 'intuition', 'eauto', 'eapply', 'econstructor', 'etransitivity', | |
| 70 'constructor', 'erewrite', 'red', 'cbv', 'lazy', 'vm_compute', | |
| 71 'native_compute', 'subst', | |
| 68 ) | 72 ) |
| 69 keywords5 = ( | 73 keywords5 = ( |
| 70 # Terminators | 74 # Terminators |
| 71 'by', 'done', 'exact', 'reflexivity', 'tauto', 'romega', 'omega', | 75 'by', 'done', 'exact', 'reflexivity', 'tauto', 'romega', 'omega', |
| 72 'assumption', 'solve', 'contradiction', 'discriminate', | 76 'assumption', 'solve', 'contradiction', 'discriminate', |
| 77 'congruence', | |
| 73 ) | 78 ) |
| 74 keywords6 = ( | 79 keywords6 = ( |
| 75 # Control | 80 # Control |
| 76 'do', 'last', 'first', 'try', 'idtac', 'repeat', | 81 'do', 'last', 'first', 'try', 'idtac', 'repeat', |
| 77 ) | 82 ) |
| 85 keyopts = ( | 90 keyopts = ( |
| 86 '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.', | 91 '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.', |
| 87 '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-', | 92 '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-', |
| 88 '<->', '=', '>', '>]', r'>\}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', | 93 '<->', '=', '>', '>]', r'>\}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', |
| 89 r'\[\|', ']', '_', '`', r'\{', r'\{<', r'\|', r'\|]', r'\}', '~', '=>', | 94 r'\[\|', ']', '_', '`', r'\{', r'\{<', r'\|', r'\|]', r'\}', '~', '=>', |
| 90 r'/\\', r'\\/', | 95 r'/\\', r'\\/', r'\{\|', r'\|\}', |
| 91 u'Π', u'λ', | 96 u'Π', u'λ', |
| 92 ) | 97 ) |
| 93 operators = r'[!$%&*+\./:<=>?@^|~-]' | 98 operators = r'[!$%&*+\./:<=>?@^|~-]' |
| 94 word_operators = ('and', 'asr', 'land', 'lor', 'lsl', 'lxor', 'mod', 'or') | |
| 95 prefix_syms = r'[!?~]' | 99 prefix_syms = r'[!?~]' |
| 96 infix_syms = r'[=<>@^|&+\*/$%-]' | 100 infix_syms = r'[=<>@^|&+\*/$%-]' |
| 97 primitives = ('unit', 'int', 'float', 'bool', 'string', 'char', 'list', | 101 primitives = ('unit', 'nat', 'bool', 'string', 'ascii', 'list') |
| 98 'array') | |
| 99 | 102 |
| 100 tokens = { | 103 tokens = { |
| 101 'root': [ | 104 'root': [ |
| 102 (r'\s+', Text), | 105 (r'\s+', Text), |
| 103 (r'false|true|\(\)|\[\]', Name.Builtin.Pseudo), | 106 (r'false|true|\(\)|\[\]', Name.Builtin.Pseudo), |
| 106 (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), | 109 (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), |
| 107 (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), | 110 (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), |
| 108 (words(keywords4, prefix=r'\b', suffix=r'\b'), Keyword), | 111 (words(keywords4, prefix=r'\b', suffix=r'\b'), Keyword), |
| 109 (words(keywords5, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo), | 112 (words(keywords5, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo), |
| 110 (words(keywords6, prefix=r'\b', suffix=r'\b'), Keyword.Reserved), | 113 (words(keywords6, prefix=r'\b', suffix=r'\b'), Keyword.Reserved), |
| 111 (r'\b([A-Z][\w\']*)(?=\s*\.)', Name.Namespace, 'dotted'), | 114 # (r'\b([A-Z][\w\']*)(\.)', Name.Namespace, 'dotted'), |
| 112 (r'\b([A-Z][\w\']*)', Name.Class), | 115 (r'\b([A-Z][\w\']*)', Name), |
| 113 (r'(%s)' % '|'.join(keyopts[::-1]), Operator), | 116 (r'(%s)' % '|'.join(keyopts[::-1]), Operator), |
| 114 (r'(%s|%s)?%s' % (infix_syms, prefix_syms, operators), Operator), | 117 (r'(%s|%s)?%s' % (infix_syms, prefix_syms, operators), Operator), |
| 115 (r'\b(%s)\b' % '|'.join(word_operators), Operator.Word), | |
| 116 (r'\b(%s)\b' % '|'.join(primitives), Keyword.Type), | 118 (r'\b(%s)\b' % '|'.join(primitives), Keyword.Type), |
| 117 | 119 |
| 118 (r"[^\W\d][\w']*", Name), | 120 (r"[^\W\d][\w']*", Name), |
| 119 | 121 |
| 120 (r'\d[\d_]*', Number.Integer), | 122 (r'\d[\d_]*', Number.Integer), |
| 128 (r"'.'", String.Char), | 130 (r"'.'", String.Char), |
| 129 (r"'", Keyword), # a stray quote is another syntax element | 131 (r"'", Keyword), # a stray quote is another syntax element |
| 130 | 132 |
| 131 (r'"', String.Double, 'string'), | 133 (r'"', String.Double, 'string'), |
| 132 | 134 |
| 133 (r'[~?][a-z][\w\']*:', Name.Variable), | 135 (r'[~?][a-z][\w\']*:', Name), |
| 134 ], | 136 ], |
| 135 'comment': [ | 137 'comment': [ |
| 136 (r'[^(*)]+', Comment), | 138 (r'[^(*)]+', Comment), |
| 137 (r'\(\*', Comment, '#push'), | 139 (r'\(\*', Comment, '#push'), |
| 138 (r'\*\)', Comment, '#pop'), | 140 (r'\*\)', Comment, '#pop'), |
| 393 'hypothesis', 'lemma', 'corollary', 'variable', 'variables', 'print', 'theorem', | 395 'hypothesis', 'lemma', 'corollary', 'variable', 'variables', 'print', 'theorem', |
| 394 'axiom', 'inductive', 'structure', 'universe', 'alias', 'help', | 396 'axiom', 'inductive', 'structure', 'universe', 'alias', 'help', |
| 395 'options', 'precedence', 'postfix', 'prefix', 'calc_trans', 'calc_subst', 'calc_refl', | 397 'options', 'precedence', 'postfix', 'prefix', 'calc_trans', 'calc_subst', 'calc_refl', |
| 396 'infix', 'infixl', 'infixr', 'notation', 'eval', 'check', 'exit', 'coercion', 'end', | 398 'infix', 'infixl', 'infixr', 'notation', 'eval', 'check', 'exit', 'coercion', 'end', |
| 397 'private', 'using', 'namespace', 'including', 'instance', 'section', 'context', | 399 'private', 'using', 'namespace', 'including', 'instance', 'section', 'context', |
| 398 'protected', 'expose', 'export', 'set_option', 'add_rewrite', 'extends') | 400 'protected', 'expose', 'export', 'set_option', 'add_rewrite', 'extends', |
| 401 'open', 'example', 'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible' | |
| 402 ) | |
| 399 | 403 |
| 400 keywords2 = ( | 404 keywords2 = ( |
| 401 'forall', 'exists', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume', 'take', | 405 'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume', 'take', |
| 402 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin', 'proof', 'qed', 'calc' | 406 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin', 'proof', 'qed', 'calc', 'match' |
| 403 ) | 407 ) |
| 404 | 408 |
| 405 keywords3 = ( | 409 keywords3 = ( |
| 406 # Sorts | 410 # Sorts |
| 407 'Type', 'Prop', | 411 'Type', 'Prop', |
| 408 ) | 412 ) |
| 409 | 413 |
| 410 keywords4 = ( | |
| 411 # Tactics | |
| 412 'apply', 'and_then', 'or_else', 'append', 'interleave', 'par', 'fixpoint', 'repeat', | |
| 413 'at_most', 'discard', 'focus_at', 'rotate', 'try_for', 'now', 'assumption', 'eassumption', | |
| 414 'state', 'intro', 'generalize', 'exact', 'unfold', 'beta', 'trace', 'focus', 'repeat1', | |
| 415 'determ', 'destruct', 'try', 'auto', 'intros' | |
| 416 ) | |
| 417 | |
| 418 operators = ( | 414 operators = ( |
| 419 '!=', '#', '&', '&&', '*', '+', '-', '/', '@', | 415 '!=', '#', '&', '&&', '*', '+', '-', '/', '@', '!', '`', |
| 420 '-.', '->', '.', '..', '...', '::', ':>', ';', ';;', '<', | 416 '-.', '->', '.', '..', '...', '::', ':>', ';', ';;', '<', |
| 421 '<-', '=', '==', '>', '_', '`', '|', '||', '~', '=>', '<=', '>=', | 417 '<-', '=', '==', '>', '_', '`', '|', '||', '~', '=>', '<=', '>=', |
| 422 '/\\', '\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥', | 418 '/\\', '\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥', |
| 423 u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈' | 419 u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞', u'⌟', u'≡', |
| 424 ) | 420 u'⟨', u'⟩' |
| 425 | 421 ) |
| 426 word_operators = ('and', 'or', 'not', 'iff', 'eq') | |
| 427 | 422 |
| 428 punctuation = ('(', ')', ':', '{', '}', '[', ']', u'⦃', u'⦄', ':=', ',') | 423 punctuation = ('(', ')', ':', '{', '}', '[', ']', u'⦃', u'⦄', ':=', ',') |
| 429 | |
| 430 primitives = ('unit', 'int', 'bool', 'string', 'char', 'list', | |
| 431 'array', 'prod', 'sum', 'pair', 'real', 'nat', 'num', 'path') | |
| 432 | 424 |
| 433 tokens = { | 425 tokens = { |
| 434 'root': [ | 426 'root': [ |
| 435 (r'\s+', Text), | 427 (r'\s+', Text), |
| 436 (r'\b(false|true)\b|\(\)|\[\]', Name.Builtin.Pseudo), | |
| 437 (r'/-', Comment, 'comment'), | 428 (r'/-', Comment, 'comment'), |
| 438 (r'--.*?$', Comment.Single), | 429 (r'--.*?$', Comment.Single), |
| 439 (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), | 430 (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), |
| 440 (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), | 431 (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), |
| 441 (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), | 432 (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), |
| 442 (words(keywords4, prefix=r'\b', suffix=r'\b'), Keyword), | |
| 443 (words(operators), Name.Builtin.Pseudo), | 433 (words(operators), Name.Builtin.Pseudo), |
| 444 (words(word_operators, prefix=r'\b', suffix=r'\b'), Name.Builtin.Pseudo), | |
| 445 (words(punctuation), Operator), | 434 (words(punctuation), Operator), |
| 446 (words(primitives, prefix=r'\b', suffix=r'\b'), Keyword.Type), | |
| 447 (u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]" | 435 (u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]" |
| 448 u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079" | 436 u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079" |
| 449 u"\u207f-\u2089\u2090-\u209c\u2100-\u214f]*", Name), | 437 u"\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*", Name), |
| 450 (r'\d+', Number.Integer), | 438 (r'\d+', Number.Integer), |
| 451 (r'"', String.Double, 'string'), | 439 (r'"', String.Double, 'string'), |
| 452 (r'[~?][a-z][\w\']*:', Name.Variable) | 440 (r'[~?][a-z][\w\']*:', Name.Variable) |
| 453 ], | 441 ], |
| 454 'comment': [ | 442 'comment': [ |
