elpi.py 7.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201
  1. """
  2. pygments.lexers.elpi
  3. ~~~~~~~~~~~~~~~~~~~~
  4. Lexer for the `Elpi <http://github.com/LPCIC/elpi>`_ programming language.
  5. :copyright: Copyright 2006-present 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 RocqLexer
  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(func)(\s+)({const_sym_re})",
  50. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  51. 'elpi-func-item'),
  52. (rf"\b(external type|type)(\s+)(({const_sym_re}(,\s*)?)+)",
  53. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  54. 'elpi-type'),
  55. (rf"\b(kind)(\s+)(({const_sym_re}|,)+)",
  56. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  57. 'elpi-type'),
  58. (rf"\b(typeabbrev)(\s+)({const_sym_re})",
  59. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  60. 'elpi-type'),
  61. (r"\b(typeabbrev)(\s+)(\([^)]+\))",
  62. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  63. 'elpi-type'),
  64. (r"\b(accumulate)(\s+)(\")",
  65. bygroups(Keyword.Declaration, Text.Whitespace, String.Double),
  66. 'elpi-string'),
  67. (rf"\b(accumulate|namespace|local)(\s+)({constant_re})",
  68. bygroups(Keyword.Declaration, Text.Whitespace, Text)),
  69. (rf"\b(shorten)(\s+)({constant_re}\.)",
  70. bygroups(Keyword.Declaration, Text.Whitespace, Text)),
  71. (r"\b(pi|sigma)(\s+)([a-zA-Z][A-Za-z0-9_ ]*)(\\)",
  72. bygroups(Keyword.Declaration, Text.Whitespace, Name.Variable, Text)),
  73. (rf"\b(constraint)(\s+)(({const_sym_re}(\s+)?)+)",
  74. bygroups(Keyword.Declaration, Text.Whitespace, Name.Function),
  75. 'elpi-chr-rule-start'),
  76. (rf"(?=[A-Z_]){constant_re}", Name.Variable),
  77. (rf"(?=[a-z_])({constant_re}|_)\\", Name.Variable),
  78. (r"_", Name.Variable),
  79. (rf"({symbol_re}|!|=>|;)", Keyword.Declaration),
  80. (constant_re, Text),
  81. (r"\[|\]|\||=>", Keyword.Declaration),
  82. (r'"', String.Double, 'elpi-string'),
  83. (r'`', String.Double, 'elpi-btick'),
  84. (r'\'', String.Double, 'elpi-tick'),
  85. (r'\{\{', Punctuation, 'elpi-quote'),
  86. (r'\{[^\{]', Text, 'elpi-spill'),
  87. (r"\(", Punctuation, 'elpi-in-parens'),
  88. (r'\d[\d_]*', Number.Integer),
  89. (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float),
  90. (r"[\+\*\-/\^\.]", Operator),
  91. ],
  92. '_elpi-comment': [
  93. (r'%[^\n]*\n', Comment),
  94. (r'/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/', Comment),
  95. (r"\s+", Text.Whitespace),
  96. ],
  97. 'elpi-indexing-expr':[
  98. (r'[0-9 _]+', Number.Integer),
  99. (r'\)', Punctuation, '#pop'),
  100. ],
  101. 'elpi-type': [
  102. (r"(ctype\s+)(\")", bygroups(Keyword.Type, String.Double), 'elpi-string'),
  103. (r'->', Keyword.Type),
  104. (r'prop', Keyword.Mode),
  105. (constant_re, Keyword.Type),
  106. (r"\(|\)", Keyword.Type),
  107. (r"\.", Text, '#pop'),
  108. include('_elpi-comment'),
  109. ],
  110. 'elpi-chr-rule-start': [
  111. (r"\{", Punctuation, 'elpi-chr-rule'),
  112. include('_elpi-comment'),
  113. ],
  114. 'elpi-chr-rule': [
  115. (r"\brule\b", Keyword.Declaration),
  116. (r"\\", Keyword.Declaration),
  117. (r"\}", Punctuation, '#pop:2'),
  118. include('elpi'),
  119. ],
  120. 'elpi-pred-item': [
  121. (r"[io]:", Keyword.Mode),
  122. (r"\.", Text, '#pop'),
  123. (r",", Keyword.Mode),
  124. include('_elpi-inner-pred-fun'),
  125. (r"\)", Keyword.Mode, '#pop'),
  126. (r"\(", Keyword.Type, '_elpi-type-item'),
  127. include('_elpi-comment'),
  128. include('_elpi-type-item'),
  129. ],
  130. 'elpi-func-item': [
  131. (constant_re, Keyword.Type),
  132. (r"\.", Text, '#pop'),
  133. (r",", Keyword.Mode),
  134. (r'->', Keyword.Mode),
  135. include('_elpi-inner-pred-fun'),
  136. (r"\)", Keyword.Mode, '#pop'),
  137. (r"\(", Keyword.Type, '_elpi-type-item'),
  138. include('_elpi-comment'),
  139. include('_elpi-type-item'),
  140. ],
  141. '_elpi-inner-pred-fun': [
  142. (r"(\()(\s*)(pred)", bygroups(Keyword.Mode,Text.Whitespace,Keyword.Declaration), 'elpi-pred-item'),
  143. (r"(\()(\s*)(func)", bygroups(Keyword.Mode,Text.Whitespace,Keyword.Declaration), 'elpi-func-item'),
  144. ],
  145. '_elpi-type-item': [
  146. (r'->', Keyword.Type),
  147. (constant_re, Keyword.Type),
  148. include('_elpi-inner-pred-fun'),
  149. (r"\(", Keyword.Type, '#push'),
  150. (r"\)", Keyword.Type, '#pop'),
  151. include('_elpi-comment'),
  152. ],
  153. ''
  154. 'elpi-btick': [
  155. (r'[^` ]+', String.Double),
  156. (r'`', String.Double, '#pop'),
  157. ],
  158. 'elpi-tick': [
  159. (r'[^\' ]+', String.Double),
  160. (r'\'', String.Double, '#pop'),
  161. ],
  162. 'elpi-string': [
  163. (r'[^\"]+', String.Double),
  164. (r'"', String.Double, '#pop'),
  165. ],
  166. 'elpi-quote': [
  167. (r'\}\}', Punctuation, '#pop'),
  168. (r"\s+", Text.Whitespace),
  169. (r"(lp:)(\{\{)", bygroups(Number, Punctuation), 'elpi-quote-exit'),
  170. (rf"(lp:)((?=[A-Z_]){constant_re})", bygroups(Number, Name.Variable)),
  171. (r"((?!lp:|\}\}).)+", using(RocqLexer)),
  172. ],
  173. 'elpi-quote-exit': [
  174. include('elpi'),
  175. (r'\}\}', Punctuation, '#pop'),
  176. ],
  177. 'elpi-spill': [
  178. (r'\{[^\{]', Text, '#push'),
  179. (r'\}[^\}]', Text, '#pop'),
  180. include('elpi'),
  181. ],
  182. 'elpi-in-parens': [
  183. (r"\(", Punctuation, '#push'),
  184. include('elpi'),
  185. (r"\)", Punctuation, '#pop'),
  186. ],
  187. }