oak_lean/lexer/
token_type.rs

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

oak_lean/lexer/
token_type.rs
