oak_lean/kind/
mod.rs

1use oak_core::{SyntaxKind, Token};
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    // 关键字
9    Axiom,
10    Constant,
11    Def,
12    Example,
13    Inductive,
14    Lemma,
15    Namespace,
16    Open,
17    Private,
18    Protected,
19    Section,
20    Structure,
21    Theorem,
22    Universe,
23    Variable,
24    Variables,
25    End,
26    Import,
27    Export,
28    Prelude,
29    Noncomputable,
30    Partial,
31    Unsafe,
32    Mutual,
33    Where,
34    Have,
35    Show,
36    Suffices,
37    Let,
38    In,
39    If,
40    Then,
41    Else,
42    Match,
43    With,
44    Fun,
45    Do,
46    For,
47    While,
48    Break,
49    Continue,
50    Return,
51    Try,
52    Catch,
53    Finally,
54    Throw,
55
56    // 标识符和字面量
57    Identifier,
58    IntegerLiteral,
59    FloatLiteral,
60    StringLiteral,
61    CharLiteral,
62
63    // 操作符
64    Plus,      // +
65    Minus,     // -
66    Star,      // *
67    Slash,     // /
68    Percent,   // %
69    Caret,     // ^
70    Hash,      // #
71    Ampersand, // &
72    Pipe,      // |
73    Tilde,     // ~
74    Bang,      // !
75    Question,  // ?
76    At,        // @
77    Dollar,    // $
78    Arrow,     // ->
79    FatArrow,  // =>
80    Eq,        // =
81    Ne,        // !=
82    Lt,        // <
83    Le,        // <=
84    Gt,        // >
85    Ge,        // >=
86    And,       // &&
87    Or,        // ||
88    Not,       // not
89    Append,    // ++
90    Cons,      // ::
91
92    // 分隔符
93    LeftParen,    // (
94    RightParen,   // )
95    LeftBrace,    // {
96    RightBrace,   // }
97    LeftBracket,  // [
98    RightBracket, // ]
99    LeftAngle,    // ⟨
100    RightAngle,   // ⟩
101    Semicolon,    // ;
102    Colon,        // :
103    Comma,        // ,
104    Dot,          // .
105    DotDot,       // ..
106    ColonEq,      // :=
107    ColonColon,   // ::
108
109    // 空白和注释
110    Whitespace,
111    Comment,
112
113    // 特殊标记
114    Eof,
115    Error,
116
117    // 语法节点类型 (非终结符)
118    SourceFile,
119    Function,
120    ParameterList,
121    Parameter,
122    BlockExpression,
123    LetStatement,
124    ExpressionStatement,
125    IdentifierExpression,
126    LiteralExpression,
127    BooleanLiteral,
128    ParenthesizedExpression,
129    BinaryExpression,
130    UnaryExpression,
131    CallExpression,
132    FieldExpression,
133    IndexExpression,
134    IfExpression,
135    MatchExpression,
136    LoopExpression,
137    WhileExpression,
138    ForExpression,
139    BreakExpression,
140    ContinueExpression,
141    ReturnExpression,
142    StructExpression,
143    TupleExpression,
144    ArrayExpression,
145    RangeExpression,
146    ClosureExpression,
147    AsyncBlockExpression,
148    UnsafeBlockExpression,
149    TryExpression,
150    AwaitExpression,
151    MacroCall,
152    Path,
153    PathSegment,
154    GenericArgs,
155    TypePath,
156    TupleType,
157    ArrayType,
158    SliceType,
159    ReferenceType,
160    PointerType,
161    FunctionType,
162    TraitObjectType,
163    ImplTraitType,
164    InferredType,
165    NeverType,
166    Pattern,
167    IdentifierPattern,
168    WildcardPattern,
169    TuplePattern,
170    StructPattern,
171    TupleStructPattern,
172    SlicePattern,
173    ReferencePattern,
174    LiteralPattern,
175    RangePattern,
176    OrPattern,
177    RestPattern,
178    StructDeclaration,
179    EnumDeclaration,
180    UnionDeclaration,
181    TraitDeclaration,
182    ImplDeclaration,
183    ModuleDeclaration,
184    UseDeclaration,
185    ConstDeclaration,
186    StaticDeclaration,
187    TypeAliasDeclaration,
188    ExternBlock,
189    ExternFunction,
190    Attribute,
191    Visibility,
192    GenericParams,
193    GenericParam,
194    TypeParam,
195    ConstParam,
196    LifetimeParam,
197    WhereClause,
198    WherePredicate,
199    ReturnType,
200    FieldList,
201    Field,
202    Variant,
203    VariantList,
204    AssociatedItem,
205    TraitItem,
206    ImplItem,
207}
208
209impl SyntaxKind for LeanSyntaxKind {
210    fn is_trivia(&self) -> bool {
211        matches!(self, Self::Whitespace | Self::Comment)
212    }
213
214    fn is_comment(&self) -> bool {
215        matches!(self, Self::Comment)
216    }
217
218    fn is_whitespace(&self) -> bool {
219        matches!(self, Self::Whitespace)
220    }
221
222    fn is_token_type(&self) -> bool {
223        use LeanSyntaxKind::*;
224        !matches!(
225            self,
226            Error | Eof |
227            // 语法节点类型 (非终结符)
228            SourceFile | Function | ParameterList | Parameter | BlockExpression |
229            LetStatement | ExpressionStatement | IdentifierExpression | LiteralExpression |
230            BooleanLiteral | ParenthesizedExpression | BinaryExpression | UnaryExpression |
231            CallExpression | FieldExpression | IndexExpression | IfExpression |
232            MatchExpression | LoopExpression | WhileExpression | ForExpression |
233            BreakExpression | ContinueExpression | ReturnExpression | StructExpression |
234            TupleExpression | ArrayExpression | RangeExpression | ClosureExpression |
235            AsyncBlockExpression | UnsafeBlockExpression | TryExpression | AwaitExpression |
236            MacroCall | Path | PathSegment | GenericArgs | TypePath | TupleType |
237            ArrayType | SliceType | ReferenceType | PointerType | FunctionType |
238            TraitObjectType | ImplTraitType | InferredType | NeverType | Pattern |
239            IdentifierPattern | WildcardPattern | TuplePattern | StructPattern |
240            TupleStructPattern | SlicePattern | ReferencePattern | LiteralPattern |
241            RangePattern | OrPattern | RestPattern | StructDeclaration | EnumDeclaration | UnionDeclaration |
242             TraitDeclaration | ImplDeclaration | ModuleDeclaration | UseDeclaration | ConstDeclaration |
243             StaticDeclaration | TypeAliasDeclaration | ExternBlock | ExternFunction |
244            Attribute | Visibility | GenericParams | GenericParam | TypeParam |
245            ConstParam | LifetimeParam | WhereClause | WherePredicate |
246            ReturnType | FieldList | Field | Variant | VariantList |
247            AssociatedItem | TraitItem | ImplItem
248        )
249    }
250
251    fn is_element_type(&self) -> bool {
252        use LeanSyntaxKind::*;
253        matches!(
254            self,
255            Error | Eof |
256            // 语法节点类型 (非终结符)
257            SourceFile | Function | ParameterList | Parameter | BlockExpression |
258            LetStatement | ExpressionStatement | IdentifierExpression | LiteralExpression |
259            BooleanLiteral | ParenthesizedExpression | BinaryExpression | UnaryExpression |
260            CallExpression | FieldExpression | IndexExpression | IfExpression |
261            MatchExpression | LoopExpression | WhileExpression | ForExpression |
262            BreakExpression | ContinueExpression | ReturnExpression | StructExpression |
263            TupleExpression | ArrayExpression | RangeExpression | ClosureExpression |
264            AsyncBlockExpression | UnsafeBlockExpression | TryExpression | AwaitExpression |
265            MacroCall | Path | PathSegment | GenericArgs | TypePath | TupleType |
266            ArrayType | SliceType | ReferenceType | PointerType | FunctionType |
267            TraitObjectType | ImplTraitType | InferredType | NeverType | Pattern |
268            IdentifierPattern | WildcardPattern | TuplePattern | StructPattern |
269            TupleStructPattern | SlicePattern | ReferencePattern | LiteralPattern |
270            RangePattern | OrPattern | RestPattern | StructDeclaration | EnumDeclaration | UnionDeclaration |
271             TraitDeclaration | ImplDeclaration | ModuleDeclaration | UseDeclaration | ConstDeclaration |
272             StaticDeclaration | TypeAliasDeclaration | ExternBlock | ExternFunction |
273            Attribute | Visibility | GenericParams | GenericParam | TypeParam |
274            ConstParam | LifetimeParam | WhereClause | WherePredicate |
275            ReturnType | FieldList | Field | Variant | VariantList |
276            AssociatedItem | TraitItem | ImplItem
277        )
278    }
279}
oak_lean/kind/mod.rs

oak_lean/kind/
mod.rs
