1use oak_core::{ElementType, Token, TokenType, UniversalElementRole, UniversalTokenRole};
2use serde::{Deserialize, Serialize};
3
4pub type LeanToken = Token<LeanSyntaxKind>;
5
6#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
7pub enum LeanSyntaxKind {
8 Root,
10 Eof,
11
12 Axiom,
14 Constant,
15 Def,
16 Example,
17 Inductive,
18 Lemma,
19 Namespace,
20 Open,
21 Private,
22 Protected,
23 Section,
24 Structure,
25 Theorem,
26 Universe,
27 Variable,
28 Variables,
29 End,
30 Import,
31 Export,
32 Prelude,
33 Noncomputable,
34 Partial,
35 Unsafe,
36 Mutual,
37 Where,
38 Have,
39 Show,
40 Suffices,
41 Let,
42 In,
43 If,
44 Then,
45 Else,
46 Match,
47 With,
48 Fun,
49 Do,
50 For,
51 While,
52 Break,
53 Continue,
54 Return,
55 Try,
56 Catch,
57 Finally,
58 Throw,
59
60 Identifier,
62 IntegerLiteral,
63 FloatLiteral,
64 StringLiteral,
65 CharLiteral,
66
67 Plus, Minus, Star, Slash, Percent, Caret, Hash, Ampersand, Pipe, Tilde, Bang, Question, At, Dollar, Arrow, FatArrow, Eq, Ne, Lt, Le, Gt, Ge, And, Or, Not, Append, Cons, LeftParen, RightParen, LeftBrace, RightBrace, LeftBracket, RightBracket, LeftAngle, RightAngle, Semicolon, Colon, Comma, Dot, DotDot, ColonEq, ColonColon, Whitespace,
115 Newline,
116 Comment,
117
118 Error,
120
121 SourceFile,
123 Function,
124 ParameterList,
125 Parameter,
126 BlockExpression,
127 LetStatement,
128 ExpressionStatement,
129 IdentifierExpression,
130 LiteralExpression,
131 BooleanLiteral,
132 ParenthesizedExpression,
133 BinaryExpression,
134 UnaryExpression,
135 CallExpression,
136 FieldExpression,
137 IndexExpression,
138 IfExpression,
139 MatchExpression,
140 LoopExpression,
141 WhileExpression,
142 ForExpression,
143 BreakExpression,
144 ContinueExpression,
145 ReturnExpression,
146 StructExpression,
147 TupleExpression,
148 ArrayExpression,
149 RangeExpression,
150 ClosureExpression,
151 AsyncBlockExpression,
152 UnsafeBlockExpression,
153 TryExpression,
154 AwaitExpression,
155 MacroCall,
156 Path,
157 PathSegment,
158 GenericArgs,
159 TypePath,
160 TupleType,
161 ArrayType,
162 SliceType,
163 ReferenceType,
164 PointerType,
165 FunctionType,
166 TraitObjectType,
167 ImplTraitType,
168 InferredType,
169 NeverType,
170 Pattern,
171 IdentifierPattern,
172 WildcardPattern,
173 TuplePattern,
174 StructPattern,
175 TupleStructPattern,
176 SlicePattern,
177 ReferencePattern,
178 LiteralPattern,
179 RangePattern,
180 OrPattern,
181 RestPattern,
182 StructDeclaration,
183 EnumDeclaration,
184 UnionDeclaration,
185 TraitDeclaration,
186 ImplDeclaration,
187 ModuleDeclaration,
188 UseDeclaration,
189 ConstDeclaration,
190 StaticDeclaration,
191 TypeAliasDeclaration,
192 ExternBlock,
193 ExternFunction,
194 Attribute,
195 Visibility,
196 GenericParams,
197 GenericParam,
198 TypeParam,
199 ConstParam,
200 LifetimeParam,
201 WhereClause,
202 WherePredicate,
203 ReturnType,
204 FieldList,
205 Field,
206 Variant,
207 VariantList,
208 AssociatedItem,
209 TraitItem,
210 ImplItem,
211}
212
213impl TokenType for LeanSyntaxKind {
214 type Role = UniversalTokenRole;
215 const END_OF_STREAM: Self = Self::Eof;
216
217 fn role(&self) -> Self::Role {
218 match self {
219 Self::Axiom
220 | Self::Constant
221 | Self::Def
222 | Self::Example
223 | Self::Inductive
224 | Self::Lemma
225 | Self::Namespace
226 | Self::Open
227 | Self::Private
228 | Self::Protected
229 | Self::Section
230 | Self::Structure
231 | Self::Theorem
232 | Self::Universe
233 | Self::Variable
234 | Self::Variables
235 | Self::End
236 | Self::Import
237 | Self::Export
238 | Self::Prelude
239 | Self::Noncomputable
240 | Self::Partial
241 | Self::Unsafe
242 | Self::Mutual
243 | Self::Where
244 | Self::Have
245 | Self::Show
246 | Self::Suffices
247 | Self::Let
248 | Self::In
249 | Self::If
250 | Self::Then
251 | Self::Else
252 | Self::Match
253 | Self::With
254 | Self::Fun
255 | Self::Do
256 | Self::For
257 | Self::While
258 | Self::Break
259 | Self::Continue
260 | Self::Return
261 | Self::Try
262 | Self::Catch
263 | Self::Finally
264 | Self::Throw => UniversalTokenRole::Keyword,
265
266 Self::Identifier => UniversalTokenRole::Name,
267
268 Self::IntegerLiteral | Self::FloatLiteral | Self::StringLiteral | Self::CharLiteral | Self::BooleanLiteral => UniversalTokenRole::Literal,
269
270 Self::Plus
271 | Self::Minus
272 | Self::Star
273 | Self::Slash
274 | Self::Percent
275 | Self::Caret
276 | Self::Hash
277 | Self::Ampersand
278 | Self::Pipe
279 | Self::Tilde
280 | Self::Bang
281 | Self::Question
282 | Self::At
283 | Self::Dollar
284 | Self::Arrow
285 | Self::FatArrow
286 | Self::Eq
287 | Self::Ne
288 | Self::Lt
289 | Self::Le
290 | Self::Gt
291 | Self::Ge
292 | Self::And
293 | Self::Or
294 | Self::Not
295 | Self::Append
296 | Self::Cons => UniversalTokenRole::Operator,
297
298 Self::LeftParen
299 | Self::RightParen
300 | Self::LeftBrace
301 | Self::RightBrace
302 | Self::LeftBracket
303 | Self::RightBracket
304 | Self::LeftAngle
305 | Self::RightAngle
306 | Self::Semicolon
307 | Self::Colon
308 | Self::Comma
309 | Self::Dot
310 | Self::DotDot
311 | Self::ColonEq
312 | Self::ColonColon => UniversalTokenRole::Punctuation,
313
314 Self::Comment => UniversalTokenRole::Comment,
315 Self::Whitespace | Self::Newline => UniversalTokenRole::Whitespace,
316 _ => UniversalTokenRole::None,
317 }
318 }
319}
320
321impl ElementType for LeanSyntaxKind {
322 type Role = UniversalElementRole;
323
324 fn role(&self) -> Self::Role {
325 match self {
326 Self::Root | Self::SourceFile => UniversalElementRole::Root,
327 Self::Function | Self::StructDeclaration | Self::EnumDeclaration => UniversalElementRole::Definition,
328 Self::BlockExpression | Self::ParameterList | Self::FieldList => UniversalElementRole::Container,
329 Self::ExpressionStatement | Self::LetStatement => UniversalElementRole::Statement,
330 Self::IdentifierExpression => UniversalElementRole::Reference,
331 Self::LiteralExpression | Self::BooleanLiteral => UniversalElementRole::Value,
332 Self::Error => UniversalElementRole::Error,
333 _ => UniversalElementRole::None,
334 }
335 }
336}