pygment style for elpi

alectryon/elpi_lexer.py

@@ -0,0 +1,153 @@
+
+"""
+A pygments lexer for Elpi.
+"""
+
+from pygments.lexer import RegexLexer, default, words, bygroups, include, inherit
+from pygments.regexopt import regex_opt, regex_opt_inner
+from pygments.token import \
+    Text, Comment, Operator, Keyword, Name, String, Number
+
+class ElpiLexer(RegexLexer):
+    """
+    For the `Elpi <http://github.com/LPCIC/elpi>`_ programming language.
+
+    .. versionadded:: 1.0
+    """
+
+    name = 'Elpi'
+    aliases = ['elpi']
+    filenames = ['*.elpi']
+    mimetypes = ['text/x-elpi']
+
+    lcase_re = r"[a-z]"
+    ucase_re = r"[A-Z]"
+    digit_re = r"[0-9]"
+    schar2_re = r"(\+|\*|/|\^|<|>|`|'|\?|@|#|~|=|&|!)"
+    schar_re = r"({}|-|\$|_)".format(schar2_re)
+    idchar_re = r"({}|{}|{}|{})".format(lcase_re,ucase_re,digit_re,schar_re)
+    idcharstarns_re = r"({}+|(?=\.[a-z])\.{}+)".format(idchar_re,idchar_re)
+    symbchar_re = r"({}|{}|{}|{}|:)".format(lcase_re, ucase_re, digit_re, schar_re)
+    constant_re = r"({}{}*|{}{}*|{}{}*|_{}+)".format(ucase_re, idchar_re, lcase_re, idcharstarns_re,schar2_re, symbchar_re,idchar_re)
+    symbol_re=r"(,|<=>|->|:-|;|\?-|->|&|=>|as|<|=<|=|==|>=|>|i<|i=<|i>=|i>|is|r<|r=<|r>=|r>|s<|s=<|s>=|s>|@|::|`->|`:|`:=|\^|-|\+|i-|i\+|r-|r\+|/|\*|div|i\*|mod|r\*|~|i~|r~)"
+    escape_re=r"\(({}|{})\)".format(constant_re,symbol_re)
+    const_sym_re = r"({}|{}|{})".format(constant_re,symbol_re,escape_re)
+
+    tokens = {
+        'root': [ include('elpi') ],
+
+        'elpi': [
+
+            # This is real Elpi
+            (r"(:before|:after|:if|:name)(\s*)(\")",bygroups(Keyword.ElpiMode,Text,String.Double),'elpi-string'),
+            (r"(:index)(\s*\()",bygroups(Keyword.ElpiMode,Text),'elpi-indexing-expr'),
+            (r"(external pred|pred)(\s+)({})".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Name.ElpiFunction),'elpi-pred-item'),
+            (r"(external type|type)(\s+)(({}(,\s*)?)+)".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Name.ElpiFunction),'elpi-type'),
+            (r"(kind)(\s+)(({}|,)+)".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Name.ElpiFunction),'elpi-type'),
+            (r"(typeabbrev)(\s+)({})".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Keyword.Type),'elpi-type'),
+            (r"(accumulate)(\s+)(\")",bygroups(Keyword.ElpiKeyword,Text,String.Double),'elpi-string'),
+            (r"(accumulate|shorten|namespace|local)(\s+)({})".format(constant_re),bygroups(Keyword.ElpiKeyword,Text,Text)),
+            (r"(pi|sigma)(\s+)([a-zA-Z][A-Za-z0-9_ ]*)(\\)",bygroups(Keyword.ElpiKeyword,Text,Name.ElpiVariable,Text)),
+
+            (r"(?=[A-Z_]){}".format(constant_re),Name.ElpiVariable),
+            (r"(?=[a-z_]){}\\".format(constant_re),Name.ElpiVariable),
+            (r"_",Name.ElpiVariable),
+            (r"({}|!|=>|;)".format(symbol_re),Keyword.ElpiKeyword),
+            (constant_re,Text),
+            (r"\[|\]|\||=>",Keyword.ElpiKeyword),
+            (r'"', String.Double, 'elpi-string'),
+            (r'`', String.Double, 'elpi-btick'),
+            (r'\'', String.Double, 'elpi-tick'),
+            (r'\{[^\{]', Text, 'elpi-spill'),
+            (r"\(",Text,'elpi-in-parens'),
+            include('_elpi-comment'),
+            (r'\d[\d_]*', Number.ElpiInteger),
+            (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.ElpiFloat),
+            (r"[+\*-/\^]", Operator),
+        ],
+        '_elpi-comment': [
+            (r'%[^\n]*\n',Comment),
+            (r"\s+",Text),
+        ],
+        'elpi-indexing-expr':[
+            (r'[0-9 _]+',Number.ElpiInteger),
+            (r'\)',Text,'#pop'),
+        ],
+        'elpi-type': [
+            (r"(ctype\s+)(\")",bygroups(Keyword.Type,String.Double),'elpi-string'),
+            (r'->',Keyword.Type),
+            (constant_re,Keyword.Type),
+            (r"\(|\)",Keyword.Type),
+            (r"\.",Text,'#pop'),
+            include('_elpi-comment'),
+        ],
+        'elpi-pred-item': [
+            (r"[io]:",Keyword.ElpiMode,'elpi-ctype'),
+            (r"\.",Text,'#pop'),
+            include('_elpi-comment'),
+        ],
+        'elpi-ctype': [
+            (r"(ctype\s+)(\")",bygroups(Keyword.Type,String.Double),'elpi-string'),
+            (constant_re,Keyword.Type),
+            (r"\(|\)",Keyword.Type),
+            (r",",Text,'#pop'),
+            (r"\.",Text,'#pop:2'),
+            include('_elpi-comment'),
+        ],
+        'elpi-btick': [
+            (r'[^` ]+', String.Double),
+            (r'`', String.Double, '#pop'),
+        ],
+        'elpi-tick': [
+            (r'[^\' ]+', String.Double),
+            (r'\'', String.Double, '#pop'),
+        ],
+        'elpi-string': [
+            (r'[^\"]+', String.Double),
+            (r'"', String.Double, '#pop'),
+        ],
+        'elpi-spill': [
+            (r'\{[^\{]', Text, '#push'),
+            (r'\}[^\}]', Text, '#pop'),
+            include('elpi'),
+        ],
+        'elpi-in-parens': [
+            (r"\(", Operator, '#push'),
+            (r"\)", Operator, '#pop'),
+            include('elpi'),
+        ],
+
+    }
+
+from .pygments_lexer import CoqLexer
+
+class CoqLexer(CoqLexer, ElpiLexer):
+
+    tokens = {
+      'root': [
+            # No clue what inherit would do here, so we copy Coq's ones
+            include('_basic'),
+            include('_vernac'),
+            include('_keywords'),
+            include('_other'),
+      ],
+      '_quotations': [
+            (r"lp:\{\{",Text, 'elpi'),
+            (r"(lp:)([A-Za-z_0-9']+)",bygroups(Text, Name.ElpiVariable)),
+            (r"(lp:)(\()([A-Z][A-Za-z_0-9']*)([a-z0-9 ]+)(\))",bygroups(Text,Text,Name.ElpiVariable,Text,Text)),
+            inherit
+      ],
+      'antiquotation': [
+            (r"\}\}",Text,'#pop'),
+            inherit
+      ],
+      'elpi': [
+            (r"\}\}",Text,'#pop'),
+            (r"global|sort|app|fun|let|prod|match|fix", Keyword.ElpiKeyword),
+            (r"\{\{",Text,'antiquotation'), # back to Coq
+            inherit
+      ],
+
+    }
+
+__all__ = ["ElpiLexer","CoqLexer"]

