Coverage for /pythoncovmergedfiles/medio/medio/usr/local/lib/python3.11/site-packages/pygments/lexers/lean.py: 89%

1""" 

2 pygments.lexers.lean 

3 ~~~~~~~~~~~~~~~~~~~~ 

4 

5 Lexers for the Lean theorem prover. 

6 

7 :copyright: Copyright 2006-2025 by the Pygments team, see AUTHORS. 

8 :license: BSD, see LICENSE for details. 

9""" 

10 

11import re 

12 

13from pygments.lexer import RegexLexer, words, include 

14from pygments.token import Comment, Operator, Keyword, Name, String, \ 

15 Number, Generic, Whitespace 

16 

17__all__ = ['Lean3Lexer', 'Lean4Lexer'] 

18 

19class Lean3Lexer(RegexLexer): 

20 """ 

21 For the Lean 3 theorem prover. 

22 """ 

23 name = 'Lean' 

24 url = 'https://leanprover-community.github.io/lean3' 

25 aliases = ['lean', 'lean3'] 

26 filenames = ['*.lean'] 

27 mimetypes = ['text/x-lean', 'text/x-lean3'] 

28 version_added = '2.0' 

29 

30 # from https://github.com/leanprover/vscode-lean/blob/1589ca3a65e394b3789409707febbd2d166c9344/syntaxes/lean.json#L186C20-L186C217 

31 _name_segment = ( 

32 "(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟]" 

33 "(?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9'ⁿ-₉ₐ-ₜᵢ-ᵪ])*") 

34 _name = _name_segment + r"(\." + _name_segment + r")*" 

35 

