elpi.py 6.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175
  1. """
  2. pygments.lexers.elpi
  3. ~~~~~~~~~~~~~~~~~~~~
  4. Lexer for the `Elpi <http://github.com/LPCIC/elpi>`_ programming language.
  5. :copyright: Copyright 2006-2025 by the Pygments team, see AUTHORS.
  6. :license: BSD, see LICENSE for details.
  7. """
  8. from pygments.lexer import RegexLexer, bygroups, include, using
  9. from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
  10. Number, Punctuation
  11. __all__ = ['ElpiLexer']
  12. from pygments.lexers.theorem import CoqLexer
  13. class ElpiLexer(RegexLexer):
  14. """
  15. Lexer for the Elpi programming language.
  16. """
  17. name = 'Elpi'
  18. url = 'http://github.com/LPCIC/elpi'
  19. aliases = ['elpi']
  20. filenames = ['*.elpi']
  21. mimetypes = ['text/x-elpi']
  22. version_added = '2.11'
  23. lcase_re = r"[a-z]"
  24. ucase_re = r"[A-Z]"
  25. digit_re = r"[0-9]"
  26. schar2_re = r"([+*^?/<>`'@#~=&!])"
  27. schar_re = rf"({schar2_re}|-|\$|_)"
  28. idchar_re = rf"({lcase_re}|{ucase_re}|{digit_re}|{schar_re})"
  29. idcharstarns_re = rf"({idchar_re}*(\.({lcase_re}|{ucase_re}){idchar_re}*)*)"
  30. symbchar_re = rf"({lcase_re}|{ucase_re}|{digit_re}|{schar_re}|:)"
  31. constant_re = rf"({ucase_re}{idchar_re}*|{lcase_re}{idcharstarns_re}|{schar2_re}{symbchar_re}*|_{idchar_re}+)"
  32. symbol_re = r"(,|<=>|->|:-|;|\?-|->|&|=>|\bas\b|\buvar\b|<|=<|=|==|>=|>|\bi<|\bi=<|\bi>=|\bi>|\bis\b|\br<|\br=<|\br>=|\br>|\bs<|\bs=<|\bs>=|\bs>|@|::|\[\]|`->|`:|`:=|\^|-|\+|\bi-|\bi\+|r-|r\+|/|\*|\bdiv\b|\bi\*|\bmod\b|\br\*|~|\bi~|\br~)"
  33. escape_re = rf"\(({constant_re}|{symbol_re})\)"
  34. const_sym_re = rf"({constant_re}|{symbol_re}|{escape_re})"
  35. tokens = {
  36. 'root': [
  37. include('elpi')
  38. ],
  39. 'elpi': [
  40. include('_elpi-comment'),
  41. (r"(:before|:after|:if|:name)(\s*)(\")",
  42. bygroups(Keyword.Mode, Text.Whitespace, String.Double),
  43. 'elpi-string'),
  44. (r"(:index)(\s*)(\()", bygroups(Keyword.Mode, Text.Whitespace, Punctuation),
  45. 'elpi-indexing-expr'),
  46. (rf"\b(external pred|pred)(\s+)({const_sym_re})",
  47. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  48. 'elpi-pred-item'),
  49. (rf"\b(external type|type)(\s+)(({const_sym_re}(,\s*)?)+)",
  50. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  51. 'elpi-type'),
  52. (rf"\b(kind)(\s+)(({const_sym_re}|,)+)",
  53. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  54. 'elpi-type'),
  55. (rf"\b(typeabbrev)(\s+)({const_sym_re})",
  56. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  57. 'elpi-type'),
  58. (r"\b(typeabbrev)(\s+)(\([^)]+\))",
  59. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  60. 'elpi-type'),
  61. (r"\b(accumulate)(\s+)(\")",
  62. bygroups(Keyword.Declaration, Text.Whitespace, String.Double),
  63. 'elpi-string'),
  64. (rf"\b(accumulate|namespace|local)(\s+)({constant_re})",
  65. bygroups(Keyword.Declaration, Text.Whitespace, Text)),
  66. (rf"\b(shorten)(\s+)({constant_re}\.)",
  67. bygroups(Keyword.Declaration, Text.Whitespace, Text)),
  68. (r"\b(pi|sigma)(\s+)([a-zA-Z][A-Za-z0-9_ ]*)(\\)",
  69. bygroups(Keyword.Declaration, Text.Whitespace, Name.Variable, Text)),
  70. (rf"\b(constraint)(\s+)(({const_sym_re}(\s+)?)+)",
  71. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  72. 'elpi-chr-rule-start'),
  73. (rf"(?=[A-Z_]){constant_re}", Name.Variable),
  74. (rf"(?=[a-z_])({constant_re}|_)\\", Name.Variable),
  75. (r"_", Name.Variable),
  76. (rf"({symbol_re}|!|=>|;)", Keyword.Declaration),
  77. (constant_re, Text),
  78. (r"\[|\]|\||=>", Keyword.Declaration),
  79. (r'"', String.Double, 'elpi-string'),
  80. (r'`', String.Double, 'elpi-btick'),
  81. (r'\'', String.Double, 'elpi-tick'),
  82. (r'\{\{', Punctuation, 'elpi-quote'),
  83. (r'\{[^\{]', Text, 'elpi-spill'),
  84. (r"\(", Punctuation, 'elpi-in-parens'),
  85. (r'\d[\d_]*', Number.Integer),
  86. (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float),
  87. (r"[\+\*\-/\^\.]", Operator),
  88. ],
  89. '_elpi-comment': [
  90. (r'%[^\n]*\n', Comment),
  91. (r'/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/', Comment),
  92. (r"\s+", Text.Whitespace),
  93. ],
  94. 'elpi-indexing-expr':[
  95. (r'[0-9 _]+', Number.Integer),
  96. (r'\)', Punctuation, '#pop'),
  97. ],
  98. 'elpi-type': [
  99. (r"(ctype\s+)(\")", bygroups(Keyword.Type, String.Double), 'elpi-string'),
  100. (r'->', Keyword.Type),
  101. (constant_re, Keyword.Type),
  102. (r"\(|\)", Keyword.Type),
  103. (r"\.", Text, '#pop'),
  104. include('_elpi-comment'),
  105. ],
  106. 'elpi-chr-rule-start': [
  107. (r"\{", Punctuation, 'elpi-chr-rule'),
  108. include('_elpi-comment'),
  109. ],
  110. 'elpi-chr-rule': [
  111. (r"\brule\b", Keyword.Declaration),
  112. (r"\\", Keyword.Declaration),
  113. (r"\}", Punctuation, '#pop:2'),
  114. include('elpi'),
  115. ],
  116. 'elpi-pred-item': [
  117. (r"[io]:", Keyword.Mode, 'elpi-ctype'),
  118. (r"\.", Text, '#pop'),
  119. include('_elpi-comment'),
  120. ],
  121. 'elpi-ctype': [
  122. (r"(ctype\s+)(\")", bygroups(Keyword.Type, String.Double), 'elpi-string'),
  123. (r'->', Keyword.Type),
  124. (constant_re, Keyword.Type),
  125. (r"\(|\)", Keyword.Type),
  126. (r",", Text, '#pop'),
  127. (r"\.", Text, '#pop:2'),
  128. include('_elpi-comment'),
  129. ],
  130. 'elpi-btick': [
  131. (r'[^` ]+', String.Double),
  132. (r'`', String.Double, '#pop'),
  133. ],
  134. 'elpi-tick': [
  135. (r'[^\' ]+', String.Double),
  136. (r'\'', String.Double, '#pop'),
  137. ],
  138. 'elpi-string': [
  139. (r'[^\"]+', String.Double),
  140. (r'"', String.Double, '#pop'),
  141. ],
  142. 'elpi-quote': [
  143. (r'\}\}', Punctuation, '#pop'),
  144. (r"\s+", Text.Whitespace),
  145. (r"(lp:)(\{\{)", bygroups(Number, Punctuation), 'elpi-quote-exit'),
  146. (rf"(lp:)((?=[A-Z_]){constant_re})", bygroups(Number, Name.Variable)),
  147. (r"((?!lp:|\}\}).)+", using(CoqLexer)),
  148. ],
  149. 'elpi-quote-exit': [
  150. include('elpi'),
  151. (r'\}\}', Punctuation, '#pop'),
  152. ],
  153. 'elpi-spill': [
  154. (r'\{[^\{]', Text, '#push'),
  155. (r'\}[^\}]', Text, '#pop'),
  156. include('elpi'),
  157. ],
  158. 'elpi-in-parens': [
  159. (r"\(", Punctuation, '#push'),
  160. include('elpi'),
  161. (r"\)", Punctuation, '#pop'),
  162. ],
  163. }