oak_vampire/kind/
mod.rs

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

oak_vampire/kind/
mod.rs