36 tokens = { 

37 'expression': [ 

38 (r'\s+', Whitespace), 

39 (r'/--', String.Doc, 'docstring'), 

40 (r'/-', Comment, 'comment'), 

41 (r'--.*?$', Comment.Single), 

42 (words(( 

43 'forall', 'fun', 'Pi', 'from', 'have', 'show', 'assume', 'suffices', 

44 'let', 'if', 'else', 'then', 'in', 'with', 'calc', 'match', 

45 'do' 

46 ), prefix=r'\b', suffix=r'\b'), Keyword), 

47 (words(('sorry', 'admit'), prefix=r'\b', suffix=r'\b'), Generic.Error), 

48 (words(('Sort', 'Prop', 'Type'), prefix=r'\b', suffix=r'\b'), Keyword.Type), 

49 (words(( 

50 '(', ')', ':', '{', '}', '[', ']', '⟨', '⟩', '‹', '›', '⦃', '⦄', ':=', ',', 

51 )), Operator), 

52 (_name, Name), 

53 (r'``?' + _name, String.Symbol), 

54 (r'0x[A-Za-z0-9]+', Number.Integer), 

55 (r'0b[01]+', Number.Integer), 

56 (r'\d+', Number.Integer), 

57 (r'"', String.Double, 'string'), 

58 (r"'(?:(\\[\\\"'nt])|(\\x[0-9a-fA-F]{2})|(\\u[0-9a-fA-F]{4})|.)'", String.Char), 

59 (r'[~?][a-z][\w\']*:', Name.Variable), 

60 (r'\S', Name.Builtin.Pseudo), 

61 ], 

62 'root': [ 

63 (words(( 

64 'import', 'renaming', 'hiding', 

65 'namespace', 

66 'local', 

67 'private', 'protected', 'section', 

68 'include', 'omit', 'section', 

69 'protected', 'export', 

70 'open', 

71 'attribute', 

72 ), prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

73 (words(( 

74 'lemma', 'theorem', 'def', 'definition', 'example', 

75 'axiom', 'axioms', 'constant', 'constants', 

76 'universe', 'universes', 

77 'inductive', 'coinductive', 'structure', 'extends', 

78 'class', 'instance', 

79 'abbreviation', 

80 

81 'noncomputable theory', 

82 

83 'noncomputable', 'mutual', 'meta', 

84 

85 'attribute', 

86 

87 'parameter', 'parameters', 

88 'variable', 'variables', 

89 

90 'reserve', 'precedence', 

91 'postfix', 'prefix', 'notation', 'infix', 'infixl', 'infixr', 

92 

93 'begin', 'by', 'end', 

94 

95 'set_option', 

96 'run_cmd', 

97 ), prefix=r'\b', suffix=r'\b'), Keyword.Declaration), 

98 (r'@\[', Keyword.Declaration, 'attribute'), 

99 (words(( 

100 '#eval', '#check', '#reduce', '#exit', 

101 '#print', '#help', 

102 ), suffix=r'\b'), Keyword), 

103 include('expression') 

104 ], 

105 'attribute': [ 

106 (r'\]', Keyword.Declaration, '#pop'), 

107 include('expression'), 

108 ], 

109 'comment': [ 

110 (r'[^/-]+', Comment.Multiline), 

111 (r'/-', Comment.Multiline, '#push'), 

112 (r'-/', Comment.Multiline, '#pop'), 

113 (r'[/-]', Comment.Multiline) 

114 ], 

115 'docstring': [ 

116 (r'[^/-]+', String.Doc), 

117 (r'-/', String.Doc, '#pop'), 

118 (r'[/-]', String.Doc) 

119 ], 

120 'string': [ 

121 (r'[^\\"]+', String.Double), 

122 (r"(?:(\\[\\\"'nt])|(\\x[0-9a-fA-F]{2})|(\\u[0-9a-fA-F]{4}))", String.Escape), 

123 ('"', String.Double, '#pop'), 

124 ], 

125 } 

126 

127 def analyse_text(text): 

128 if re.search(r'^import [a-z]', text, re.MULTILINE): 

129 return 0.1 

130 

131 

132LeanLexer = Lean3Lexer 

133 

134 

135class Lean4Lexer(RegexLexer): 

136 """ 

137 For the Lean 4 theorem prover. 

138 """ 

139 

140 name = 'Lean4' 

141 url = 'https://github.com/leanprover/lean4' 

142 aliases = ['lean4'] 

143 filenames = ['*.lean'] 

144 mimetypes = ['text/x-lean4'] 

145 version_added = '2.18' 

146 

147 # same as Lean3Lexer, with `!` and `?` allowed 

148 _name_segment = ( 

149 "(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟]" 

150 "(?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9'ⁿ-₉ₐ-ₜᵢ-ᵪ!?])*") 

151 _name = _name_segment + r"(\." + _name_segment + r")*" 

152 

153 keywords1 = ( 

154 'import', 'unif_hint', 

155 'renaming', 'inline', 'hiding', 'lemma', 'variable', 

156 'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias', 

157 '#help', 'precedence', 'postfix', 'prefix', 

158 'infix', 'infixl', 'infixr', 'notation', '#eval', 

159 '#check', '#reduce', '#exit', 'end', 'private', 'using', 'namespace', 

160 'instance', 'section', 'protected', 

161 'export', 'set_option', 'extends', 'open', 'example', 

162 '#print', 'opaque', 

163 'def', 'macro', 'elab', 'syntax', 'macro_rules', '#reduce', 'where', 

164 'abbrev', 'noncomputable', 'class', 'attribute', '#synth', 'mutual', 

165 'scoped', 'local', 

166 ) 

167 

168 keywords2 = ( 

169 'forall', 'fun', 'obtain', 'from', 'have', 'show', 'assume', 

170 'let', 'if', 'else', 'then', 'by', 'in', 'with', 

171 'calc', 'match', 'nomatch', 'do', 'at', 

172 ) 

173 

174 keywords3 = ( 

175 # Sorts 

176 'Type', 'Prop', 'Sort', 

177 ) 

178 

179 operators = ( 

180 '!=', '#', '&', '&&', '*', '+', '-', '/', '@', '!', 

181 '-.', '->', '.', '..', '...', '::', ':>', ';', ';;', '<', 

182 '<-', '=', '==', '>', '_', '|', '||', '~', '=>', '<=', '>=', 

183 '/\\', '\\/', '∀', 'Π', 'λ', '↔', '∧', '∨', '≠', '≤', '≥', 

184 '¬', '⁻¹', '⬝', '▸', '→', '∃', '≈', '×', '⌞', 

185 '⌟', '≡', '⟨', '⟩', "↦", 

186 ) 

187 

188 punctuation = ('(', ')', ':', '{', '}', '[', ']', '⦃', '⦄', 

189 ':=', ',') 

190 

191 tokens = { 

192 'expression': [ 

193 (r'\s+', Whitespace), 

194 (r'/--', String.Doc, 'docstring'), 

195 (r'/-', Comment, 'comment'), 

196 (r'--.*$', Comment.Single), 

197 (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), 

198 (words(('sorry', 'admit'), prefix=r'\b', suffix=r'\b'), Generic.Error), 

199 (words(operators), Name.Builtin.Pseudo), 

200 (words(punctuation), Operator), 

201 (_name_segment, Name), 

202 (r'``?' + _name, String.Symbol), 

203 (r'(?<=\.)\d+', Number), 

204 (r'(\d+\.\d*)([eE][+-]?[0-9]+)?', Number.Float), 

205 (r'\d+', Number.Integer), 

206 (r'"', String.Double, 'string'), 

207 (r'[~?][a-z][\w\']*:', Name.Variable), 

208 (r'\S', Name.Builtin.Pseudo), 

209 ], 

210 'root': [ 

211 (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

212 (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), 

213 (r'@\[', Keyword.Declaration, 'attribute'), 

214 include('expression') 

215 ], 

216 'attribute': [ 

217 (r'\]', Keyword.Declaration, '#pop'), 

218 include('expression'), 

219 ], 

220 'comment': [ 

221 # Multiline Comments 

222 (r'[^/-]+', Comment.Multiline), 

223 (r'/-', Comment.Multiline, '#push'), 

224 (r'-/', Comment.Multiline, '#pop'), 

225 (r'[/-]', Comment.Multiline) 

226 ], 

227 'docstring': [ 

228 (r'[^/-]+', String.Doc), 

229 (r'-/', String.Doc, '#pop'), 

230 (r'[/-]', String.Doc) 

231 ], 

232 'string': [ 

233 (r'[^\\"]+', String.Double), 

234 (r'\\[n"\\\n]', String.Escape), 

235 ('"', String.Double, '#pop'), 

236 ], 

237 } 

238 

239 def analyse_text(text): 

240 if re.search(r'^import [A-Z]', text, re.MULTILINE): 

241 return 0.1