Merge in HSAIL lexer (PR#518).

1 files changed, 29 insertions, 24 deletions

diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py
index 47fdc8b6..f8c7d0a9 100644
--- a/pygments/lexers/theorem.py
+++ b/pygments/lexers/theorem.py
@@ -43,7 +43,8 @@ class CoqLexer(RegexLexer):
         'Proposition', 'Fact', 'Remark', 'Example', 'Proof', 'Goal', 'Save',
         'Qed', 'Defined', 'Hint', 'Resolve', 'Rewrite', 'View', 'Search',
         'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside',
-        'outside', 'Check',
+        'outside', 'Check', 'Global', 'Instance', 'Class', 'Existing',
+        'Universe', 'Polymorphic', 'Monomorphic', 'Context'
     )
     keywords2 = (
         # Gallina
@@ -64,12 +65,16 @@ class CoqLexer(RegexLexer):
         'unfold', 'change', 'cutrewrite', 'simpl', 'have', 'suff', 'wlog',
         'suffices', 'without', 'loss', 'nat_norm', 'assert', 'cut', 'trivial',
         'revert', 'bool_congr', 'nat_congr', 'symmetry', 'transitivity', 'auto',
-        'split', 'left', 'right', 'autorewrite', 'tauto',
+        'split', 'left', 'right', 'autorewrite', 'tauto', 'setoid_rewrite',
+        'intuition', 'eauto', 'eapply', 'econstructor', 'etransitivity',
+        'constructor', 'erewrite', 'red', 'cbv', 'lazy', 'vm_compute',
+        'native_compute', 'subst',
     )
     keywords5 = (
         # Terminators
         'by', 'done', 'exact', 'reflexivity', 'tauto', 'romega', 'omega',
         'assumption', 'solve', 'contradiction', 'discriminate',
+        'congruence',
     )
     keywords6 = (
         # Control
@@ -87,15 +92,13 @@ class CoqLexer(RegexLexer):
         '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-',
         '<->', '=', '>', '>]', r'>\}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>',
         r'\[\|', ']', '_', '`', r'\{', r'\{<', r'\|', r'\|]', r'\}', '~', '=>',
-        r'/\\', r'\\/',
+        r'/\\', r'\\/', r'\{\|', r'\|\}',
         u'Π', u'λ',
     )
     operators = r'[!$%&*+\./:<=>?@^|~-]'
-    word_operators = ('and', 'asr', 'land', 'lor', 'lsl', 'lxor', 'mod', 'or')
     prefix_syms = r'[!?~]'
     infix_syms = r'[=<>@^|&+\*/$%-]'
-    primitives = ('unit', 'int', 'float', 'bool', 'string', 'char', 'list',
-                  'array')
+    primitives = ('unit', 'nat', 'bool', 'string', 'ascii', 'list')
 
     tokens = {
         'root': [
@@ -108,11 +111,10 @@ class CoqLexer(RegexLexer):
             (words(keywords4, prefix=r'\b', suffix=r'\b'), Keyword),
             (words(keywords5, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo),
             (words(keywords6, prefix=r'\b', suffix=r'\b'), Keyword.Reserved),
-            (r'\b([A-Z][\w\']*)(?=\s*\.)', Name.Namespace, 'dotted'),
-            (r'\b([A-Z][\w\']*)', Name.Class),
+            # (r'\b([A-Z][\w\']*)(\.)', Name.Namespace, 'dotted'),
+            (r'\b([A-Z][\w\']*)', Name),
             (r'(%s)' % '|'.join(keyopts[::-1]), Operator),
             (r'(%s|%s)?%s' % (infix_syms, prefix_syms, operators), Operator),
-            (r'\b(%s)\b' % '|'.join(word_operators), Operator.Word),
             (r'\b(%s)\b' % '|'.join(primitives), Keyword.Type),
 
             (r"[^\W\d][\w']*", Name),
@@ -130,7 +132,7 @@ class CoqLexer(RegexLexer):
 
             (r'"', String.Double, 'string'),
 
-            (r'[~?][a-z][\w\']*:', Name.Variable),
+            (r'[~?][a-z][\w\']*:', Name),
         ],
         'comment': [
             (r'[^(*)]+', Comment),
@@ -388,20 +390,23 @@ class LeanLexer(RegexLexer):
 
     flags = re.MULTILINE | re.UNICODE
 
-    keywords1 = ('import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition', 'renaming',
-                 'inline', 'hiding', 'exposing', 'parameter', 'parameters', 'conjecture',
-                 'hypothesis', 'lemma', 'corollary', 'variable', 'variables', 'print', 'theorem',
-                 'axiom', 'inductive', 'structure', 'universe', 'alias', 'help',
-                 'options', 'precedence', 'postfix', 'prefix', 'calc_trans', 'calc_subst', 'calc_refl',
-                 'infix', 'infixl', 'infixr', 'notation', 'eval', 'check', 'exit', 'coercion', 'end',
-                 'private', 'using', 'namespace', 'including', 'instance', 'section', 'context',
-                 'protected', 'expose', 'export', 'set_option', 'add_rewrite', 'extends',
-                 'open', 'example', 'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible'
+    keywords1 = (
+        'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition',
+        'renaming', 'inline', 'hiding', 'exposing', 'parameter', 'parameters',
+        'conjecture', 'hypothesis', 'lemma', 'corollary', 'variable', 'variables',
+        'print', 'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias',
+        'help', 'options', 'precedence', 'postfix', 'prefix', 'calc_trans',
+        'calc_subst', 'calc_refl', 'infix', 'infixl', 'infixr', 'notation', 'eval',
+        'check', 'exit', 'coercion', 'end', 'private', 'using', 'namespace',
+        'including', 'instance', 'section', 'context', 'protected', 'expose',
+        'export', 'set_option', 'add_rewrite', 'extends', 'open', 'example',
+        'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible',
     )
 
     keywords2 = (
-        'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume', 'take',
-        'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin', 'proof', 'qed', 'calc', 'match'
+        'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume',
+        'take', 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin',
+        'proof', 'qed', 'calc', 'match',
     )
 
     keywords3 = (
@@ -412,10 +417,10 @@ class LeanLexer(RegexLexer):
     operators = (
         '!=', '#', '&', '&&', '*', '+', '-', '/', '@', '!', '`',
         '-.', '->', '.', '..', '...', '::', ':>', ';', ';;', '<',
-        '<-', '=', '==', '>', '_', '`', '|', '||', '~', '=>', '<=', '>=',
+        '<-', '=', '==', '>', '_', '|', '||', '~', '=>', '<=', '>=',
         '/\\', '\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥',
-        u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞', u'⌟', u'≡',
-        u'⟨', u'⟩'
+        u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞',
+        u'⌟', u'≡', u'⟨', u'⟩',
     )
 
     punctuation = ('(', ')', ':', '{', '}', '[', ']', u'⦃', u'⦄', ':=', ',')