oak_vampire/kind/
mod.rs

1#![doc = include_str!("../../readme.md")]
2
3use oak_core::{ElementType, Token, TokenType, UniversalElementRole, UniversalTokenRole};
4use serde::{Deserialize, Serialize};
5
6/// Type alias for Token with VampireSyntaxKind
7pub type VampireToken = Token<VampireSyntaxKind>;
8
9#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
10pub enum VampireSyntaxKind {
11    // 根节点
12    Root,
13
14    // 基础文本
15    Text,
16    Whitespace,
17    Newline,
18
19    // 错误处理
20    Error,
21
22    // EOF
23    Eof,
24
25    // 标点符号
26    LeftParen,
27    RightParen,
28    LeftBracket,
29    RightBracket,
30    LeftBrace,
31    RightBrace,
32    Colon,
33    Semicolon,
34    Dot,
35    Comma,
36    Question,
37    Bang,
38    At,
39    Hash,
40    Dollar,
41    Percent,
42    Caret,
43    Ampersand,
44    Star,
45    Plus,
46    Minus,
47    Eq,
48    LessThan,
49    GreaterThan,
50    Slash,
51    Backslash,
52    Pipe,
53    Tilde,
54
55    // 复合操作符
56    EqEq,
57    NotEq,
58    LessEq,
59    GreaterEq,
60    AndAnd,
61    OrOr,
62    PlusPlus,
63    MinusMinus,
64    PlusEq,
65    MinusEq,
66    StarEq,
67    SlashEq,
68    PercentEq,
69    LeftShift,
70    RightShift,
71    Arrow,
72
73    // Vampire 关键字
74    FofKw,
75    CnfKw,
76    TffKw,
77    ThfKw,
78    TpiKw,
79    IncludeKw,
80    AxiomKw,
81    HypothesisKw,
82    DefinitionKw,
83    AssumptionKw,
84    LemmaKw,
85    TheoremKw,
86    ConjectureKw,
87    NegatedConjectureKw,
88    PlainKw,
89    TypeKw,
90    FiDomainKw,
91    FiFunctorsKw,
92    FiPredicatesKw,
93    UnknownKw,
94
95    // 逻辑操作符
96    ForallKw,
97    ExistsKw,
98    AndKw,
99    OrKw,
100    NotKw,
101    ImpliesKw,
102    IffKw,
103    XorKw,
104    NorKw,
105    NandKw,
106
107    // 基本类型
108    BoolKw,
109    IntKw,
110    RealKw,
111    RatKw,
112    IndividualKw,
113    OTypeKw,
114    ITypeKw,
115    TTypeKw,
116
117    // 字面量
118    IntegerLiteral,
119    RealLiteral,
120    StringLiteral,
121    BoolLiteral,
122    Identifier,
123
124    // 注释
125    LineComment,
126    BlockComment,
127}
128
129impl TokenType for VampireSyntaxKind {
130    const END_OF_STREAM: Self = Self::Eof;
131    type Role = UniversalTokenRole;
132
133    fn role(&self) -> Self::Role {
134        match self {
135            Self::Whitespace | Self::Newline => UniversalTokenRole::Whitespace,
136            Self::LineComment | Self::BlockComment => UniversalTokenRole::Comment,
137            Self::Eof => UniversalTokenRole::Eof,
138            _ => UniversalTokenRole::None,
139        }
140    }
141}
142
143impl ElementType for VampireSyntaxKind {
144    type Role = UniversalElementRole;
145
146    fn role(&self) -> Self::Role {
147        match self {
148            Self::Error => UniversalElementRole::Error,
149            _ => UniversalElementRole::None,
150        }
151    }
152}
oak_vampire/kind/mod.rs

oak_vampire/kind/
mod.rs