alectryon/pygments.py

@@ -33,7 +33,7 @@
 
 from dominate.util import raw as dom_raw
 
-from .pygments_lexer import CoqLexer
+from .elpi_lexer import CoqLexer
 from .pygments_style import AlectryonStyle
 
 LEXER = CoqLexer(ensurenl=False) # pylint: disable=no-member
@@ -215,5 +215,6 @@ def replace_builtin_coq_lexer():
     from pygments.lexers import _lexer_cache
     from pygments.lexers._mapping import LEXERS
     (_mod, name, aliases, ext, mime) = LEXERS['CoqLexer']
-    LEXERS['CoqLexer'] = ("alectryon.pygments_lexer", name, aliases, ext, mime)
+    LEXERS['CoqLexer'] = ("alectryon.elpi_lexer", name, aliases, ext, mime)
     _lexer_cache.pop(name, None)
+    LEXERS['ElpiLexer'] = ('alectryon.elpi_lexer','Elpi',('elpi',),('*.elpi',),('text/x-elpi',))

alectryon/pygments_lexer.py

@@ -512,14 +512,19 @@ class CoqLexer(RegexLexer):
             include('_basic'),
             default("#pop"),
         ],
-
+        '_quotations': [
+        ],
+        'antiquotation': [
+            include('_gallina'),
+        ],
         # The symbol regexp below consumes symbol chars one by one.  Without
         # this, expressions like ``("x", y)`` would be incorrectly parsed as
         # ``("``, ``x``, and ``", y)``, with the first ``"`` coalesced with the
         # preceding ``(`` and the second ``"`` lexed as a string opener.
         # Clients can reconstitute multi-character symbols later (e.g. before
         # running other filters) using a ``TokenMergeFilter``.
         '_other': [
+            include('_quotations'),
             (name_re, Name),
             (evar_re, Name.Label),
             # ['] is not a symbol character according to the grammar, but it has
@@ -530,3 +535,4 @@ class CoqLexer(RegexLexer):
     }
 
 __all__ = ["CoqLexer"]
+